#!/usr/bin/env python3

from z3 import *

init_X, init_Y=BitVecs('init_X init_Y', 32)

X, Y=init_X, init_Y

X=X^Y
Y=Y^X
X=X^Y

print ("X=", simplify(X))
print ("Y=", simplify(Y))