Yices: An 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.

• Introduction
• Documentation
• Wiki
• FAQ (Frequently Asked Questions)
• Download
  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.
• Mailing Lists and Bug Reports
• Awards
• Status

Yices is one of the SRI FormalWare tools.

Last modified: Tue 06 Oct 2009 17:46 PDT