diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index f430f3a0c..882025024 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -190,7 +190,7 @@ namespace nlsat {
         }
         
         ~imp() {
-            reset();
+            clear();
         }
 
         void mk_true_bvar() {
@@ -230,6 +230,11 @@ namespace nlsat {
             m_assignment.reset();
         }
 
+        void clear() {
+            undo_until_size(0);
+            del_clauses();
+            del_unref_atoms();
+        }
 
         void checkpoint() {
             if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());