diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 2d857efea..2db4d8037 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -248,18 +248,24 @@ namespace seq {
     }
 
     bool nielsen_node::add_constraint(constraint const &c) {
-        if (graph().get_manager().is_and(c.fml)) {
+        auto& m = graph().get_manager();
+        if (m.is_and(c.fml)) {
             for (const auto f : *to_app(c.fml)) {
-                if (!add_constraint(constraint(f, c.dep, graph().get_manager())))
+                if (!add_constraint(constraint(f, c.dep, m)))
                     return false;
             }
             return true;
         }
+        expr* l, *r;
+        if (m.is_eq(c.fml, l, r)) {
+            if (l == r)
+                return true;
+        }
         m_constraints.push_back(c);
         if (m_graph.m_literal_if_false) {
             auto lit = m_graph.m_literal_if_false(c.fml);
             if (lit != sat::null_literal) {
-                set_external_conflict(lit);
+                set_external_conflict(lit, c.dep);
                 return false;
             }
         }
@@ -1762,13 +1768,13 @@ namespace seq {
                 var = r;
                 def = l;
             }
-            else if (l->is_unit() && l->arg(0)->is_var() && r->is_char_or_unit()) {
-                var = l->arg(0);
-                def = r->arg(0);
+            else if (l->is_unit() && r->is_char_or_unit()) {
+                var = l;
+                def = r;
             }
-            else if (r->is_unit() && r->arg(0)->is_var() && l->is_char_or_unit()) {
-                var = r->arg(0);
-                def = l->arg(0);
+            else if (r->is_unit() && l->is_char_or_unit()) {
+                var = r;
+                def = l;
             }
 
             if (var) {
@@ -3663,22 +3669,20 @@ namespace seq {
             if (n->m_conflict_external_literal != sat::null_literal) {
                 // We know from the outer solver that this literal is assigned false
                 deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
+                if (n->m_conflict_internal)
+                    deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
                 continue;
             }
             SASSERT(n->outgoing().empty());
             SASSERT(n->m_conflict_internal);
             deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
-            // for (str_eq const& eq : n->str_eqs())
-            //     deps = m_dep_mgr.mk_join(deps, eq.m_dep);
-            // for (str_mem const& mem : n->str_mems())
-            //     deps = m_dep_mgr.mk_join(deps, mem.m_dep);
         }
         return deps;
     }
 
 
     // NSB review: this is one of several methods exposed for testing
-    void nielsen_graph::explain_conflict(svector<enode_pair>& eqs,
+    void nielsen_graph::test_aux_explain_conflict(svector<enode_pair>& eqs,
         svector<sat::literal>& mem_literals) const {
         SASSERT(m_root);
         auto deps = collect_conflict_deps();
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 3c0a496e6..3f2c7356d 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -628,11 +628,12 @@ namespace seq {
             m_conflict_internal = confl;
         }
 
-        void set_external_conflict(sat::literal lit) {
+        void set_external_conflict(sat::literal lit, dep_tracker confl) {
             if (m_reason != backtrack_reason::unevaluated)
                 return;
             m_reason = backtrack_reason::external;
             m_conflict_external_literal = ~lit;
+            m_conflict_internal = confl;
         }
 
         bool is_progress() const { return m_is_progress; }
@@ -900,7 +901,7 @@ namespace seq {
         // explain a conflict: partition the dep_source leaves into str_eq indices
         // (kind::eq) and str_mem indices (kind::mem).
         // Must be called after solve() returns unsat.
-        void explain_conflict(svector<enode_pair> &eqs,
+        void test_aux_explain_conflict(svector<enode_pair> &eqs,
                               svector<sat::literal> &mem_literals) const;
 
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 5f04fcdf9..97e7cc019 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -735,14 +735,37 @@ namespace smt {
 
 #ifdef Z3DEBUG
 #if 1
-        std::vector<std::pair<unsigned, unsigned>> confl;
-        for (auto& lit : lits) {
-            std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n";
+        // Pass constraints to a subsolver to check correctness modulo legacy solver
+        {
+            smt_params p;
+            p.m_string_solver = "seq";
+            kernel kernel(m, p);
+
+            for (seq::dep_source const& d : m_nielsen.conflict_sources()) {
+                if (std::holds_alternative<enode_pair>(d))
+                    kernel.assert_expr(
+                        m.mk_eq(
+                        std::get<enode_pair>(d).first->get_expr(),
+                        std::get<enode_pair>(d).second->get_expr()
+                            )
+                        );
+                else
+                    kernel.assert_expr(ctx.literal2expr(std::get<sat::literal>(d)));
+            }
+            const auto res = kernel.check();
+            if (res == l_true) {
+                std::cout << "Insufficient justification:\n";
+                for (auto& lit : lits) {
+                    std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n";
+                }
+                for (auto& eq : eqs) {
+                    std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << "\n-----------\n";
+                }
+                auto dot = m_nielsen.to_dot();
+                std::cout << std::endl;
+            }
+            VERIFY(res != l_true);
         }
-        for (auto& eq : eqs) {
-            std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << "\n-----------\n";
-        }
-        std::cout << std::endl;
 #endif
 #endif
 
diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp
index 8f517b305..160a7ecd8 100644
--- a/src/test/nseq_basic.cpp
+++ b/src/test/nseq_basic.cpp
@@ -160,7 +160,7 @@ static void test_nseq_symbol_clash() {
     // verify conflict explanation returns the equality index
     smt::enode_pair_vector eqs;
     sat::literal_vector mem_idx;
-    ng.explain_conflict(eqs, mem_idx);
+    ng.test_aux_explain_conflict(eqs, mem_idx);
     SASSERT(eqs.size() == 1);
     SASSERT(eqs[0].first == nullptr);
     SASSERT(mem_idx.empty());
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 397a18f8a..c4aedffe5 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -1496,7 +1496,7 @@ static void test_explain_conflict_single_eq() {
     // but the conflict should still be detected
     svector<seq::enode_pair> eqs;
     svector<sat::literal> mem_literals;
-    ng.explain_conflict(eqs, mem_literals);
+    ng.test_aux_explain_conflict(eqs, mem_literals);
     // with test-friendly overload (null deps), eqs will be empty
     // the important check is that the conflict was detected
 }
@@ -1526,7 +1526,7 @@ static void test_explain_conflict_multi_eq() {
     // the important check is that the conflict was detected
     svector<seq::enode_pair> eqs;
     svector<sat::literal> mem_literals;
-    ng.explain_conflict(eqs, mem_literals);
+    ng.test_aux_explain_conflict(eqs, mem_literals);
 }
 
 // test that is_extended is set after solve generates extensions
@@ -2117,7 +2117,7 @@ static void test_explain_conflict_mem_only() {
     // with test-friendly overload (null deps), explain_conflict won't return deps
     svector<seq::enode_pair> eqs;
     svector<sat::literal> mem_literals;
-    ng.explain_conflict(eqs, mem_literals);
+    ng.test_aux_explain_conflict(eqs, mem_literals);
 }
 
 // test explain_conflict: mixed eq + mem conflict
@@ -2151,7 +2151,7 @@ static void test_explain_conflict_mixed_eq_mem() {
     // with test-friendly overload (null deps), explain_conflict won't return deps
     svector<seq::enode_pair> eqs;
     svector<sat::literal> mem_literals;
-    ng.explain_conflict(eqs, mem_literals);
+    ng.test_aux_explain_conflict(eqs, mem_literals);
 }
 
 // test subsumption pruning during solve: a node whose constraint set