Authors: Dejan Jovanovic and Clark Barrett

Title:Sharing is Caring: Combination of the Theories 

One of the main shortcomings of the traditional methods for combining theories is the
complexity of guessing the arrangement of the variables shared by the individual theories. This paper
presents a reformulation of the Nelson-Oppen method that takes into account explicit equality prop-
agation and can ignore pairs of shared variables that the theories do not care about. We show the
correctness of the new approach and present care functions for the theory of uninterpreted functions
and the theory of arrays. The effectiveness of the new method is illustrated by experimental results
demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.