How can we use xor operation on integers in z3 using python?

Question

from z3 import *
x = Int('x') #declaration
y = Int('y') #declaration
solve((x ^ y)==2) #solving

i was unable to perform xor operation in z3 using python.please help tell what is the correct way of writing if i am doing it wrong else suggest some other way of doing it.please reply as soon as possible.

Answer 1

You can use ^ on integers in Python:

>>> 2^3
1

However, z3 does not use integers, but their own Int objects, and they don't support xor. You have to use the BitVec type.

x = BitVec('x', 32)
y = BitVec('y', 32)

solve(x^y==2, show=True)