Z3py cannot solve the power operator

Question

I'm new to Z3py, and I used the lastest z3py z3-4.4.2.4e7a867cd995-x64-win. But, I just wonder why z3py cannot solve the following code.

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

I got unknow rather than sat.

Answer 1

When x = Int('x') is changed into x = Real('x'), you can get a sat.

I think the regulation of solving an evolution equation has a rule that the type of variable should be Real.