Home	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	•	Mail	•	Awards	•	Status	•	FM Tools

Download Yices 2

Modulo a few bug fixes, this is the Yices 2 prototype that entered the Satisfiability Modulo Theory Competition in August 2009.

This prototype reads an input specification in the SMT-LIB format and prints sat or unsat on standard output. Optionally, it can also print a model if the input is satisfiable.

We distribute Yices 2 as a free binary, under the following license terms. If you would like to discuss alternative license terms, contact fm-licensing@csl.sri.com

Yices 2 is distributed as a gzipped tarfile for a variety of systems. Yices 2 uses the GNU Multiprecision library (GMP). You can choose a distribution with GMP either statically or dynamically linked. The statically linked versions are recommended.

To download Yices 2:

Select the distribution you want. This will open a web page showing the license terms.
If you agree with the license terms, click on the accept button to start downloading the tarfile.

Yices 2 with GMP statically linked

The following distributions are statically linked against GMP.

Yices 2 without GMP

To use the following distributions, you must have the GMP library installed on your machine as a dynamically loadable library. See the GMP website for instructions on how to build and install GMP.

Getting Help

If the versions above do not work for your OS or hardware, send an e-mail to yices-sri@csl.sri.com

Send bug reports to yices-bugs@csl.sri.com

For other issues, check the Yices Frequently Asked Questions or send an e-mail to yices-help@csl.sri.com

Home	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	•	Mail	•	Awards	•	Status	•	FM Tools

Last modified: Mon 23 Nov 2009 18:59 PST