Refutation soundness bug in QF_NRA

[KJongUk]

Hi,
Even if the below instance is satisfiable, the following versions of z3 incorrectly return unsat.

• Tested versions of z3: from release 4.8.15 version to night build version 6ed2b44
• Tested formula

$ z3 bug.smt2
unsat
$ cvc5 bug.smt2
sat
$ cat bug.smt2
(set-logic QF_NRA)
(declare-fun v () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v5 () Real)
(declare-fun v8 () Real)
(declare-fun v10 () Real)
(declare-fun v1 () Real)
(define-fun h () Bool (= v1 0)) ;; the root cause of the bug that I guessed
(assert (and 
            (= 0 (+ (* v3 v8) (* v10 v2 v3) (* v2 v3 v5) (* v3 v5 (- 1)) (* v2 v3 v8 (- 1)))) 
            (= 0 (+ v (* v3 v8) (* v10 v2 v3) (* v2 v3 v5) (* v3 v5 (- 1)) (* v v8 (- 1)) 
                 (* v2 v3 v8 (- 1)) (* v v1 v8 (- 1)))) 
            (< 0 (* v3 v3)) (> v2 0) (> v 0)))
(assert (= v1 (+ v 1.0)))
(check-sat)

I think this bug is different from bugs that are reported already, in that the bug is triggered due to the introduction of the fresh symbol h (i.e., the bug is not triggered without introducing h) but I haven't observed similar bug-triggering patterns in old issues related to QF_NRA such as #2650.

[NikolajBjorner]

I can't take fuzzing QF_NRA bugs until there is better understanding of 2650.
Root cause analysis considers the code paths involved. The input permutations is too weak a proxy.
This is a higher bar than filing a fuzz bug with a reduced repro.