From 44d05e537548d01e31ab49dab81bf24701a610e0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 9 Nov 2016 18:00:15 +0000
Subject: [PATCH] Fix cleanup/initialization of sat::simplifier. Relates to
 #570.

---
 src/sat/sat_clause.h       |   6 +-
 src/sat/sat_probing.cpp    |  18 ++---
 src/sat/sat_simplifier.cpp |  36 ++++++----
 src/sat/sat_simplifier.h   |  21 ++++--
 src/sat/sat_solver.cpp     | 130 ++++++++++++++++++-------------------
 src/sat/sat_types.h        |   4 +-
 6 files changed, 119 insertions(+), 96 deletions(-)

diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h
index 1662b429f..1aededbb6 100644
--- a/src/sat/sat_clause.h
+++ b/src/sat/sat_clause.h
@@ -102,10 +102,14 @@ namespace sat {
         unsigned m_val1;
         unsigned m_val2;
     public:
-        bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
+        bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
         literal get_literal1() const { return to_literal(m_val1); }
         literal get_literal2() const { return to_literal(m_val2 >> 1); }
         bool is_learned() const { return (m_val2 & 1) == 1; }
+        bool operator==(const bin_clause & other) const {
+            return  m_val1 == other.m_val1 && m_val2 == other.m_val2 ||
+                    m_val1 == other.m_val2 && m_val2 == other.m_val1;
+        }
     };
 
     class tmp_clause {
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index 165d39ad8..c00b68ac2 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -95,7 +95,7 @@ namespace sat {
             if (updt_cache)
                 cache_bins(l, old_tr_sz);
             s.pop(1);
-            
+
             literal_vector::iterator it  = m_to_assert.begin();
             literal_vector::iterator end = m_to_assert.end();
             for (; it != end; ++it) {
@@ -178,10 +178,10 @@ namespace sat {
             m_num_assigned(p.m_num_assigned) {
             m_watch.start();
         }
-        
+
         ~report() {
             m_watch.stop();
-            IF_VERBOSE(SAT_VB_LVL, 
+            IF_VERBOSE(SAT_VB_LVL,
                        verbose_stream() << " (sat-probing :probing-assigned "
                        << (m_probing.m_num_assigned - m_num_assigned)
                        << " :cost " << m_probing.m_counter;
@@ -189,7 +189,7 @@ namespace sat {
                        verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
     };
-     
+
     bool probing::operator()(bool force) {
         if (!m_probing)
             return true;
@@ -200,8 +200,8 @@ namespace sat {
         CASSERT("probing", s.check_invariant());
         if (!force && m_counter > 0)
             return true;
-        
-        if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) 
+
+        if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
             m_cached_bins.finalize();
 
         report rpt(*this);
@@ -256,14 +256,14 @@ namespace sat {
     }
 
     void probing::free_memory() {
-        m_assigned.cleanup();
+        m_assigned.finalize();
         m_to_assert.finalize();
     }
-    
+
     void probing::collect_statistics(statistics & st) const {
         st.update("probing assigned", m_num_assigned);
     }
-    
+
     void probing::reset_statistics() {
         m_num_assigned = 0;
     }
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b200524e7..151bdf45b 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -63,6 +63,7 @@ namespace sat {
     }
 
     simplifier::~simplifier() {
+        free_memory();
     }
 
     inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@@ -96,7 +97,7 @@ namespace sat {
     inline void simplifier::remove_clause_core(clause & c) {
         unsigned sz = c.size();
         for (unsigned i = 0; i < sz; i++)
-            insert_todo(c[i].var());
+            insert_elim_todo(c[i].var());
         m_sub_todo.erase(c);
         c.set_removed(true);
         TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@@ -116,6 +117,7 @@ namespace sat {
     inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
         SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
         s.get_wlist(~l1).erase(watched(l2, learned));
+        m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
     }
 
     void simplifier::init_visited() {
@@ -127,27 +129,36 @@ namespace sat {
         m_use_list.finalize();
         m_sub_todo.finalize();
         m_sub_bin_todo.finalize();
+        m_elim_todo.finalize();
         m_visited.finalize();
         m_bs_cs.finalize();
         m_bs_ls.finalize();
     }
 
+    void simplifier::initialize() {
+        m_need_cleanup = false;
+        s.m_cleaner(true);
+        m_last_sub_trail_sz = s.m_trail.size();
+        m_use_list.init(s.num_vars());
+        m_sub_todo.reset();
+        m_sub_bin_todo.reset();
+        m_elim_todo.reset();
+        init_visited();
+        TRACE("after_cleanup", s.display(tout););
+        CASSERT("sat_solver", s.check_invariant());
+    }
+
     void simplifier::operator()(bool learned) {
         if (s.inconsistent())
             return;
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
+        initialize();
+
         CASSERT("sat_solver", s.check_invariant());
         TRACE("before_simplifier", s.display(tout););
 
-        s.m_cleaner(true);
-        m_last_sub_trail_sz = s.m_trail.size();
-        TRACE("after_cleanup", s.display(tout););
-        CASSERT("sat_solver", s.check_invariant());
-        m_need_cleanup = false;
-        m_use_list.init(s.num_vars());
-        init_visited();
         bool learned_in_use_lists = false;
         if (learned) {
             register_clauses(s.m_learned);
@@ -158,7 +169,6 @@ namespace sat {
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
-
         if (!learned)
             m_num_calls++;
 
@@ -617,7 +627,7 @@ namespace sat {
         TRACE("elim_lit", tout << "processing: " << c << "\n";);
         m_need_cleanup = true;
         m_num_elim_lits++;
-        insert_todo(l.var());
+        insert_elim_todo(l.var());
         c.elim(l);
         clause_use_list & occurs = m_use_list.get(l);
         occurs.erase_not_removed(c);
@@ -920,7 +930,7 @@ namespace sat {
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
             model_converter::entry * new_entry = 0;
-            if (s.is_external(l.var()) || s.was_eliminated(l.var())) 
+            if (s.is_external(l.var()) || s.was_eliminated(l.var()))
                 return;
             {
 
@@ -1235,12 +1245,14 @@ namespace sat {
                 for (; it2 != end2; ++it2) {
                     if (it2->is_binary_clause() && it2->get_literal() == l) {
                         TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
+                        m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
                         continue;
                     }
                     *itprev = *it2;
                     itprev++;
                 }
                 wlist2.set_end(itprev);
+                m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
             }
         }
         TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);
@@ -1343,7 +1355,7 @@ namespace sat {
         }
         TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
 
-        
+
         // eliminate variable
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 85922cf7c..f0f78b9c2 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -9,7 +9,7 @@ Abstract:
 
     SAT simplification procedures that use a "full" occurrence list:
     Subsumption, Blocked Clause Removal, Variable Elimination, ...
-    
+
 
 Author:
 
@@ -83,7 +83,7 @@ namespace sat {
         bool                   m_subsumption;
         unsigned               m_subsumption_limit;
         bool                   m_elim_vars;
-        
+
         // stats
         unsigned               m_num_blocked_clauses;
         unsigned               m_num_subsumed;
@@ -97,6 +97,8 @@ namespace sat {
 
         void checkpoint();
 
+        void initialize();
+
         void init_visited();
         void mark_visited(literal l) { m_visited[l.index()] = true; }
         void unmark_visited(literal l) { m_visited[l.index()] = false; }
@@ -135,7 +137,7 @@ namespace sat {
         void mark_as_not_learned_core(watch_list & wlist, literal l2);
         void mark_as_not_learned(literal l1, literal l2);
         void subsume();
-        
+
         void cleanup_watches();
         void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
 
@@ -145,7 +147,7 @@ namespace sat {
         lbool value(literal l) const;
         watch_list & get_wlist(literal l);
         watch_list const & get_wlist(literal l) const;
-        
+
         struct blocked_clause_elim;
         void elim_blocked_clauses();
 
@@ -172,14 +174,19 @@ namespace sat {
         simplifier(solver & s, params_ref const & p);
         ~simplifier();
 
-        void insert_todo(bool_var v) { m_elim_todo.insert(v); }
-        void reset_todo() { m_elim_todo.reset(); }
+        void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); }
+
+        void reset_todos() {
+            m_elim_todo.reset();
+            m_sub_todo.reset();
+            m_sub_bin_todo.reset();
+        }
 
         void operator()(bool learned);
 
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
-        
+
         void free_memory();
 
         void collect_statistics(statistics & st) const;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e0bb0f2a3..1aede522a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -141,7 +141,7 @@ namespace sat {
         m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
         m_assigned_since_gc.push_back(false);
         m_case_split_queue.mk_var_eh(v);
-        m_simplifier.insert_todo(v);
+        m_simplifier.insert_elim_todo(v);
         SASSERT(!was_eliminated(v));
         return v;
     }
@@ -151,7 +151,7 @@ namespace sat {
             for (unsigned i = 0; i < num_lits; i++)
                 SASSERT(m_eliminated[lits[i].var()] == false);
         });
-        
+
         if (m_user_scope_literals.empty()) {
             mk_clause_core(num_lits, lits, false);
         }
@@ -175,8 +175,8 @@ namespace sat {
 
     void solver::del_clause(clause& c) {
         if (!c.is_learned()) m_stats.m_non_learned_generation++;
-        m_cls_allocator.del_clause(&c); 
-        m_stats.m_del_clause++; 
+        m_cls_allocator.del_clause(&c);
+        m_stats.m_del_clause++;
     }
 
     clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
@@ -188,7 +188,7 @@ namespace sat {
                 return 0; // clause is equivalent to true.
             }
             ++m_stats.m_non_learned_generation;
-        }        
+        }
 
         switch (num_lits) {
         case 0:
@@ -739,10 +739,10 @@ namespace sat {
                 m_restart_threshold       = m_config.m_restart_initial;
             }
 
-            // iff3_finder(*this)();            
+            // iff3_finder(*this)();
             simplify_problem();
             if (check_inconsistent()) return l_false;
-            
+
 
             if (m_config.m_max_conflicts == 0) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
@@ -763,7 +763,7 @@ namespace sat {
 
                 restart();
                 simplify_problem();
-                if (check_inconsistent()) return l_false;                
+                if (check_inconsistent()) return l_false;
                 gc();
             }
         }
@@ -891,7 +891,7 @@ namespace sat {
         else {
             mk_model();
             return l_true;
-        }        
+        }
     }
 
 
@@ -920,8 +920,8 @@ namespace sat {
             return;
         }
 
-        TRACE("sat", 
-              for (unsigned i = 0; i < num_lits; ++i) 
+        TRACE("sat",
+              for (unsigned i = 0; i < num_lits; ++i)
                   tout << lits[i] << " ";
               tout << "\n";
               if (!m_user_scope_literals.empty()) {
@@ -932,7 +932,7 @@ namespace sat {
 
         for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
             literal nlit = ~m_user_scope_literals[i];
-            assign(nlit, justification());                   
+            assign(nlit, justification());
         }
 
         if (weights && !inconsistent()) {
@@ -947,9 +947,9 @@ namespace sat {
 
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
-            SASSERT(is_external(lit.var()));  
-            add_assumption(lit);  
-            assign(lit, justification());       
+            SASSERT(is_external(lit.var()));
+            add_assumption(lit);
+            assign(lit, justification());
         }
     }
 
@@ -962,10 +962,10 @@ namespace sat {
         unsigned num_cores = 0;
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
-            SASSERT(is_external(lit.var()));  
+            SASSERT(is_external(lit.var()));
             TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
             SASSERT(m_scope_lvl == 1);
-            add_assumption(lit);  
+            add_assumption(lit);
             switch(value(lit)) {
             case l_undef:
                 values.push_back(l_true);
@@ -973,10 +973,10 @@ namespace sat {
                 if (num_cores*2 >= num_lits) {
                     break;
                 }
-                propagate(false);                
+                propagate(false);
                 if (inconsistent()) {
                     flet<bool> _init(m_initializing_preferred, true);
-                    while (inconsistent()) {                        
+                    while (inconsistent()) {
                         if (!resolve_conflict()) {
                             return true;
                         }
@@ -1001,15 +1001,15 @@ namespace sat {
                     for (unsigned k = i; k >= j; --k)  {
                         if (is_assumption(lits[k])) {
                             pop_assumption();
-                        }                        
+                        }
                     }
                     values.resize(j);
                     TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";);
                     i = j - 1;
                 }
-                break;                
-                
-            case l_false: 
+                break;
+
+            case l_false:
                 ++num_cores;
                 values.push_back(l_false);
                 SASSERT(!inconsistent());
@@ -1028,14 +1028,14 @@ namespace sat {
                 SASSERT(m_assumptions.size() <= i+1);
                 if (m_core.size() <= 3) {
                     m_inconsistent = true;
-                    TRACE("opt", tout << "found small core: " << m_core << "\n";); 
+                    TRACE("opt", tout << "found small core: " << m_core << "\n";);
                     IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";);
                     return true;
                 }
                 pop_assumption();
-                m_inconsistent = false; 
+                m_inconsistent = false;
                 break;
-            case l_true: 
+            case l_true:
                 values.push_back(l_true);
                 SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0);
                 break;
@@ -1046,7 +1046,7 @@ namespace sat {
         if (m_weight >= max_weight) {
             // block the current correction set candidate.
             ++m_stats.m_blocked_corr_sets;
-            TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); 
+            TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";);
             IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";);
             pop_to_base_level();
             mk_clause_core(m_blocker);
@@ -1062,17 +1062,17 @@ namespace sat {
             m_min_core.reset();
             m_min_core.append(m_core);
             m_min_core_valid = true;
-        }        
+        }
     }
 
     void solver::reset_assumptions() {
         m_assumptions.reset();
-        m_assumption_set.reset();                
+        m_assumption_set.reset();
     }
 
     void solver::add_assumption(literal lit) {
-        m_assumption_set.insert(lit);       
-        m_assumptions.push_back(lit);                   
+        m_assumption_set.insert(lit);
+        m_assumptions.push_back(lit);
     }
 
     void solver::pop_assumption() {
@@ -1089,8 +1089,8 @@ namespace sat {
         for (unsigned i = 0; i < m_min_core.size(); ++i) {
             literal lit = m_min_core[i];
             SASSERT(is_external(lit.var()));
-            add_assumption(lit);  
-            assign(lit, justification());       
+            add_assumption(lit);
+            assign(lit, justification());
         }
         propagate(false);
         SASSERT(inconsistent());
@@ -1132,7 +1132,7 @@ namespace sat {
         m_min_core_valid = false;
         m_min_core.reset();
         TRACE("sat", display(tout););
-        
+
         if (m_config.m_bcd) {
             bceq bc(*this);
             bc();
@@ -1149,11 +1149,11 @@ namespace sat {
         }
         IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";);
 
-        // Disable simplification during MUS computation.        
+        // Disable simplification during MUS computation.
         // if (m_mus.is_active()) return;
         TRACE("sat", tout << "simplify\n";);
 
-        pop(scope_lvl());        
+        pop(scope_lvl());
 
         SASSERT(scope_lvl() == 0);
 
@@ -1166,7 +1166,7 @@ namespace sat {
         m_simplifier(false);
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
-        
+
         if (!m_learned.empty()) {
             m_simplifier(true);
             CASSERT("sat_missed_prop", check_missed_propagation());
@@ -1260,7 +1260,7 @@ namespace sat {
                     TRACE("sat", tout << "failed: " << c << "\n";
                           tout << "assumptions: " << m_assumptions << "\n";
                           tout << "trail: " << m_trail << "\n";
-                          tout << "model: " << m << "\n";      
+                          tout << "model: " << m << "\n";
                           m_mc.display(tout);
                           );
                     ok = false;
@@ -1289,10 +1289,10 @@ namespace sat {
         }
         for (unsigned i = 0; i < m_assumptions.size(); ++i) {
             if (value_at(m_assumptions[i], m) != l_true) {
-                TRACE("sat", 
+                TRACE("sat",
                       tout << m_assumptions[i] << " does not model check\n";
                       tout << "trail: " << m_trail << "\n";
-                      tout << "model: " << m << "\n";      
+                      tout << "model: " << m << "\n";
                       m_mc.display(tout);
                       );
                 ok = false;
@@ -1664,7 +1664,7 @@ namespace sat {
             resolve_conflict_for_unsat_core();
             return false;
         }
-        
+
         if (m_conflict_lvl == 0) {
             return false;
         }
@@ -1849,11 +1849,11 @@ namespace sat {
     bool solver::resolve_conflict_for_init() {
         if (m_conflict_lvl == 0) {
             return false;
-        }        
+        }
         m_lemma.reset();
         m_lemma.push_back(null_literal); // asserted literal
         if (m_not_l != null_literal) {
-            TRACE("sat", tout << "not_l: " << m_not_l << "\n";);            
+            TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
             process_antecedent_for_init(m_not_l);
         }
         literal consequent = m_not_l;
@@ -1988,7 +1988,7 @@ namespace sat {
                     SASSERT(!is_marked(m_trail[i].var()));
                 }});
 
-        unsigned old_size = m_unmark.size();        
+        unsigned old_size = m_unmark.size();
         int idx = skip_literals_above_conflict_level();
 
         if (m_not_l != null_literal) {
@@ -2005,7 +2005,7 @@ namespace sat {
                 process_consequent_for_unsat_core(m_not_l, js);
             }
         }
-                    
+
         literal consequent = m_not_l;
         justification js   = m_conflict;
 
@@ -2031,7 +2031,7 @@ namespace sat {
             SASSERT(lvl(consequent) == m_conflict_lvl);
             js             = m_justification[c_var];
             idx--;
-        }        
+        }
         reset_unmark(old_size);
         if (m_config.m_core_minimize) {
             if (m_min_core_valid && m_min_core.size() < m_core.size()) {
@@ -2039,7 +2039,7 @@ namespace sat {
                 m_core.reset();
                 m_core.append(m_min_core);
             }
-            // TBD: 
+            // TBD:
             // apply optional clause minimization by detecting subsumed literals.
             // initial experiment suggests it has no effect.
             m_mus(); // ignore return value on cancelation.
@@ -2511,7 +2511,7 @@ namespace sat {
 
     void solver::pop_reinit(unsigned num_scopes) {
         pop(num_scopes);
-        reinit_assumptions();        
+        reinit_assumptions();
     }
 
     void solver::pop(unsigned num_scopes) {
@@ -2578,13 +2578,13 @@ namespace sat {
         m_clauses_to_reinit.shrink(j);
     }
 
-    // 
+    //
     // All new clauses that are added to the solver
     // are relative to the user-scope literals.
-    // 
+    //
 
     void solver::user_push() {
-        literal lit;      
+        literal lit;
         bool_var new_v = mk_var(true, false);
         lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
@@ -2674,7 +2674,7 @@ namespace sat {
             m_phase.shrink(v);
             m_prev_phase.shrink(v);
             m_assigned_since_gc.shrink(v);
-            m_simplifier.reset_todo();
+            m_simplifier.reset_todos();
         }
     }
 
@@ -2698,7 +2698,7 @@ namespace sat {
                     unassign_vars(i);
                     break;
                 }
-            }            
+            }
             gc_var(lit.var());
         }
     }
@@ -3080,10 +3080,10 @@ namespace sat {
         }
         bool non_empty = true;
         m_seen[0].reset();
-        while (non_empty) {            
+        while (non_empty) {
             literal_vector mutex;
             bool turn = false;
-            m_reachable[turn] = ps; 
+            m_reachable[turn] = ps;
             while (!m_reachable[turn].empty()) {
                 literal p = m_reachable[turn].pop();
                 if (m_seen[0].contains(p)) {
@@ -3100,7 +3100,7 @@ namespace sat {
                 turn = !turn;
             }
             if (mutex.size() > 1) {
-                mutexes.push_back(mutex);            
+                mutexes.push_back(mutex);
             }
             non_empty = !mutex.empty();
         }
@@ -3144,7 +3144,7 @@ namespace sat {
             switch (get_model()[v]) {
             case l_true: lits.push_back(literal(v, false)); break;
             case l_false: lits.push_back(literal(v, true)); break;
-            default: break;                
+            default: break;
             }
         }
         is_sat = get_consequences(asms, lits, conseq);
@@ -3171,7 +3171,7 @@ namespace sat {
         }
         propagate(false);
         if (check_inconsistent()) return l_false;
-       
+
         unsigned num_units = 0, num_iterations = 0;
         extract_fixed_consequences(num_units, assumptions, vars, conseq);
         while (!vars.empty()) {
@@ -3188,14 +3188,14 @@ namespace sat {
                 push();
                 assign(~lit, justification());
                 propagate(false);
-                while (inconsistent()) {      
+                while (inconsistent()) {
                     if (!resolve_conflict()) {
                         TRACE("sat", display(tout << "inconsistent\n"););
                         m_inconsistent = false;
                         is_sat = l_undef;
                         break;
                     }
-                    propagate(false);                    
+                    propagate(false);
                     ++num_resolves;
                 }
                 if (scope_lvl() == 1) {
@@ -3209,7 +3209,7 @@ namespace sat {
                 else {
                     is_sat = bounded_search();
                     if (is_sat == l_undef) {
-                        restart();      
+                        restart();
                     }
                 }
             }
@@ -3220,7 +3220,7 @@ namespace sat {
             if (is_sat == l_true) {
                 delete_unfixed(vars);
             }
-            extract_fixed_consequences(num_units, assumptions, vars, conseq);            
+            extract_fixed_consequences(num_units, assumptions, vars, conseq);
             IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
                        << " iterations: " << num_iterations
                        << " variables: " << vars.size()
@@ -3240,10 +3240,10 @@ namespace sat {
             if (value(lit) == l_true) {
                 to_keep.insert(lit);
             }
-        }        
+        }
         unfixed = to_keep;
     }
-    
+
     void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
         if (scope_lvl() > 1) {
             pop(scope_lvl() - 1);
@@ -3293,7 +3293,7 @@ namespace sat {
     }
 
     void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
-        index_set s;        
+        index_set s;
         if (assumptions.contains(lit)) {
             s.insert(lit.index());
         }
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 00edaa593..509cc58ba 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -200,7 +200,7 @@ namespace sat {
         iterator begin() const { return m_set.begin(); }
         iterator end() const { return m_set.end(); }
         void reset() { m_set.reset(); m_in_set.reset(); }
-        void cleanup() { m_set.finalize(); m_in_set.finalize(); }
+        void finalize() { m_set.finalize(); m_in_set.finalize(); }
         uint_set& operator&=(uint_set const& other) {
             unsigned j = 0;
             for (unsigned i = 0; i < m_set.size(); ++i) {
@@ -259,7 +259,7 @@ namespace sat {
         bool empty() const { return m_set.empty(); }
         unsigned size() const { return m_set.size(); }
         void reset() { m_set.reset(); }
-        void cleanup() { m_set.cleanup(); }
+        void finalize() { m_set.finalize(); }
         class iterator {
             uint_set::iterator m_it;
         public: