Hi,
For this formula:
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (<= (/ (- 2) c) a))
(check-sat)
(assert (> b 0))
(check-sat)
(get-model)
Z3 gives an invalid model:
(model
(define-fun c () Real
(/ 1.0 8.0))
(define-fun a () Real
0.0)
(define-fun b () Real
0.0)
(define-fun /0 ((x!0 Real) (x!1 Real)) Real
(ite (and (= x!0 (- 2.0)) (= x!1 (/ 1.0 8.0))) (- 16.0)
0.0))
)
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: ad6062c
Hi,
For this formula:
Z3 gives an invalid model:
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: ad6062c