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

Это известная проблема? (Это использует Z3 V3.2 как на Linux, так и на Mac.)

Answer 1

Да, это была ошибка в модели генератора.Ошибка была исправлена.Эту ошибку можно избежать, используя

(set-option :auto-config false)

Если Z3 становится слишком медленным в задачах, свободных от квантификаторов, то мы также можем добавить

(set-option :relevancy 0)