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.
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.