Hi,
For this formula,
(declare-datatypes ((a 0)) (((b) (c (d a)))))
(declare-fun e () a)
(declare-fun f () a)
(assert (= f e))
(assert (not ((_ is (c (a) a)) f)))
(assert (or ((_ is (c (a) a)) e)))
(check-sat-using pqffd)
(get-model)
z3 incorrectly gives sat and an incorrect model:
(define-fun f () a
b)
(define-fun e () a
b)
If I feed this model to the formula, z3 reports unsat.
OS: Ubuntu 18.04
Revision: 805ac74
Hi,
For this formula,
z3 incorrectly gives
satand an incorrect model:If I feed this model to the formula, z3 reports
unsat.OS: Ubuntu 18.04
Revision: 805ac74