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