Added a DEBUG flag that generates the Z3 assertions in smt2 format. Added analysis test. WIP.