For one example of why Z3 is cool, check out this application to "peephole" compiler optimizations: http://blog.regehr.org/archives/1170 http://blog.regehr.org/

For one example of why Z3 is cool, check out this application to "peephole" compiler optimizations: http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170 Also take a look at the "licensing" section to see why switching to the MIT license is a big deal. Even open source software projects like LLVM have had to worry about whether using Z3 was OK or not. Now they don't any more!