1 files changed, 13 insertions, 0 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 2cacfbcc0..8da3856ff 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -67,6 +67,19 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(0, dummy);
     remove_satisfied      = false;
+
+    // add the initialization for all the internal variables
+    for (int i = frozen.size(); i < vardata.size(); ++ i) {
+      frozen    .push(1);
+      eliminated.push(0);
+      if (use_simplification){
+          n_occ     .push(0);
+          n_occ     .push(0);
+          occurs    .init(i);
+          touched   .push(0);
+          elim_heap .insert(i);
+      }
+    }
 }