CVC4 performance issue on QF_NRA formula

[muchang]

Hi, for these formulas, CVC4 reports unknown or hangs on the last formula. If we change (set-logic ALL) to (set-logic QF_NRA), cvc4 answers sat immediately.

[574] % cvc4 small.smt2
sat
sat
unknown
[575] % 
[575] % timeout -s 9 30 cvc4 --nl-ext-tplanes small.smt2
sat
sat
Killed
[576] % timeout -s 9 30 cvc4 --nl-ext-tplanes --nl-rlv=always small.smt2
sat
sat
Killed
[577] % cat small.smt2
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< (* (- 3) c) (+ 9 c a) 0))
(assert (>= (+ a (* 2 b)) 0))
(check-sat)
(reset)
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> (/ (+ a b) (* 7 b)) 0))
(assert (>= (+ a (* 2 b)) 0))
(check-sat)
(reset)
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (or (< (* (- 3) c) (+ 9 c a) 0) (> (/ (+ a b) (* 7 b)) 0)))
(assert (>= (+ a (* 2 b)) 0))
(check-sat)
[578] %

Commit: 13cf418

[nafur]

We should enable --nl-cad by default:

$ time bin/cvc4 cur.smt2 
sat
sat
unknown

real    0m1,038s
user    0m1,026s
sys 0m0,012s
$ time bin/cvc4 --nl-cad cur.smt2 
sat
sat
sat

real    0m1,031s
user    0m1,023s
sys 0m0,008s
$ time bin/cvc4 --no-nl-ext --nl-cad cur.smt2 
sat
sat
sat

real    0m0,139s
user    0m0,123s
sys 0m0,016s