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 email@example.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.