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。