定點解釋Z3

Question

當我在定點Z3Py中啓用解釋生成選項時，我得到一個包含以下消息的核心轉儲。

設置'DL_GENERATE_EXPLANATIONS'時出錯，原因：未知選項。
拋出的「z3_error」實例終止後，被稱爲中止 （核心轉儲）

我使用Z3 4.2在Ubuntu 12.04，和我在「說明」中Z3Py文檔中給出的示例中的錯誤部分。

我想知道什麼可能會導致此問題。

Answer 1

固定點引擎的選項將改變爲4.2。 該文檔適用於最新版本4.1。 您可以通過將選項直接設置到固定點對象上來將選項設置爲Z3。 這與在求解器對象和策略對象上如何管理選項類似。 例如，

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