how can I change get-model or get-value output to print decimals instead of fractions

z3

Solution

Please use the command

(set-option :pp.decimal true)

Please look the following example

(declare-const t Real)
(assert (= t (/ 1.0 2.0)))
(check-sat)
(set-option :pp.decimal true)
(get-model)
(get-value (t))

and the corresponding output is

sat (model (define-fun t () Real 0.5) )
((t 0.5))

Problem

When solving using SMTLIB2 files, if I call get-model or get-value everything is printed as fractions. Is there an easy way to get Z3 to print the decimal values? For example, `(get-value t)` might output `((t (/ 1.0 2.0)))`, whereas I would prefer something like `((t 0.5))`.

Original source