Encode asm into z3, then solve. Use SSA for efficiency.

Original writeup (https://github.com/perfectblue/ctf-writeups/tree/master/csaw-ctf-2018-finals/lab).