(qfnra smt) Soundness bug on NRA formula

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[548] % z3 small.smt2
unsat
sat
[549] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(assert (forall ((g Real)) (and (= (= g f) (= g e)) (= (/ b d) h) (> (/ a c) h))))
(assert (= (/ a c) (/ b d)))
(check-sat)
(check-sat-using (then qfnra smt))
[550] %

OS: Ubuntu 18.04
Commit: 38e0968

[NikolajBjorner]

I get:

C:\z3\build>z3 4144.smt2
unsat
unknown

[zhendongsu]

Nikolaj, I can still reproduce it on my release build (as well as debug build) of the latest commit (b571e43) on Ubuntu 18.04:

[571] % z3 bug4144.smt2 
unsat
sat
[572] % z3release bug4144.smt2 
unsat
sat
[573] % cat bug4144.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(assert (forall ((g Real)) (and (= (= g f) (= g e)) (= (/ b d) h) (> (/ a c) h))))
(assert (= (/ a c) (/ b d)))
(check-sat)
(check-sat-using (then qfnra smt))
[574] % 

[NikolajBjorner]

indeed. Caused another revision of arithmetic purification, which has been a root of very many bugs.