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.

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.

• Introduction
• Documentation
• Wiki
• FAQ (Frequently Asked Questions)
• Download Yices
• Download Yices 2 (Updated April 23, 2010)
• Mailing Lists (For Announcements, Getting Help, Reporting Bugs)
• Awards
• Status

Yices is one of the SRI FormalWare tools.

Last modified: Fri 23 Apr 2010 18:52 PDT