Z3 Solver aids in simplifying deobfuscation techinques. This post covers 2 example use cases where a convoluted string decryption routine is broken down and simplified into a single XOR operation. Z3 is used to prove that the extra parts of the decryption routine cancel each other out.