z3 / python реал

Question

С веб-интерфейсом z3 / python, если я спрашиваю:

x = Real ('x')
solve(x * x == 2, show=True)

Я хорошо получаю:

Problem:
[x·x = 2]
Solution:
[x = -1.4142135623?]

Я думал, что следующий скрипт smt-lib2 будет иметь такое же решение:

(set-option :produce-models true)
(declare-fun s0 () Real)
(assert (= 2.0 (* s0 s0)))
(check-sat)

Увы, я получаю unknown с z3 (v3.2).

Я подозреваю, что проблема связана с нелинейным термином (* s0 s0), от которого интерфейс Python почему-то не страдает. Есть ли способ кодировать то же самое в smt-lib2, чтобы получить модель?

Answer 1

Попробуйте ваш пример с веб-интерфейсом Z3, я получаю результат sat.

Веб-интерфейс Z3 и Z3Py основаны на Z3 v4.0, поэтому я думаю, что проблема будет исправлена ​​в следующем выпуске.