We explore automated reasoning techniques for the non-disjoint combination of theories that share set variables and operations. We are motivated by applications to software analysis, where verification conditions are often expressed in a combination of such theories. The standard Nelson-Oppen result on combining theories does not apply in this setting, because the theories share more than just equalities. We state and prove a new combination theorem and use it to show the decidability of the satisfiability problem for a class of formulas obtained by applying propositional connectives to formulas belonging to:

• Boolean algebra with Presburger arithmetic (with quantifiers over sets and integers)
• weak monadic second-order logic over trees (with first and second order quantifiers)
• two-variable logic with counting quantifiers
• the Bernays-Schönfinkel-Ramsey class of first-order logic with equality (with ∀^* ∃^* quantifier prefix)
• the quantifier-free logic of multisets with cardinality constraint We illustrate our result through verification conditions expressing properties of data structures.

This is a joint work with Thomas Wies and Viktor Kuncak.