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.
Yices is open source software distributed under the GPLv3 license. The Yices source is available on GitHub. To discuss alternative license terms, please contact firstname.lastname@example.org.
You can install Yices with homebrew on Mac OS X or with apt or aptitude on Debian/Ubuntu Linux. We also kindly 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.4. It was released on 2021-10-22.
Older versions of Yices can be downloaded here.
We no longer maintain Yices 1 but you can still download it here and the old documentation is 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.