Refutation soundness issue on a QF_NRA formula

[zhendongsu]

[685] % cvc4 -q small.smt2
sat
[686] % z3release small.smt2
sat
[687] % z3release nlsat.reorder=false nlsat.simplify_conflicts=false rewriter.flat=false small.smt2
unsat
[688] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (>= (* a a) 0))
(assert (> 0 (* a (- 1 a))))
(assert (> 0 (- (ite (= a 0) 0 1))))
(assert (> 0 (+ a (* b (- b)))))
(assert (>= a 0))
(check-sat)
[689] % 

Commit: 44156f9

The issue does not reproduce if (set-logic QF_NRA) is added to the formula.

[NikolajBjorner]

Run with -v:10, shows nlsat portion is to blame. smt.arith.nl.nra=false results in unknown.
Almost for sure a duplicate of other nlsat bugs (many are now filed as separate bugs but really trace back to a very old and open bug).

BTW, Is anybody interested in (small) $ for a bug bounty on this one?

[NikolajBjorner]

duplicate #2650