Home Docs Download 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.

Yices is available as a free binary download for many platforms; we do not currently provide source. 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 Download Mail Status FM Tools

Last modified: Tue 01 Apr 2014 19:56 PDT