Hi,
For this formula,
(declare-fun x () Real)
(assert (= (^ (- 1.0 x) (- 1.0)) (* 2.0 (^ x (- 1.0)))))
(check-sat)
(get-model)
z3 gives an incorrect model
(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 2.0)
0.0))
)
If I feed this model to the formula, z3 reports unsat.
OS: Ubuntu 18.04
Revision: 5497022
Hi,
For this formula,
z3 gives an incorrect model
If I feed this model to the formula, z3 reports unsat.
OS: Ubuntu 18.04
Revision: 5497022