Hi,
For this formula,
(declare-fun x () Real)
(assert (= x 0.0))
(assert (= (^ x (- 1.0)) (/ 1.0 x)))
(check-sat)
(get-model)
z3 model_validate=true throw out an error:
sat
(error "line 4 column 10: an invalid model was generated")
(model
(define-fun x () Real
0.0)
(define-fun /0 ((x!0 Real) (x!1 Real)) Real
(ite (and (= x!0 1.0) (= x!1 0.0)) 1.0
0.0))
)
While this model is actually valid.
OS: Ubuntu 18.04
Commit: ad6062c
Hi,
For this formula,
z3 model_validate=true throw out an error:
While this model is actually valid.
OS: Ubuntu 18.04
Commit: ad6062c