# Is stable infinity required of theories combined with model-based theory combination?

In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen combination method, which requires that the two theories being combined are 1) disjoint and 2) stably infinite. Then they describe model-based theory combination. Paraphrasing the intro of section 4:

Our approach minimizes the number of produced shared equalities. It is based on the fact that, in practice, the number of local inconsistencies is much bigger than the number of global (cross theory) inconsistencies. It works for convex and non-convex theories alike.

As stable infinity is not mentioned at all, I am inclined to believe that model-based theory combination can also combine non-stably infinite theories. Also the more detailed paragraphs after this do not mention stable infinity.

Empirically, this makes sense. Their SMT solver that implements this approach (Z3) supports bools as a value type. Booleans are effectively a bit vector of width one, and as the theory of bit vectors is the common example of a non-stably-infinite theory, supporting booleans means supporting & combining (at least one) non-stably infinite theory with other stably infinite theories.

If anyone can clarify, confirm, or falsify part of my explanation that'd be very appreciated! Because at the moment I'm stumped as to why stable infinity seems to be such an important requirement, while there is no source explaining how to deal with the finiteness of the boolean sort.

(I asked a relevant though different question here: 2. Since I cannot find a definition of stable infinity for many-sorted first order logic, I figured it's probably best to just ask about a clarification about an existing paper, than to further convolute my already existing question.)

Essentially, I perceive the trick here to be that you add type information to all axioms. Then, it is safe to extend any interpretation found with infinite domains with elems that do not satisfy e.g. the is-bv predicate. I'm assuming Z3 uses this trick to support non-stably infinite theories; whether this implies that model-based theory combination does or does not rely on stable infinity, is not yet clear.