diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 7352813a8..04660cdd8 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -697,9 +697,10 @@ namespace seq {
             return nullptr;
 
         euf::snode* rebuilt = nullptr;
-        for (unsigned k = 0; k < result.size(); ++k)
-            rebuilt = (k == 0) ? result[k] : sg.mk_concat(rebuilt, result[k]);
-        if (!rebuilt) rebuilt = sg.mk_empty_seq(side->get_sort());
+        for (auto tok : result) 
+            rebuilt = rebuilt ? sg.mk_concat(rebuilt, tok) : tok;        
+        if (!rebuilt) 
+            rebuilt = sg.mk_empty_seq(side->get_sort());
         return rebuilt;
     }
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 3fed67df9..6075e23b5 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -702,16 +702,11 @@ namespace smt {
                 break;
             case l_false: 
                 // this should not happen because nielsen checks for this before returning a satisfying path.
-                IF_VERBOSE(0, verbose_stream()
+                IF_VERBOSE(1, verbose_stream()
                                   << "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
                 ctx.force_phase(lit);
-                if (!was_internalized) {
-                    has_undef = true;
-                    ctx.force_phase(lit);    
-                    break;
-                }
-                TRACE(seq, tout << "assigned to false: " << c.fml << "\n");
-                UNREACHABLE();
+                has_undef = true;
+                ctx.force_phase(lit);    
                 break;
             }
         }