Merging interpretations of types may result in unsat

[JoD]

Given two structures over the same vocabulary, with disjunctively interpreted types, it may occur that an unsatisfiable function symbol becomes satisfiable after merging the structures. Currently, the function remains satisfiable.

Example in attachment.