Hi,
For this case, Z3 gives an invalid model:
[662] % z3release model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[663] %
[663] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= (- b a) 1))
(assert (= 2 (/ 1 a b)))
(assert (< b 0))
(check-sat)
[664] %
OS: Ubuntu 18.04
Commit: a14c2a3
Hi,
For this case, Z3 gives an invalid model:
OS: Ubuntu 18.04
Commit: a14c2a3