Z3 SMT的分段錯誤

Question

我正在使用Z3的Java API。在檢查'可滿足性'（s.status）時，我正在分段錯誤。有人可以幫助調試這個問題。有沒有辦法轉儲消息，以便我可以調試此問題。我嘗試使用Log.open（），但似乎沒有多大的幫助。

在此先感謝。

Answer 1

Log.open()必須在與Z3進行任何其他交互之前調用。一旦啓用，它將生成一個名爲z3.log的文件，我們可以在不需要訪問應用程序/輸入/數據/等的情況下重播。

'SATISFIABILITY'和s.status都不是有效的Z3/Java表達式，所以我不能說出你到底想要做什麼。如果您認爲這是由於Z3中的錯誤引起的，請在我們的issue tracker中創建一個新問題。