Home Docs Mail Status FM Tools

The Yices SMT Solver

Yices 2 is an efficient SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, bitvectors, scalar types, and tuples.

Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported).

Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types.

Yices 2 can also be used as a library in other software.

You can download the source or precompiled binaries for common operating systems. Yices is free for non-commercial use. Here are the license terms; if you would like to discuss alternative license terms, please contact fm-licensing@csl.sri.com.

The current release is Yices 2.2.2 (released August 6, 2014)

Our older solver Yices 1 is no longer maintained, but you can still download it here and the old documentation is here.

Yices is one of the SRI FormalWare tools.

Home Docs Mail Status FM Tools

Last modified: Thu 04 Sep 2014 11:04 PDT