3

今日、この一見重大なバグに遭遇しました。

この Z3 スクリプトを検討してください。(完全を期すために以下に再掲します。)

式は未飽和です。最初に、追加の仮定を使用して式を確認し、unsat期待どおりに取得します。ただし、もう一度確認すると、何も仮定せずに Z3 が報告するようになりsatました。モデルを求めると、明らかに間違ったモデルが得られます (本質的に矛盾してい(distinct 1 1)ます)。

(check-sat ...)最初のものを(push)andで囲むと(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)
4

1 に答える 1

4

バグを報告していただきありがとうございます。このバグは、Z3 <= v4.3.1 のすべてに影響します。私はこのバグを修正しました。修正はすでに codeplex で入手できます。

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

進行中のブランチを取得するには、次を使用します

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

「作業中」ブランチを使用すると、他の更新や変更も取得されるため、不便な場合があります。したがって、別のオプションは、使用しているバージョンに修正を手動で適用することです。修正は非常に小さな変更であることに注意してください。

于 2012-12-17T22:14:37.063 に答える