轉換爲「set-option」SMTLib格式

Question

我想將此z3py代碼（online code）轉換爲標準SMTLib格式。除設置選項屬性「（set-option：produce-models true）（set-option：timeout 4000）」之外，所有內容都轉換爲SMTLib格式。爲什麼不工作？轉換代碼由Leonardo de Moura提出。

我想輸出到像 -

; benchmark 
(set-info :status unknown) 
(set-option :produce-models true) 
(set-option :timeout 4000) 
(set-logic QF_UFLIA) 
(assert true) 
(check-sat) 

感謝

Answer 1

我運行你的代碼，我獲得

; benchmark 
(set-info :status unknown) 
(set-logic QF_UFLIA) 
(assert true) 
(check-sat) 

Answer 2

選項不是由SMT-LIB2漂亮的打印機打印。 美麗的打印機返回一個字符串，你應該能夠預先選擇你所選擇的選項。