diff --git a/examples/python/union_sort.py b/examples/python/union_sort.py
new file mode 100644
index 000000000..5a609d6cd
--- /dev/null
+++ b/examples/python/union_sort.py
@@ -0,0 +1,20 @@
+# Copyright Microsoft Corporation 2019
+# This example illustrates the use of union types
+# from the Python API. It is given as an example
+# as response to #2215.
+
+from z3 import *
+
+u = Datatype('IntOrString')
+u.declare('IntV', ('int', IntSort()))
+u.declare('StringV', ('string', StringSort()))
+IntOrString = u.create()
+StringV = IntOrString.StringV
+IntV = IntOrString.IntV
+
+print(IntV(1))
+print(StringV(StringVal("abc")))
+print(IntV(1).sort())
+print(IntV(1) == StringV(StringVal("abc")))
+s = String('s')
+print(simplify(IntV(1) == StringV(s)))
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a40efe228..a5c722d4b 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1330,10 +1330,11 @@ namespace smt {
         for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
             new_eq & entry = m_eq_propagation_queue[i];
             add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
-            if (inconsistent())
+            if (inconsistent()) {
+                m_eq_propagation_queue.reset();
                 return false;
+            }
         }
-        TRACE("add_eq", tout << m_eq_propagation_queue.size() << " " << i << "\n";);
         m_eq_propagation_queue.reset();
         return true;
     }
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index 9dcc7afad..d7ba74a87 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -162,6 +162,10 @@ namespace smt {
         for (auto const& kv : m_relations) {
             if (extract_equalities(*kv.m_value)) {
                 new_equality = true;
+                //return FC_CONTINUE;
+            }
+            if (get_context().inconsistent()) {
+                return FC_CONTINUE;
             }
         }
         if (new_equality) {
@@ -322,7 +326,9 @@ namespace smt {
         ast_manager& m = get_manager();
         (void)m;
         r.m_graph.compute_zero_edge_scc(scc_id);
-        for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) {
+        int start = ctx.get_random_value();
+        for (unsigned idx = 0, j = 0; !ctx.inconsistent() && idx < scc_id.size(); ++idx) {
+            unsigned i = (start + idx) % scc_id.size();
             if (scc_id[i] == -1) {
                 continue;
             }
@@ -336,8 +342,10 @@ namespace smt {
                     r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r);
                     r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r);
                     literal_vector const& lits = r.m_explanation;
-                    TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << " ", lits) << "\n";);
-                    eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr())));
+                    TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n", lits) << "\n";);
+                    IF_VERBOSE(20, ctx.display_literals_verbose(verbose_stream() << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n", lits) << "\n";);
+                    eq_justification js(ctx.mk_justification(ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, nullptr, 
+                                                                                                     x, y)));
                     ctx.assign_eq(x, y, js);
                 }
             }