diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index a91ed8ea7..085a5567b 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -573,8 +573,8 @@ namespace seq {
     }
 
     void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) {
-        if (!m_root)
-            m_root = mk_node();
+        if (!root())
+            create_root();
         dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
         str_eq eq(lhs, rhs, dep);
         eq.sort();
@@ -582,8 +582,8 @@ namespace seq {
     }
 
     void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) {
-        if (!m_root)
-            m_root = mk_node();
+        if (!root())
+            create_root();
         dep_tracker dep = m_dep_mgr.mk_leaf(l);
         euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
         unsigned id = next_mem_id();
@@ -592,8 +592,8 @@ namespace seq {
 
     // test-friendly overloads (no external dependency tracking)
     void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
-        if (!m_root)
-            m_root = mk_node();
+        if (root())
+            create_root();
         dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
         str_eq eq(lhs, rhs, dep);
         eq.sort();
@@ -601,8 +601,8 @@ namespace seq {
     }
 
     void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) {
-        if (!m_root)
-            m_root = mk_node();
+        if (!root())
+            create_root();
         dep_tracker dep = nullptr;
         euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
         unsigned id = next_mem_id();
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index b7e96c94f..84a92b7c3 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -835,11 +835,24 @@ namespace seq {
 
         // root node access
         nielsen_node* root() const { return m_root; }
-        void set_root(nielsen_node* n) { m_root = n; }
+        void set_root(nielsen_node* n) {
+            SASSERT(n);
+            m_root = n;
+        }
 
         // satisfying leaf node (set by solve() when result is sat)
         nielsen_node* sat_node() const { return m_sat_node; }
-        void set_sat_node(nielsen_node* n) { m_sat_node = n; }
+        void set_sat_node(nielsen_node* n) {
+            SASSERT(n);
+            m_sat_node = n;
+        }
+
+        // creates a new root for the graph
+        void create_root() {
+            SASSERT(!root());
+            set_root(mk_node());
+        }
+
         // path of edges from root to sat_node (set when sat_node is set)
         svector<nielsen_edge*> const& sat_path() const { return m_sat_path; }
 
@@ -935,9 +948,10 @@ namespace seq {
         bool solve_sat_path_ints(model_ref& mdl);
 
         // accessor for the seq_regex module
-        seq::seq_regex* seq_regex_module() const { return m_seq_regex; }
+        seq_regex* seq_regex_module() const { return m_seq_regex; }
 
     private:
+
         search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
 
         // Regex widening: overapproximate `str` by replacing variables with
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index d26fa69a0..40c45e895 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -371,8 +371,12 @@ namespace smt {
             return FC_CONTINUE;
         }
 
+        // there is nothing to do for the string solver, as there are no string constraints
         if (m_state.empty() && m_ho_terms.empty() && !has_unhandled_preds()) {
             IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state+ho, FC_DONE (no solve)\n";);
+            m_nielsen.reset();
+            m_nielsen.create_root();
+            m_nielsen.set_sat_node(m_nielsen.root());
             return FC_DONE;
         }
 
@@ -384,6 +388,9 @@ namespace smt {
 
         if (m_state.empty() && !has_unhandled_preds()) {
             IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n";);
+            m_nielsen.reset();
+            m_nielsen.create_root();
+            m_nielsen.set_sat_node(m_nielsen.root());
             return FC_DONE;
         }