The YICES SMT Solver

TLDR

SMT (Satisfiability Modulo Theories) solves the satisfiability of complex formulas in theories such as arithmetic and uninterpreted functions, and is widely used in theorem proving, hardware/software verification, and scheduling. This paper describes Yices, an efficient SMT solver developed at SRI International. Yices supports a rich combination of first‑order theories—including arithmetic, uninterpreted functions, bit vectors, arrays, and recursive datatypes—and also handles weighted MAX‑SMT, unsatisfiable core extraction, and model construction. Yices serves as the primary decision procedure for the SAL model‑checking environment, is integrated into the PVS theorem prover, and powers the probabilistic consistency engine of SRI’s CALO system as a MAX‑SMT solver.

Abstract

SMT stands for Satisfiability Modulo Theories. An SMT solver decides the satisfiability of propositionally complex formulas in theories such as arithmetic and uninterpreted functions with equality. SMT solving has numerous applications in automated theorem proving, in hardware and software verification, and in scheduling and planning problems. This paper describes Yices, an efficient SMT solver developed at SRI International. Yices supports a rich combination of first-order theories that occur frequently in software and hardware modeling: arithmetic, uninterpreted functions, bit vectors, arrays, recursive datatypes, and more. Beyond pure SMT solving, Yices can solve weighted MAX-SMT problems, compute unsatisfiable cores, and construct models. Yices is the main decision procedure used by the SAL model checking environment, and it is being integrated to the PVS theorem prover. As a MAX-SMT solver, Yices is the main component of the probabilistic consistency engine used in SRI’s CALO system.