Oh yeah? Well, take a look at this.
http://llvmweekly.org/issue/65The Z3 theorem prover from Microsoft Research is now on Github, and more importantly now released under the MIT license. This is a true open source license allowing commercial use, unlike the previous non-commercial use only license. It's been used with LLVM in the ALIVe project. Work has already begun to integrate it directly into LLVM.