Home • Docs • Download • Mail • FAQ • Awards • Status • MSR

Z3 An Efficient SMT Solver

Introduction

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 is still under development, but it has already been integrated with Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, and HAVOC. It can read problems in SMT-LIB and Simplify formats.

Links:

Last modified Tue Jul 8 06:37:26 2008