z3 - 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)