CODEWITHSUNDEEP
z3z3py
Kun
Kun

Reputation: 101

Z3py cannot solve the power operator

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.

Upvotes: 0

Views: 526

Answers (1)

yjgong
yjgong

Reputation: 11

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.

Upvotes: 0

Related Questions