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

我得到的是 unknow 而不是 sat。

Answer 1

当x = Int('x') 变成x = Real('x') 时，你可以得到一个sat。

我认为求解进化方程的规则有一个规则，变量的类型应该是Real。