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 install Yices with homebrew on Mac OS X or with apt or aptitude on Debian/Ubuntu Linux. We also provide precompiled binaries of the latest stable release below.
On Ubuntu or Debian:
sudo add-apt-repository ppa:sri-csl/formal-methods sudo apt-get update sudo apt-get install yices2
On Mac OS X:
brew install SRI-CSL/sri-csl/yices2
The current version is Yices 2.6.2. It was released on 2020-04-06.
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.