The Yices SMT Solver

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.

Yices is available as a free binary download for many platforms; we do not currently provide source. Here are the license terms; if you would like to discuss alternative license terms, please contact fm-licensing@csl.sri.com.

You can download Yices 1, our full-featured SMT solver, or our new Yices 2 solver.

• More Information
• Documentation
• Download Yices 1 (Updated January 8, 2013)
• Download Yices 2 (Updated August 3, 2012)
• Report a Bug
• Get Help
• Subscribe or Post to the Yices mailing lists
• Wiki
• FAQ (Frequently Asked Questions)
• Awards
• Status

Yices is one of the SRI FormalWare tools.

Last modified: Thu 10 Jan 2013 09:20 PST