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 firstname.lastname@example.org.
You can download Yices 1, our full-featured SMT solver, or our new Yices 2 solver.
Yices is one of the SRI FormalWare tools.