Z3: models with Reals

Question

For this benchmark:

(set-option :produce-models true)
(declare-fun s0 () Real)
(declare-fun s1 () Real)
(assert (> s0 s1))
(check-sat)
(get-value (s0))
(get-value (s1))

I'm getting:

sat
((s0 0.0))
((s1 0.0))

Is this a known issue? (This is using Z3 V3.2 both on Linux and Mac.)

Answer 1

Yes, this was a bug in the model generator. The bug has been fixed. The bug can be avoided using

(set-option :auto-config false)

If Z3 becomes too slow in quantifier free problems, then we can also add

(set-option :relevancy 0)