Z3 is a new high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 has already been integrated with Spec#/Boogie, and HAVOC. We are currently integrating Z3 with Pex, SAGE, Yogi, Vigilante, and SLAM. It can read problems in SMT-LIB and Simplify formats.http://community.research.microsoft.com/blogs/z3theorem_prover/atom.aspxCommunity Server2008-01-08T14:21:00Z/blogs/z3theorem_prover/archive/2008/01/08/documentation.aspx2008-01-08T20:44:00Z2008-01-08T20:44:00ZOnline documentation: http://research.microsoft.com/projects/z3/documentation.html FAQ: http://research.microsoft.com/projects/z3/faq.html...(<a href="http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/documentation.aspx">read more</a>)<img src="http://community.research.microsoft.com/aggbug.aspx?PostID=298" width="1" height="1">Leonardo de Mourahttp://community.research.microsoft.com/members/Leonardo-de-Moura/default.aspx/blogs/z3theorem_prover/archive/2008/01/08/smt-comp-2007.aspx2008-01-08T20:21:00Z2008-01-08T20:21:00Z<p>Z3 did very well in the recent <a class="external text" title="http://www.smt-comp.org" href="http://www.smt-comp.org/" rel="nofollow">2007 SMT Competition</a>: it won&nbsp;4 divisions and took 7 second places.</p><div style="clear:both;"></div><img src="http://community.research.microsoft.com/aggbug.aspx?PostID=295" width="1" height="1">Leonardo de Mourahttp://community.research.microsoft.com/members/Leonardo-de-Moura/default.aspx