diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 2746899da..7ae8c5793 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -268,6 +268,7 @@ namespace seq {
             for (const auto f : *to_app(c.fml)) {
                 add_constraint(constraint(f, c.dep, m));
             }
+            return;
         }
         expr* l, *r;
         if (m.is_eq(c.fml, l, r)) {
@@ -275,10 +276,6 @@ namespace seq {
                 return;
         }
         m_constraints.push_back(c);
-        SASSERT(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, c.dep);
     }
 
     void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@@ -1334,7 +1331,7 @@ namespace seq {
             return search_result::unknown;
 
 #ifdef Z3DEBUG
-        if (m_stats.m_num_dfs_nodes % 1000 == 0) {
+        if (m_stats.m_num_dfs_nodes % 200 == 0) {
             std::string dot = to_dot();
             dot = dot;
         }
@@ -4006,8 +4003,13 @@ nielsen_graph::generate_length_constraints(vector<length_constraint>& constraint
         // already present in the enclosing solver scope; asserting them again would
         // be redundant (though harmless).  This is called by search_dfs right after
         // simplify_and_init, which is where new constraints are produced.
+        SASSERT(m_literal_if_false);
         for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
-            m_solver.assert_expr(node->constraints()[i].fml);
+            auto& c = node->constraints()[i];
+            m_solver.assert_expr(c.fml);
+            auto lit = m_literal_if_false(c.fml);
+            if (lit != sat::null_literal)
+                node->set_external_conflict(lit, c.dep);
         }
     }
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index fe3e7768b..0ad11f3f1 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -248,7 +248,7 @@ namespace smt {
     void theory_nseq::assign_eh(bool_var v, bool is_true) {
         try {
             expr* e = ctx.bool_var2expr(v);
-            std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
+            // std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
             expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr;
             TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
             if (m_seq.str.is_in_re(e, s, re)) {
@@ -737,7 +737,7 @@ namespace smt {
             case l_true: 
                 break;
             case l_undef:
-                //std::cout << "Undef: " << mk_pp(c.fml, m) << "\n";
+                //std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << "\n";
                 has_undef = true; 
                 ctx.force_phase(lit);                
                 IF_VERBOSE(2, verbose_stream() << 
@@ -751,7 +751,7 @@ namespace smt {
                 ctx.force_phase(lit);
                 has_undef = true;
                 ctx.force_phase(lit);
-                //std::cout << "False: " << mk_pp(c.fml, m) << "\n";
+                //std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
                 break;
             }
         }