これまで学術目的に限り自由に利用できていた Z3 Theorem Prover のライセンスが変更され MIT License になりました: https://news.ycombinator.com/item?id=9272275
そのプロジェクトも Codeplex から GitHub に移行しています。
Z3 は SMT solver であり、Microsoft が開発している各種検証ツールの基盤として利用されている実用的なものです。クロスプラットフォームであり、C/C++ や .NET、Java、Python の API があります。その実装は効率を高めるための工夫が凝らされており、また quantifier を含む問題も制限付きながら扱えるそうです: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf