Performance issue on NRA logic formula

[muchang]

Hi,
For this formula,

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun vuscore2dollarskuscore () Real)
(assert
 (exists ((e Real))
  (and
   (or
    (> (/ 0 (- (+ (* g h) (* b d) (/ 6 b d)) (* (- 39 b d) vuscore2dollarskuscore))) f)
    (< vuscore2dollarskuscore (/ 0 a c)))
   (<= (/ 2 a c) h))))
(check-sat)

Z3 will be hundres of times faster if I change vuscore2dollarskuscore to i:

[760] % time z3 small.smt2
sat
real    1m47.390s
user    1m47.214s
sys     0m0.012s
[761] % time z3 small2.smt2 
sat
real    0m0.114s
user    0m0.107s
sys     0m0.004s
[762] % 
[762] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun vuscore2dollarskuscore () Real)
(assert
 (exists ((e Real))
  (and
   (or
    (> (/ 0 (- (+ (* g h) (* b d) (/ 6 b d)) (* (- 39 b d) vuscore2dollarskuscore))) f)
    (< vuscore2dollarskuscore (/ 0 a c)))
   (<= (/ 2 a c) h))))
(check-sat)
[763] % 
[763] % cat small2.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert
 (exists ((e Real))
  (and
   (or
    (> (/ 0 (- (+ (* g h) (* b d) (/ 6 b d)) (* (- 39 b d) i))) f)
    (< i (/ 0 a c)))
   (<= (/ 2 a c) h))))
(check-sat)

OS: Ubuntu 18.04
Revision: 22f1c64

[NikolajBjorner]

this is a won't fix: the branch order is fixed before search and a bad ordering can be exponentially worse than a good ordering. As I see it, it would be a major revision of the nlsat_solver to deal with this.