Converting to "set-option" SMTLib format

Question

I want to convert this z3py code (online code) to standard SMTLib format. Everything is converted to SMTLib format except the set options properties "(set-option :produce-models true) (set-option :timeout 4000)". Why isn't working? The conversion code was suggested by Leonardo de Moura.

I want output to be like -

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

Thanks

Answer 1

I am running your code and I am obtaining

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

Answer 2

Options are not printed by the SMT-LIB2 pretty printer. The pretty printer returns a string and you should be able to pre-pend options of your choice.