I've read Chapter 10 from (https://www.decision-procedures.org/) and come up with a question of Nelson-Oppen combination under a specific situation (I'll try to state the question w.r.t. the definitions from the book):
Consider the combination of two theories, T_1 and T_2, where V is the set of shared variables, and a constant symbol is a (nonlogical) function symbol with arity 0.
After the purification step, F_1 is the conjunction of T_1-literals and F_2 is the conjunction of T_2-literals.
Then think of a situation that F_1 implies v_1=v_2=x, and F_2 implies v_1=v_2=y, but x ≠ y.
(v_1, v_2 belong to V, x is a constant symbol of T_1, and y is a constant symbol of T_2.
Based on my understanding, Nelson-Oppen combination only propagates equalities between shared variables(v_1, v_2) and does not detect the situation which causes inconsistent.
So, my question is: Does Nelson-Oppen combination prevent or deal with this situation?
Also, I couldn't think of a case using the combination of theories introduced in the book (such as the theory of linear arithmetic, equality and uninterpreted functions, arrays). I'm wondering if this situation actually happens or there is just something that I misunderstand.