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 use

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 http://jelv.is/chlorophyll.pdf [2]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-overview-notes.pdf http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-...