z3 - Z3 のセグメンテーション違反

Question

ビットベクトル演算を使用した定量化された BitVector 式を使用したベンチマークに取り組んでいます。このベンチマークでは、Z3 4.3.0 で Linux 64 ビットのセグメンテーション エラーが発生します。この問題は、平等の推移的な使用が原因で発生すると思います。

...
(assert (= (bvadd (capacity this) (_ bv1 5)) (EAO.length (elements this))  ))
(assert (= (EAO.length (elements this)) (IKAO.length (heap this)) ))

問題の完全なベンチマークはここにあります: 例

Answer 1

クラッシュを報告していただきありがとうございます。バグを修正しました。この修正は、不安定な (進行中の) ブランチで既に利用可能です。ここでは、不安定なブランチをビルドする方法について説明します。この修正は、Z3 ナイトリー ビルドでも明日利用可能になります。

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