diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 43e5e3b03..086eecc79 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -250,9 +250,8 @@ namespace seq {
 
     bool nielsen_node::add_constraint(constraint const &c) {
         if (graph().get_manager().is_and(c.fml)) {
-            for (auto f : *to_app(c.fml)) {
-                if (!add_constraint(constraint(f, c.dep, graph().get_manager())))
-                    return false;
+            for (const auto f : *to_app(c.fml)) {
+                add_constraint(constraint(f, c.dep, graph().get_manager()));
             }
             return true;
         }
@@ -1432,6 +1431,9 @@ namespace seq {
         generate_node_length_constraints(node);
         assert_node_new_int_constraints(node);
 
+        if (node->is_currently_conflict())
+            return search_result::unsat;
+
         // integer feasibility check: the solver now holds all path constraints
         // incrementally; just query the solver directly
         if (!cur_path.empty() && !check_int_feasibility()) {
@@ -1443,6 +1445,7 @@ namespace seq {
         }
 
         SASSERT(sr != simplify_result::satisfied || node->is_satisfied());
+        SASSERT(!node->is_currently_conflict());
 
         if (node->is_satisfied()) {
             // Before declaring SAT, check leaf-node regex feasibility:
@@ -1464,6 +1467,8 @@ namespace seq {
         if (depth >= m_depth_bound)
             return search_result::unknown;
 
+        SASSERT(!node->is_currently_conflict());
+
         // generate extensions only once per node; children persist across runs
         if (!node->is_extended()) {
             bool ext = generate_extensions(node);
@@ -1474,6 +1479,8 @@ namespace seq {
             ++m_stats.m_num_extensions;
         }
 
+        SASSERT(!node->is_currently_conflict());
+
         // explore children
         bool any_unknown = false;
         for (nielsen_edge *e : node->outgoing()) {
@@ -1493,8 +1500,7 @@ namespace seq {
                 e->set_len_constraints_computed(true);
 
                 for (const auto& sc : e->side_constraints()) {
-                    if (!e->tgt()->add_constraint(sc))
-                        return search_result::unsat;
+                    e->tgt()->add_constraint(sc);
                 }
             }
 
@@ -1556,12 +1562,10 @@ namespace seq {
                 while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) {
                     euf::snode* lt = lhs_toks[prefix];
                     euf::snode* rt = rhs_toks[prefix];
-                    if (m.are_equal(lt->get_expr(), rt->get_expr())) {
+                    if (m.are_equal(lt->get_expr(), rt->get_expr()))
                         ++prefix;
-                    }
-                    else if (m_sg.are_unit_distinct(lt, rt)) {
+                    else if (m_sg.are_unit_distinct(lt, rt))
                         break;
-                    }
                     else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
                         nielsen_node* child = mk_child(node);
                         nielsen_edge* e = mk_edge(node, child, true);
@@ -1579,6 +1583,8 @@ namespace seq {
                         eqs[eq_idx] = eqs.back();
                         eqs.pop_back();
 
+                        if (lt->is_char())
+                            std::swap(lt, rt);
                         nielsen_subst subst(lt, rt, eq.m_dep);
                         e->add_subst(subst);
                         child->apply_subst(m_sg, subst);
@@ -1597,12 +1603,10 @@ namespace seq {
                 while (suffix < lsz - prefix && suffix < rsz - prefix) {
                     euf::snode* lt = lhs_toks[lsz - 1 - suffix];
                     euf::snode* rt = rhs_toks[rsz - 1 - suffix];
-                    if (m.are_equal(lt->get_expr(), rt->get_expr())) {
+                    if (m.are_equal(lt->get_expr(), rt->get_expr()))
                         ++suffix;
-                    }
-                    else if (m_sg.are_unit_distinct(lt, rt)) {
+                    else if (m_sg.are_unit_distinct(lt, rt))
                         break;
-                    }
                     else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
                         nielsen_node* child = mk_child(node);
                         nielsen_edge* e = mk_edge(node, child, true);
@@ -1614,6 +1618,8 @@ namespace seq {
                         eqs[eq_idx] = eqs.back();
                         eqs.pop_back();
 
+                        if (lt->is_char())
+                            std::swap(lt, rt);
                         nielsen_subst subst(lt, rt, eq.m_dep);
                         e->add_subst(subst);
                         child->apply_subst(m_sg, subst);
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 99f679798..eeef89424 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -646,17 +646,16 @@ namespace seq {
         }
 
         void set_conflict(const backtrack_reason r, const dep_tracker confl) {
-            SASSERT(m_reason == backtrack_reason::unevaluated);
-            SASSERT(!m_conflict_internal);
-            SASSERT(m_conflict_external_literal == sat::null_literal);
+            if (m_conflict_internal != nullptr)
+                return;
+            // We prefer internal conflicts (we need it as a justification for general conflicts)
             m_reason = r;
             m_conflict_internal = confl;
         }
 
         void set_external_conflict(sat::literal lit) {
-            SASSERT(m_reason == backtrack_reason::unevaluated);
-            SASSERT(!m_conflict_internal);
-            SASSERT(m_conflict_external_literal == sat::null_literal);
+            if (m_reason != backtrack_reason::unevaluated)
+                return;
             m_reason = backtrack_reason::external;
             m_conflict_external_literal = ~lit;
         }