If you want a fun example of using Z3, I gave a talk recently that walks you through verifying programs in a tiny little imperative language by compiling them t

If you want a fun example of using Z3, I gave a talk recently that walks you through verifying programs in a tiny little imperative language by compiling them to Z3 formulas. It's easier than it sounds! It was recorded [1] and I have example code and additional resources (papers, etc) on my site [2]. [1]: https://youtube.com/watch?v=ruNFcH-KibY https://youtube.com/watch?v=ruNFcH-KibY [2]: http://jelv.is/talks/compose-2016/ http://jelv.is/talks/compose-2016/ If you want to do more, you can extend the same process to synthesizing programs, not just verifying them. It doesn't scale too far, but otherwise it's like magic.