Search code examples
pythonintegerz3smtz3py

z3.z3types.Z3Exception: Z3 integer expression expected

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * y ** 3 + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + x ** 3) % 11223344 == 33445566)

Upon running s.check(), z3 throws an error z3.z3types.Z3Exception: Z3 integer expression expected. I do not understand why as everything I used is an integer. I also tried BitVector however that gave a different error: unsupported operand type(s) for ** or pow(): 'BitVecRef' and 'BitRefValue'

I'm sorry that I could not provide the actual values here as it is sensitive data - but I simply replaced integer values and kept everything else the same.

Solution

  • In z3, power operator always returns a Real value. Which makes your arithmetic use mixed-types, and z3 rightfully complains.

    There's a very recent discussion of this on stack-overflow, see here: Why does the type change to Real in z3 python?

    You can avoid the issue by casting to integer explicitly:

    from z3 import *

x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * ToInt(y ** 3) + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + ToInt(x ** 3)) % 11223344 == 33445566)

    The above goes through without any complaints.

    However, keep in mind the caveats that come with using the power-operator in the linked answer. If you're always raising to the third power, I'd recommend simply writing x * x * x (or define a function that does that for you). Your problem will still be non-linear, but at least you'll avoid the issues due to the further complexity of exponentiation.