z3 - Z3：具有 Reals 的模型

Question

对于这个基准：

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

我越来越：

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

这是一个已知的问题？（这是在 Linux 和 Mac 上使用 Z3 V3.2。）

Answer 1

是的，这是模型生成器中的一个错误。该错误已得到修复。该错误可以避免使用

(set-option :auto-config false)

如果 Z3 在无量词问题上变得太慢，那么我们也可以添加

(set-option :relevancy 0)