Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic.
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. You can also use Yices 2 as a library in your software.
You can download the source or precompiled binaries for common operating systems. Yices is free for non-commercial use. You can check the license terms here. If you would like to discuss alternative license terms, please contact firstname.lastname@example.org.
The current version is Yices 2.5.2. It was released in February 2017.
Older versions of Yices can be downloaded here.
Yices 2 is developed by SRI International's Computer Science Laboratory. The development of Yices has been funded by SRI International, the National Science Foundation, the National Aeronautics and Space Administration, and the Defense Advanced Research Projects Agency.
SRI International distributes other formal method tools that you may find useful.