From bfaa9ddf633b542a0aa01bd925a7c3d1a5b3097d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 10 Nov 2016 17:06:55 +0000
Subject: [PATCH] Fixed potential SAT solver cleanup problem. Renamed functions
 for consistency. Relates to #570.

---
 src/sat/sat_probing.cpp    |  5 +++--
 src/sat/sat_probing.h      |  2 +-
 src/sat/sat_simplifier.cpp | 10 ++++++----
 src/sat/sat_simplifier.h   |  2 +-
 src/sat/sat_solver.cpp     |  2 +-
 src/sat/sat_solver.h       |  1 +
 6 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index c00b68ac2..0b5edb2c9 100644
--- a/src/sat/sat_probing.cpp
+++ b/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 {
diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h
index daf6817e3..cce165a34 100644
--- a/src/sat/sat_probing.h
+++ b/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();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 3e817b2a9..c42572f1e 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/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);
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index f0f78b9c2..9ee239083 100644
--- a/src/sat/sat_simplifier.h
+++ b/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();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5bc9e4ed9..7acfda822 100644
--- a/src/sat/sat_solver.cpp
+++ b/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();
     }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c0d736ebf..a44f07a23 100644
--- a/src/sat/sat_solver.h
+++ b/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;