diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h
index 54139f6c1..803cee39e 100644
--- a/src/smt/nseq_context_solver.h
+++ b/src/smt/nseq_context_solver.h
@@ -68,6 +68,10 @@ namespace smt {
         void get_model(model_ref& mdl) override {
             m_kernel.get_model(mdl);
         }
+
+        void reset() override {
+            m_kernel.reset();
+        }
     };
 
 }
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 370927572..1e54ac798 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -538,8 +538,6 @@ namespace seq {
         m_parikh(alloc(seq_parikh, sg)),
         m_seq_regex(alloc(seq::seq_regex, sg)),
         m_len_vars(sg.get_manager()) {
-
-        m_solver.push(); // we start by resetting the graph which will pop it first
     }
 
     nielsen_graph::~nielsen_graph() {
@@ -635,8 +633,7 @@ namespace seq {
         m_len_var_cache.clear();
         m_len_vars.reset();
         m_dep_mgr.reset();
-        m_solver.pop(1);
-        m_solver.push();
+        m_solver.reset();
     }
 
     std::ostream& nielsen_graph::display(std::ostream& out) const {
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index e597db807..64a5e57c1 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -278,6 +278,7 @@ namespace seq {
         virtual void    push() = 0;
         virtual void    pop(unsigned num_scopes) = 0;
         virtual void    get_model(model_ref& mdl) { mdl = nullptr; }
+        virtual void    reset() = 0;
     };
 
     // simplification result for constraint processing