Z3py解不出功率算子

Question

我是Z3py的新手，我使用了最新的z3py z3-4.4.2.4e7a867cd995-x64-win。但是，我只是想知道为什么z3py不能解决下面的代码。

from z3 import *
x = Int('x')
s = Solver()
s.add(x**2 == 4)
print s.check()

我不知道而不是坐着。

Answer 1

当x = Int('x')被转换为x = Real('x')时，您可以得到一个sat。

我认为解演化方程的规则是，变量的类型应该是Real。