Yices is a decision procedure developed at SRI International that decides formulas in a combination of useful theories. Yices decides the satisfiability of formulas in a quantifier-free, first-order theory containing both uninterpreted function symbols and interpreted symbols from a rich combination including: real and integer arithmetic, recursive datatypes, tuples/records, extensional arrays, and lambda expressions. Yices supports a richer input language similar to the SAL language. Dependent types are also supported, since we found them to be useful for specifying properties of uninterpreted function symbols.

Yices got the first place in the QF_LIA (linear integer arithmetic) and QF_AUFLIA (arrays, uninterpreted functions, and linear integer arithmetic) divisions, and the second place in all other divisions in SMT-COMP'05.

yices website