1

MacOS X10.8でZ34.3.1（マスターブランチから）を使用しています。次の例でセグメンテーション違反が発生します。

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)


(check-sat-using qe)

この問題を解決する方法について何かアイデアはありますか？

4

2 に答える 2

2

OSX と Z3 4.3.1 を使用して、説明したバグを再現することができました。このバグは修正されており、次の公式リリースで利用できるようになります。それまでの間、OSX のナイトリー ビルドを使用するか、unstable(進行中の) ブランチを使用して Z3 をビルドできます。

ナイトリー ビルドはhttp://z3.codeplex.com/releasesからダウンロードできます。「計画済み」リンクをクリックする必要があります。ここにいくつかの指示を書きました。

ところで、充足可能性を確認したい場合は、Axel によって投稿された例のように、 のsmt後にゲーム終了の戦術 ( など) を使用する必要があります。qeによって生成された結果を調べたい場合はqe、代わりに を使用する必要があります(apply qe)。

于 2013-02-19T00:49:50.613 に答える