今日、この一見重大なバグに遭遇しました。
この 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)