内挿を抽出するために iz3 を使用しようとしていました。ドキュメントページに記載されている例ではうまくいくようです。Z3 が UNSAT に準拠した例として、iz3 を実行してみました。しかし、iZ3を使用すると、次のエラーがポップアップしました
iZ3: 式でサポートされていない Z3 演算子 (bvule bv100[101] main.a'64'0) iZ3: 式でサポートされていない Z3 演算子 (bvadd main.a'64'0 main.b'64'0) セグメンテーション違反
iZ3 は AUFLIA の理論のみをサポートし、 QF_AUFBV はサポートしませんか? 上記の bit_vector 操作をサポートする QF_AUFBV の補間を取得する方法はありますか? z3 4.1 バージョンにあった iZ3 を使用しました
前もって感謝します