**Challenge** circuit123

sploit.py generates all the z3 rules to solve this challenge.
z3_rules.py contains all the rules and gets us the flag.

Original writeup (https://github.com/twisted-fun/CTFs/tree/master/PICO18/REV_800).