Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570.

src/sat/sat_probing.cpp

@@ -239,7 +239,7 @@ namespace sat {
             m_counter *= 2;
         }
         CASSERT("probing", s.check_invariant());
-        free_memory();
+        finalize();
         return r;
     }
 
@@ -255,9 +255,10 @@ namespace sat {
         // TODO
     }
 
-    void probing::free_memory() {
+    void probing::finalize() {
         m_assigned.finalize();
         m_to_assert.finalize();
+        m_cached_bins.finalize();
     }
 
     void probing::collect_statistics(statistics & st) const {

src/sat/sat_probing.h

@@ -69,7 +69,7 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void free_memory();
+        void finalize();
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();

src/sat/sat_simplifier.cpp

@@ -63,7 +63,7 @@ namespace sat {
     }
 
     simplifier::~simplifier() {
-        free_memory();
+        finalize();
     }
 
     inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@@ -125,7 +125,7 @@ namespace sat {
         m_visited.resize(2*s.num_vars(), false);
     }
 
-    void simplifier::free_memory() {
+    void simplifier::finalize() {
         m_use_list.finalize();
         m_sub_todo.finalize();
         m_sub_bin_todo.finalize();
@@ -154,6 +154,7 @@ namespace sat {
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
+
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());
@@ -175,6 +176,7 @@ namespace sat {
         }
         register_clauses(s.m_clauses);
 
+
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
@@ -216,7 +218,7 @@ namespace sat {
         }
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
-        free_memory();
+        finalize();
     }
 
     /**
@@ -941,8 +943,8 @@ namespace sat {
             model_converter::entry * new_entry = 0;
             if (s.is_external(l.var()) || s.was_eliminated(l.var()))
                 return;
-            {
 
+            {
                 m_to_remove.reset();
                 {
                     clause_use_list & occs = s.m_use_list.get(l);

src/sat/sat_simplifier.h

@@ -187,7 +187,7 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void free_memory();
+        void finalize();
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();

src/sat/sat_solver.cpp

@@ -3042,7 +3042,7 @@ namespace sat {
         if (scope_lvl() > 0 || inconsistent())
             return;
         m_simplifier(learned);
-        m_simplifier.free_memory();
+        m_simplifier.finalize();
         if (m_ext)
             m_ext->clauses_modifed();
     }

src/sat/sat_solver.h

@@ -239,6 +239,7 @@ namespace sat {
         void checkpoint() {
             if (!m_rlimit.inc()) {
                 m_mc.reset();
+                m_model_is_current = false;
                 throw solver_exception(Z3_CANCELED_MSG);
             }
             ++m_num_checkpoints;