I'm not pavpanchekha, but I worked on a project[1] that used Z3 to optimize array-forth code without having to implement a classical optimizing compiler. We used Z3 to synthesize basic blocks of array-forth code against an executable specification which involves verifying that two programs have the same behavior and actually searching for programs against certain constraints.

There is a whole field of research in program synthesis, much of which can be done efficiently on theorem-provers like Z3. You can read these slides[2] for a good overview.

[1]: http://jelv.is/chlorophyll.pdf

[2]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-...