Z3 使用 push/pop 返回不同的答案？

Question

在使用Z3检查以下问题时，我在用一对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)

特别是在直接检查时（不被push/pop包裹），Z3返回unsat （这里是在线链接：http://rise4fun.com/Z3/cDt3）

但是，当用push/pop 包装它时，Z3 返回unknown (http://rise4fun.com/Z3/epyh0)

有没有人知道为什么 Z3 会这样？

非常感谢！

Answer 1

这个问题包含通用量词（不是...（存在...）），当Z3认为它无法解决它时会放弃这些问题（这就是你得到unknown的原因）。根据使用的策略/战术/解决方案，它可能会决定早点或晚点放弃。在这种特殊情况下，它使用了一个不支持 push/pop 的求解器，添加它们会导致它回退到另一个求解器（或参数设置），从而使其放弃。

StackOverflow 上有多个关于此问题和相关问题的问题，例如，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?