The Nuts and Bolts of Yices
                                       Bruno Dutertre
                                  Computer Science Laboratory
                                       SRI International
                                   Bruno.Dutertre@sri.com



                                          Abstract

    At a high-level, the architecture of many SMT solvers is well known. It is the combination of
a SAT solver and one or more decision procedures called theory solvers. But how to effectively
implement such a combination is rarely discussed in the literature. This talk will focus on
implementation issues. We will discuss the practical integration of CDCL-based SAT solvers
and theory solvers. We will present data structures and algorithms employed by the Yices SMT
solver, and examine preprocessing and formula simplification, which have a significant impact
on a solver’s performance.
    Yices is developed and distributed by SRI International. It is free for non-commercial use.
Source and binaries are available at http://yices.csl.sri.com.




                                                                                               1