\myheading{Simplifying long and messy expressions using Z3}
\renewcommand{\CURPATH}{proofs}

SMT solvers can optimize whatever you give them at input, and the results of that step can be obtained at the \ac{API} side.

\lstinputlisting[style=custompy]{\CURPATH/simp.py}

\lstinputlisting[style=custompy, caption=The result]{\CURPATH/simp.txt}

Sometimes, that step is used by all sorts of code deobfuscation tools...

Another interesting tool I used is \texttt{BooleanMinimize} function in Wolfram Mathematica
\footnote{\url{https://reference.wolfram.com/language/ref/BooleanMinimize.html}}.