\myheading{XOR swapping algorithm}

\leveldown{}

This is well-known XOR swap algorithm (which don't use additional variable).
How it works?

\lstinputlisting[numbers=left,style=custompy]{proofs/xor_swap_Z3_check.py}

Now we see a final states of X/Y variables:

\begin{lstlisting}
X= init_X ^ init_Y ^ init_Y ^ init_X ^ init_Y
Y= init_Y ^ init_X ^ init_Y
unsat
\end{lstlisting}

Z3 gave "unsat", meaning, it can't find any counterexample to the last equation (line 18).
Hence, the equation is correct and so is the whole algorithm.

\myheading{In SMT-LIB form}

\lstinputlisting[style=customsmt]{proofs/XOR_swap.smt}

\lstinputlisting[style=customsmt]{proofs/XOR_swap2.smt}

\levelup{}