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 version 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.

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: Tue 05 Aug 2014 17:20 PDT