soundness issue when combining incremental mode and QF_NRA #8477
Description
This issue has been reported in #7114, but it's actually not fixed.
(declare-fun a () Real)
(declare-fun b () Real)
(check-sat)
(assert (< 0 a))
(assert (= (- b) (* a (+ a b))))
(assert (= 1 (+ (* a a) (* b b))))
(check-sat)
This query should output two sats, but since 4.12.3 it could output unsat for the second check-sat. My local outputs are:
$ for z in ~/.local/bin/z3*; do echo $z; $z /tmp/bug1.smt2; done
/Users/zhonhu/.local/bin/z3-4.10.0
sat
sat
/Users/zhonhu/.local/bin/z3-4.10.1
sat
sat
/Users/zhonhu/.local/bin/z3-4.10.2
sat
sat
/Users/zhonhu/.local/bin/z3-4.11.0
sat
sat
/Users/zhonhu/.local/bin/z3-4.11.2
sat
sat
/Users/zhonhu/.local/bin/z3-4.12.0
sat
sat
/Users/zhonhu/.local/bin/z3-4.12.1
sat
sat
/Users/zhonhu/.local/bin/z3-4.12.2
sat
sat
/Users/zhonhu/.local/bin/z3-4.12.3
sat
unsat
/Users/zhonhu/.local/bin/z3-4.12.4
sat
unsat
/Users/zhonhu/.local/bin/z3-4.12.5
sat
unsat
/Users/zhonhu/.local/bin/z3-4.12.6
sat
unsat
/Users/zhonhu/.local/bin/z3-4.13.0
sat
unsat
/Users/zhonhu/.local/bin/z3-4.13.2
sat
sat
/Users/zhonhu/.local/bin/z3-4.13.3
sat
sat
/Users/zhonhu/.local/bin/z3-4.13.4
sat
sat
/Users/zhonhu/.local/bin/z3-4.14.0
sat
sat
/Users/zhonhu/.local/bin/z3-4.14.1
sat
sat
/Users/zhonhu/.local/bin/z3-4.15.0
sat
unsat
/Users/zhonhu/.local/bin/z3-4.15.1
sat
unsat
/Users/zhonhu/.local/bin/z3-4.15.2
sat
unsat
/Users/zhonhu/.local/bin/z3-4.15.3
sat
unsat
/Users/zhonhu/.local/bin/z3-4.15.4
sat
unsat