The Yices SMT Solver

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 fm-licensing@csl.sri.com.

Downloads

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

Latest Release

The current version is Yices 2.6.5. It was released on 2024-06-24.

• Documentation
• Release notes
• Source Code
• Binaries
  • Linux (64 bits) AMD/Intel
  • Mac OS X (64 bits) Intel Apple-Silicon
  • Windows (64 bits)

Previous Releases

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.

Contact Us

• Get Help
• Report a Bug
• Subscribe or Post to the Yices mailing lists

Acknowledgements

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.