I was checking the sort for some operations in z3py and ran into the following:
x = Int('x')
y = Int('y')
print((1 + (2 + (x*(y**2)))).sort())
which outputs
Real
Why does the type of the expression result in a Real?
It's because the ** (exponentiation) operator always returns a Real in z3, even if the arguments are integers. Note that if the second argument is negative, then the result will not be an integer.
Compare:
>>> from z3 import *
>>> x, y, z = Ints('x y z')
>>> s = Solver()
>>> s.add(And(x == 2, y == -1, z == x ** y))
>>> print(s.check())
unsat
to:
>>> from z3 import *
>>> x, y = Ints('x y')
>>> z = Real('z')
>>> s = Solver()
>>> s.add(And(x == 2, y == -1, z == x ** y))
>>> print(s.check())
sat
>>> print(s.model())
[z = 1/2, y = -1, x = 2]
If you want an integer-only producing version of exponentiation, you can code it yourself by enforcing all results to be equal to some existential Int.
Note that the power operator is usually difficult to deal with in SMT solvers due to non-linearity, and undecidable in general due to the undecidability of Diophantine equations. So unless the constraints are easy enough you'll most likely get unknown as an answer at best, or the solver will loop forever.