http://community.research.microsoft.com/blogs/z3theorem_prover/default.aspxZ3 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.enCommunityServer 2007.1 (Build: 20917.1142)http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/documentation.aspxTue, 08 Jan 2008 19:44:00 GMTeaca9afb-5ccf-4c08-b3f3-369c7e6f1a06:298Leonardo de Moura1http://community.research.microsoft.com/blogs/z3theorem_prover/rsscomments.aspx?PostID=298http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/documentation.aspx#commentsOnline 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">http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/smt-comp-2007.aspxTue, 08 Jan 2008 19:21:00 GMTeaca9afb-5ccf-4c08-b3f3-369c7e6f1a06:295Leonardo de Moura0http://community.research.microsoft.com/blogs/z3theorem_prover/rsscomments.aspx?PostID=295http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/smt-comp-2007.aspx#comments<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><img src="http://community.research.microsoft.com/aggbug.aspx?PostID=295" width="1" height="1">