2

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!

Trung Ta
  • 1,582
  • 1
  • 16
  • 25

1 Answers1

2

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?

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • Thanks for your thorough answer! I have read related questions and answers that you mentioned but there isn't any good solution for this situation. I feel that in this case, Z3 gives up ... so soon. Hope that it will be improved in future releases. – Trung Ta Jul 02 '15 at 02:39