Being polite is not enough (and other limits of theory combination)

Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar

In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and th…