python - 固定点Z3での説明

Question

固定ポイントZ3Pyで説明生成オプションを有効にすると、次のメッセージを含むコアダンプが表示されます。

'DL_GENERATE_EXPLANATIONS'の設定エラー、理由：不明なオプション。
'z3_error'のインスタンスをスローした後に呼び出された終了中止（コアダンプ）

Ubuntu12.04でZ34.2を使用していますが、「説明」セクションのZ3Pyドキュメントに記載されている例のエラーが発生します。

何がこの問題を引き起こしているのだろうかと思います。

Answer 1

固定小数点エンジンのオプションは、4.2で変更される予定です。ドキュメントは最後のリリース4.1のものです。オプションを固定小数点オブジェクトに直接設定することにより、オプションをZ3に設定できます。これは、ソルバーオブジェクトと戦術オブジェクトでオプションを管理する方法に似ています。例、

fp = Fixedpoint()
fp.set(engine='datalog',generate_explanations=True)

Answer 2

上記は私にはうまくいきませんでした。私が使用した：

fp.set('datalog.generate_explanations', True)

z34.8.5pythonパッケージを使用します。