Problems of Z3 (version 4.3): Output of Real value is not round automatically

2
votes

Please help me to solve this problem, I have tried various ways but not successful.

In the site: http://rise4fun.com/Z3

when solving this formula:

(declare-const a Real)
(assert (= a (/ 5 2)))
(check-sat)
(get-model)

the result is

sat
(model 
  (define-fun a () Real
    (/ 5.0 2.0))
)

The answer is (/ 5.0 2.0) which is not a round value. (I need 2.5)

In the old version of Z3 (version 3.2), with the same above formula: the answer is 2.5 (that is what I need)

Is there anyone know how to config Z3 (version 4.3) to get the same answer as its old version?

Thanks.

1
z3

1 Answers

2
votes

Please use the following code

(declare-const a Real)
(assert (= a (/ 5 2)))
(check-sat)
(set-option :pp-decimal true)
(get-model)

and the output is

sat 
(model 
  (define-fun a () Real 
  2.5) 
)