title: How can we use xor operation on integers in z3 using python?
body: <pre><code>from z3 import *
  x = Int('x') #declaration
  y = Int('y') #declaration
  solve((x ^ y)==2) #solving
  </code></pre>
  
  <p>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.</p>