Z3：型号雷亚尔

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)