Consider the following formula
(declare-fun x () Real)
(declare-fun y () Real)
(assert (= x 0.0))
(assert (= y (^ x 0.0)))
(assert (= y 1.0))
(check-sat)
(get-model)
Z3 reports a correct model here but model validation fails:
(= 1.0 (^ 0.0 0.0)) -> false
sat
(error "line 11 column 10: an invalid model was generated")
(model
(define-fun y () Real
1.0)
(define-fun x () Real
0.0)
)
The original formula has is very similar to the one in Issue #707.
OS: Ubuntu 18.04
Revision: 1d77e3e
Consider the following formula
Z3 reports a correct model here but model validation fails:
The original formula has is very similar to the one in Issue #707.
OS: Ubuntu 18.04
Revision: 1d77e3e