Invalid model on QF_NRA

[merlinsun]

Hi,
For this following instance, z3 3baaba5 gives an invalid model.

$ cat small.smt2
(declare-const x26 Bool) 
(declare-const x Real) 
(declare-const x23176 Real) 
(declare-const x1 Real) 
(declare-fun b (Int Real) Bool) 
(declare-fun v () Real) 
(declare-fun var1 () Real) 
(declare-fun r1 () Real) 
(declare-fun var3 () Real) 
(declare-fun va () Real) 
(declare-fun r () Real) 
(declare-fun r3 () Real) 
(declare-fun ar33 () Real) 
(declare-fun r38 () Real) 
(declare-fun r11 () Int) 
(declare-fun r4 () Real) 
(declare-fun var () Real) 
(push 1) 
(assert x26) 
(check-sat) 
(pop 1) 
(assert (or (and true true (>= r1 0.0) (= 0.0 (/ x23176 0.0))) (and (> r11 0) (= va (- 0.0 1 (/ 0.0 var)))))) 
(assert (or x26 (< 0.0 x) (b 0 0.0) (<= x r38) (distinct va (* 101 x x x23176) 0.0 x1) (and (= 24 x1) (<= x r3) (<= x23176 0)) (xor (>= 1 (/ 2 v r4)) (> x 1) (>= var3 0) (> 0 (* var1 (- 1 var1))) (= 1.0 (- ar33 r)) x26 (= 1 v) (<= (- (div x1 x1)) 0)))) 
(check-sat)            
$ z3 model_validate=true small.smt2
sat
sat
(error "line 24 column 10: an invalid model was generated")

[NikolajBjorner]

duplicate #7017