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 2008.5 SP1 (Build: 31106.3070)http://community.research.microsoft.com/blogs/z3theorem_prover/archive/2008/01/08/documentation.aspx#2232Mon, 14 Jul 2008 08:19:44 GMTeaca9afb-5ccf-4c08-b3f3-369c7e6f1a06:2232pmatos<p>I am wondering which languages are being used to implement Z3? It seems it nowhere in the site or in the FAQ. Thanks!</p> <div style="clear:both;"></div><img src="http://community.research.microsoft.com/aggbug.aspx?PostID=2232" width="1" height="1">