Z3 return different answers WITH and WITHOUT using push/pop?

Question

When checking the following problem using Z3, I receive different answers when wrapping or not wrapping it by a pair of push/pop

(declare-fun sz_53 () Int)
(declare-fun x () Int)
(declare-fun u () Int)
(declare-fun y () Int)
(assert (> u 0))
(assert (= (+ y (- 0 0)) 0))
(assert (or (= (- x u) 0) (> x 0)))
(assert (<= (* (- 0 1) sz_53) 0))
(assert (or (= (- x u) 0) (not (= (- x u) 0))))
(assert (not (and (and (and (and (exists ((sz_64 Int)) (and (= sz_64 0) (exists ((sz_62 Int)) (and (exists ((sz_55 Int)) (and (<= (* (- 0 1) sz_55) 0) (= (+ sz_53 (- sz_62 sz_55)) 0))) (= (+ sz_62 (- (- 0 1) sz_64)) 0))))) (>= y 0)) (or (= (+ x (* (- 0 1) y)) 0) (> x 0))) (not (= (+ u (* (- 0 1) y)) 0))) (not (= (+ u (* (- 0 1) y)) 0)))))
(assert (not false))
(check-sat)

Particularly, when checking it directly (not wrapping by push/pop), Z3 returns unsat (Here is the online link: http://rise4fun.com/Z3/cDt3)

However, when wrapping it by push/pop, Z3 returns unknown (http://rise4fun.com/Z3/epyh0)

Is there anybody who knows why Z3 behaves like this?

Thank you very much!

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2015-07-01T12:21:52

This problem contains universal quantifiers (not ... (exists ... )), and Z3 will give up on those problems when it thinks it can't solve it (that's why you get unknown). Depending on which strategy/tactic/solver is used, it may decide to give up earlier or later. In this particular case, it uses a solver that doesn't support push/pop, adding them causes it to fall back onto a different solver (or parameter settings) that make it give up.

There are multiple questions on StackOverflow on this and related issues, e.g., z3 produces unknown for assertions without quantifiers, Different check-sat answers when asserting same property in between, Why does Z3 return “unknown” on this simple input?

Z3 return different answers WITH and WITHOUT using push/pop?

1 Answers