我们今天遇到了这个看似严重的错误。
考虑这个 Z3 脚本。（为完整起见，转载如下。）
公式是不饱和的。我们首先用一个额外的假设检查公式，并得到unsat预期的结果。然而，当我们再次检查时，没有任何假设，Z3 现在报告sat. 当我们要求一个模型时，我们得到一个明显错误的模型（本质上是矛盾的(distinct 1 1)）。
(check-sat ...)如果我们用(push)和包围第一个(pop)，结果如预期。这表明，当check-sat传递额外的假设时，它会对上下文进行不合理的简化。
我们是否可能check-sat以不正确的方式使用？
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(declare-const start25 Bool)
(declare-const bf07 Bool)
(declare-const bf19 Bool)
(declare-const lt06 Int)
(declare-const ef08 Int)
(declare-const ef110 Int)
(declare-fun whileM4 (Int) Int)
(assert start25)
(assert (=> start25 (distinct lt06 1)))
(assert (=> start25 (= lt06 (whileM4 0))))
(assert (=> (not bf07) (= ef08 0)))
(assert (=> bf07 (= ef08 (whileM4 (+ 0 1)))))
(assert (=> start25 (not (< (whileM4 0) 1))))
(assert (=> start25 (= (whileM4 0) ef08)))
(assert (=> start25 (and (=> bf07 (< 0 1)) (=> (< 0 1) bf07))))
(assert (=> (not bf19) (= ef110 (+ 0 1))))
(assert (=> bf19 (= ef110 (whileM4 (+ (+ 0 1) 1)))))
(assert (=> bf07 (not (< (whileM4 (+ 0 1)) 1))))
(assert (=> bf07 (= (whileM4 (+ 0 1)) ef110)))
(assert (=> bf07 (and (=> bf19 (< (+ 0 1) 1)) (=> (< (+ 0 1) 1) bf19))))
(push) ; comment out to produce bug
(check-sat (not bf19))
(pop) ; comment out to produce bug
(check-sat)