Navigating the Universe of Z3 Theory Solvers.

Modular combination of theory solvers is an integral theme in engineering modern SMT solvers. The CDCL(T) architecture provides an overall setting for how theory solvers may cooperate around a SAT solver based on conflict driven clause learning. The Nelson-Oppen framework provides the interface contracts between theory solvers for disjoint signatures. This paper provides an update on theories integrated in Z3. We briefly review principles of theory integration in CDCL(T) and then examine the theory solvers available in Z3, with special emphasis on two recent solvers: a new solver for arithmetic and a pluggable user solver that allows callbacks to invoke propagations and detect conflicts.