diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 2de93677d..a2492cb1a 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -109,13 +109,10 @@ namespace api {
 
     context::~context() {
         m_last_obj = nullptr;
-        u_map<api::object*>::iterator it = m_allocated_objects.begin();
-        while (it != m_allocated_objects.end()) {
-            api::object* val = it->m_value;
-            DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*val).name()););
-            m_allocated_objects.remove(it->m_key);
+        for (auto& kv : m_allocated_objects) {
+            api::object* val = kv.m_value;
+            DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
             dealloc(val);
-            it = m_allocated_objects.begin();
         }
     }
 
diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre
index 4d221aac3..5c1a3bd06 100644
--- a/src/api/ml/z3native_stubs.c.pre
+++ b/src/api/ml/z3native_stubs.c.pre
@@ -458,7 +458,7 @@ CAMLprim DLL_PUBLIC value n_mk_config() {
   z3rv = Z3_mk_config();
 
   if (z3rv == NULL) {
-    caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "internal error");
+    caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "Object allocation failed");
   }
 
   /* construct simple return value */
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index f430f3a0c..6ea764a0a 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,14 @@ namespace nlsat {
             m_assignment.reset();
         }
 
+        void clear() {
+            m_explain.reset();
+            m_lemma.reset();
+            m_lazy_clause.reset();
+            undo_until_size(0);
+            del_clauses();
+            del_unref_atoms();
+        }
 
         void checkpoint() {
             if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());