Computing weakest precondition of Imp programs directly in Z3. Requires reflection of smtlib expressions into expression datatypes and representing the variable store as an array. In principle, smtlib is it's own macro system.
Typically people use python or some other language to generate smtlib. Boogie and Why3 are frameworks that generate smtlib (among other things) from imperative code. We can remove one level of indirection by directly programming in Z3. There are so many other good abstractions that smtlib is just barely able to express in this style.