Soundness issues for QF_NRA formulas

[rainoftime]

Hi, for the following formula,

(set-logic QF_NRA)
(set-option :model_validate true)
(declare-const r0 Real)
(declare-const r1 Real)
(assert (> (* r1 r0 r1 r0) 0.0))
(check-sat)
(get-model)

z3 99f20c5 returns an invalid model

sat
(error "line 6 column 10: an invalid model was generated")
(model 
  (define-fun r1 () Real
    0.0)
  (define-fun r0 () Real
    1.0)
)

API log
model.log

[rainoftime]

@levnach
Could you check the following formula?
At commit b0da540, seems smt.arith.solver=6 is unsound.

z3 smt.arith.solver=6 f.smt2
sat

z3 smt.arith.solver=6 f.smt2
unsat

CVC4 and Yices2 also return unsat

(set-logic QF_NRA)
(declare-const r1 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(push 1)
(declare-const r9 Real)
(declare-const v24 Bool)
(declare-const r10 Real)
(declare-const r12 Real)
(assert (or (<= r7 6805.0 (* (/ 7434.32 (/ (- r1 r1 r1 r1) (- r1))) r1 (- r1) (- r1)) (- (- r1))) false))
(assert (or (xor (< 7434.32 7434.32 r1) (= (/ (- r1) r10) (- (/ (- r1 r1 r1 r1) (- r1 r1 r1 r1)) (- r1) 7434.32 60773.0) r8 (- r1) 508987.0) v24) (> (/ (- r1 r1 r1 r1) (- r1 r1 r1 r1)) r10 7434.32 r12 r9) false))
(check-sat)

[rainoftime]

For the following QF_NRA instance,
both z3 arith.sovler {2, 6} give "unsat".

z3arith.txt

But CVC4, Yices2, and SMTInterpol return sat.

[NikolajBjorner]

it is a bug in nlsat_solver, a duplicate of an old one on this thread: #2650
It is a bug that doesn't involve quantifiers, so this is useful.

z3 z3arith.txt /v:10 /tr:nlsat_solver /tr:nlsat nlsat.check_lemmas=true

[NikolajBjorner]

Close as this is now referenced from #2650