Hi,
consider the following formula.
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(assert (= (or (= 0 0)) (b 0)))
(push)
(assert (= true (distinct true (distinct false (= a 0)) (= false (b 0)))))
(check-sat)
(get-model)
Z3 returns sat here although the second assert is clearly unsatisfiable. It seems like Z3 dropped the second assert.
OS: Ubuntu 18.04
Revision: 2c6e6b1
Hi,
consider the following formula.
Z3 returns sat here although the second assert is clearly unsatisfiable. It seems like Z3 dropped the second assert.
OS: Ubuntu 18.04
Revision: 2c6e6b1