Closed
Description
Hi,
For this following instance, z3 79bbbf7 gives an invalid model.
$ cat small.smt2
(declare-const x Real)
(declare-const x4 Real)
(declare-const x44 Bool)
(declare-fun r () Real)
(check-sat)
(assert (xor x44 (= 0.0 (/ r 0.0)) (= 1.0 (/ x4 0.0)) x44 (= 1.0 (* r (- (abs x)) (+ r 5)))))
(check-sat)
$ z3 model_validate=true small.smt2
sat
sat
(error "line 7 column 10: an invalid model was generated")
Metadata
Metadata
Assignees
Labels
No labels