CODEWITHSUNDEEP
z3z3py
user1770051
user1770051

Reputation: 149

Converting to "set-option" SMTLib format

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

Upvotes: 0

Views: 754

Answers (2)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

Upvotes: 1

Juan Ospina
Juan Ospina

Reputation: 1347

I am running your code and I am obtaining

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

Upvotes: 0

Related Questions