solution unsoundness issue on a QF_NIRA instance

[zhendongsu]

Commit: https://github.com/Z3Prover/z3/commit/c48dc6905056c7dbfc976ff7c54e3f7b962c240f OS: Ubuntu 18.04

The instance should be unsat.

[555] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
[556] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (<= (* c (* (to_real (mod (to_int b) 2)) 1)) a b 1 a))
(assert (> c 2))
(check-sat)

[zhendongsu]

Another likely related incremental QF_NIA instance (the last check-sat should return unsat):

[570] % z3release model_validate=true small.smt2
sat
sat
sat
(error "line 10 column 10: an invalid model was generated")
[571] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (> b 0))
(assert (= 0 (+ c a a)))
(check-sat)
(assert (< 0 c))
(check-sat)
(assert (= (+ 1 c) (div 2 b)))
(check-sat)

[zhendongsu]

An invalid model issue (as the formula is sat) that might also be related:

[569] % z3release model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
[570] % cat small.smt2
(set-option :smt.random_seed 7)
(declare-fun e () Int)
(declare-fun i () Int)
(assert (= (* i 2) (- (+ e 2 (mod (- e 1) e)))))
(check-sat)

[zhendongsu]

Another invalid model instance involving tactics:

[542] % z3release model_validate=true small.smt2
sat
(error "line 12 column 43: an invalid model was generated")
[543] % cat small.smt2
(set-option :proof true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(assert (or (and (>= b c e 0) (> (+ f g) 0) (= (+ f g (* a h)) 0 (+ (* (- 2) d) h))) (> i 0)))
(check-sat-using (then purify-arith qfufbv))