Com a interface da web z3 / python, se eu perguntar:

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

Eu agradeço:

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

Pensei que o seguinte script smt-lib2 tivesse a mesma solução:

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

Atlas, eu recebounknown com z3 (v3.2).

Suspeito que o problema esteja no termo não linear(* s0 s0), da qual a interface python de alguma forma não sofre. Existe uma maneira de codificar o mesmo no smt-lib2 para obter um modelo?