HI,
For this formula,
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 0))
(assert (distinct (div (* x y) y) x))
(check-sat)
z3 nightly build gives unknown while z3-4.8.7 gives sat:
[611] % z3 simple.smt2
unknown
[612] % z3-4.8.7 simple.smt2
sat
[613] % cvc4 --quiet simple.smt2
sat
[614] % cat simple.smt2
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 0))
(assert (distinct (div (* x y) y) x))
(check-sat)
If x is replaced by 0, then z3 is able to report sat:
[618] % z3 simple2.smt2
sat
[619] % cat simple2.smt2
(declare-fun x () Int)
(declare-fun y () Int)
; (assert (= x 0))
(assert (distinct (div (* 0 y) y) 0))
(check-sat)
OS: Ubuntu 18.04
Revision: 55f62fc
HI,
For this formula,
z3 nightly build gives unknown while z3-4.8.7 gives sat:
If x is replaced by 0, then z3 is able to report sat:
OS: Ubuntu 18.04
Revision: 55f62fc