I thought SMT2 (what you can feed to z3 -smt2), is a s-expression language that is the lowest level ("bytecode") thing. If you look at Dafny/Boogie, boogie is a

I thought SMT2 (what you can feed to z3 -smt2), is a s-expression language that is the lowest level ("bytecode") thing. If you look at Dafny/Boogie, boogie is a much more human readable IR. I'm trying to build a pythonic variant of Boogie. https://github.com/adsharma/py2many/blob/main/tests/cases/demorgan.py https://github.com/adsharma/py2many/blob/main/tests/cases/de...