Home Intro Docs Wiki FAQ Download - Mail Awards Status FM Tools
Yices

Yices: An SMT Solver


 *NEW* Download Yices 2, the SMT solver we entered in SMT-COMP 09  *NEW*

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 one of the SRI FormalWare tools.

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

Last modified: Tue 06 Oct 2009 17:46 PDT