Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch · Fundamenta Informaticae · 2010
We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for