diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index faa940869..7a6957467 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -656,6 +656,7 @@ namespace sat {
         s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
         if (s.inconsistent())
             return;
+        m_use_list.reserve(s.num_vars());
         unsigned new_trail_sz = s.m_trail.size();
         for (unsigned i = old_trail_sz; i < new_trail_sz; i++) {
             literal l = s.m_trail[i];
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 0b512275e..a1bd18901 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -40,15 +40,17 @@ namespace sat {
 
     class use_list {
         vector<clause_use_list> m_use_list;
+        
     public:
         void init(unsigned num_vars);
+        void reserve(unsigned num_vars) { while (m_use_list.size() <= 2*num_vars) m_use_list.push_back(clause_use_list()); }
         void insert(clause & c);
         void block(clause & c);
         void unblock(clause & c);
         void erase(clause & c);
         void erase(clause & c, literal l);
-        clause_use_list & get(literal l) { return m_use_list[l.index()]; }
-        clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
+        clause_use_list& get(literal l) { return m_use_list[l.index()]; }
+        clause_use_list const& get(literal l) const { return m_use_list[l.index()]; }
         void finalize() { m_use_list.finalize(); }
         std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); }
     };