Con la interfaz web z3 / python, si pregunto:

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

Me encanta:

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

Pensé que el siguiente script smt-lib2 tendría la misma solución:

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

Alas, consigounknown con z3 (v3.2).

Sospecho que el problema es con el término no lineal(* s0 s0), que la interfaz de Python de alguna manera no sufre. ¿Hay alguna manera de codificar lo mismo en smt-lib2 para obtener un modelo?