Formal methods in software and hardware design often generate formulas that need to be
validated, either interactively or automatically. Among the automatic tools, SMT (Satisfiability
Modulo Theories) solvers are particularly suitable to discharge such proof obligations, as
their input language is equational logic with symbols from various useful decidable
fragments such as uninterpreted symbols, linear arithmetic, and usual data-structures like
arrays or lists. In this paper, we present an approach to combine decision procedures and …