通过假设时检查坐的错误

Question

我们今天遇到了这个看似严重的错误。

考虑this Z3 script。 （为完整起见，转载如下。）

公式不满足。我们首先用一个额外的假设检查公式，并按预期得到unsat。然而，当我们第二次检查它时，没有任何假设，Z3 现在报告sat。当我们要求一个模型时，我们得到一个明显错误的模型（本质上与(distinct 1 1) 相矛盾）。

如果我们用(push) 和(pop) 包围第一个(check-sat ...)，则结果与预期一致。这表明当 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)

Answer 1

感谢您报告错误。该错误影响所有 Z3

http://z3.codeplex.com/SourceControl/changeset/8c211dd4fcd3

为了获得工作中的分支，我们使用

git clone https://git01.codeplex.com/z3 -b unstable

使用“work-in-progress”分支可能不方便，因为您还会获得其他更新和修改。因此，另一种选择是手动将修复应用到您正在使用的版本。 请注意，修复是一个非常small modification。