z3py：如何在使用z3 python api時檢查跟蹤信息

Question

假設我想檢查「random_split」的跟蹤信息。我寫了

enable_trace("random_split") 

在我使用z3 python api的python腳本中，但沒有顯示出來。

我想知道如何在使用z3py時檢查跟蹤信息？

Answer 1

跟蹤僅在調試模式下可用，因此您需要使用python scripts/mk_make.py --debug自己編譯Z3。如果跟蹤沒有產生任何輸出，那麼這段代碼永遠不會到達，所以它永遠不會打印任何東西。