diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b200524e7..2a1930f4f 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -141,6 +141,8 @@ namespace sat {
         CASSERT("sat_solver", s.check_invariant());
         TRACE("before_simplifier", s.display(tout););
 
+        m_sub_todo.reset();
+        m_sub_bin_todo.reset();
         s.m_cleaner(true);
         m_last_sub_trail_sz = s.m_trail.size();
         TRACE("after_cleanup", s.display(tout););
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e0bb0f2a3..68c42f712 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3078,6 +3078,10 @@ namespace sat {
             m_binary_clause_graph[l1.index()].push_back(l2);
             m_binary_clause_graph[l2.index()].push_back(l1);
         }
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            m_binary_clause_graph.reserve(lits[i].index() + 1);
+            m_binary_clause_graph.reserve((~lits[i]).index() + 1);
+        }
         bool non_empty = true;
         m_seen[0].reset();
         while (non_empty) {