| Home | • | Intro | • | Docs | • | Wiki | • | FAQ | • | Download | • | • | Awards | • | Status | • | FM Tools |
|---|
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:
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.
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 | • | • | Awards | • | Status | • | FM Tools |
|---|
Last modified: Mon 23 Nov 2009 18:59 PST