Over the years SMT, Satisfiability Modulo Theories, has become more prevalent in usage on finding flaws and exploitable conditions. I want to show the audience how I used SMT libraries, mostly z3, to do what took weeks using pencil and paper….and of course, Calc.exe.