An interactive development environment for SMT-LIB files and Z3. Z3 and Contessa as well as various SMTLIB supporting theorem provers & solvers are supported. Structured statements can be inserted and ran with C-c