Yices is a high-performance SMT solver developed at SRI International. Yices decides the satisfiability of propositional formulas that mix uninterpreted function symbols and equality with interpreted symbols from the following theories:
Yices also does MaxSMT (given an unsatisfiable set of weighted clauses, find the satisfiable subset of maximum weight); dually, it can find the unsat core (the set of unsatisfiable clauses of minimum weight).
The Yices input language is similar to the SAL languages. Yices also accepts specifications written in the SMT-LIB language. Yices can be used as a regular SAT solver and can read boolean problems in the CNF DIMACS format.
Yices can also be used as a library in other applications. A light-weight API is provided for this purpose. A richer API is under construction.
ICS was the first SMT solver developed at SRI International. Until recently, ICS2.0 was the default backend solver used by the SAL infinite-state bounded model checker.
ICS has several inefficiencies and performance limitations and it should no longer be considered state-of-the-art. We do not maintain or develop ICS anymore, but ICS 2.0 can still be downloaded at http://ics.csl.sri.com.
In 2005, we implemented from scratch two new prototype SMT solvers that greatly outperformed ICS. Both solvers participated in the SMT-COMP05 competition associated with CAV 2005.
Based on our experiments with Yices 0.1 and Simplics, we
reimplemented a new SMT solver from scratch, with a new architecture
and more efficient solvers. This new SMT solver is
Although Yices is better than ICS in most dimensions (it has a richer input language with records, dependent typing and subtyping, and it provides more complete and vastly faster automation), Yices does lack some of ICS' capabilities: Yices does not include a canonizer, it does not have applicative state (only push/pop and assert/retract), and it does it offer a capability for displaying and querying its internal state. It remains to be seen whether these lacks are significant in practice.