Z3のセグメンテーションフォルトSMT

Question

私はZ3のJava APIを使用しています。 'SATISFIABILITY'（s.status）をチェックしている間、私はセグメンテーションフォルトを取得しています。誰かがこの問題をデバッグするのを手伝ってください。私はこの問題をデバッグできるようにメッセージをダンプする方法はありますか？私はLog.open（）を使ってみましたが、それはずっと助けになっていないようです。

ありがとうございます。

Answer 1

Log.open()は、Z3との他のやりとりを行う前に呼び出す必要があります。有効にすると、アプリケーション/入力/データ/ etcへのアクセスを必要とせずに再生できるz3.logというファイルが生成されます。

'SATISFIABILITY'もs.statusも有効なZ3/Java式ではないので、正確に何をしようとしているのかわかりません。これがZ3のバグに起因すると思われる場合は、issue trackerに新しい問題を作成してください。