2 files changed, 17 insertions, 3 deletions
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 97b05802d..6a7078696 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -25,7 +25,9 @@ namespace CVC4 {
 namespace preprocessing {
 
 AssertionPipeline::AssertionPipeline(context::Context* context)
-    : d_substitutionsIndex(context, 0), d_topLevelSubstitutions(context)
+    : d_substitutionsIndex(context, 0),
+      d_topLevelSubstitutions(context),
+      d_realAssertionsEnd(0)
 {
 }
 
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 6f76b60e9..97fa32d17 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -56,7 +56,12 @@ class AssertionPipeline
   size_t size() const { return d_nodes.size(); }
 
   void resize(size_t n) { d_nodes.resize(n); }
-  void clear() { d_nodes.clear(); }
+
+  void clear()
+  {
+    d_nodes.clear();
+    d_realAssertionsEnd = 0;
+  }
 
   Node& operator[](size_t i) { return d_nodes[i]; }
   const Node& operator[](size_t i) const { return d_nodes[i]; }
@@ -99,6 +104,10 @@ class AssertionPipeline
     return d_topLevelSubstitutions;
   }
 
+  size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
+
+  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
+
  private:
   std::vector<Node> d_nodes;
 
@@ -107,12 +116,15 @@ class AssertionPipeline
    * corresponding introduced Boolean ite
    */
   IteSkolemMap d_iteSkolemMap;
-  
+
   /* Index for where to store substitutions */
   context::CDO<unsigned> d_substitutionsIndex;
 
   /* The top level substitutions */
   theory::SubstitutionMap d_topLevelSubstitutions;
+
+  /** Size of d_nodes when preprocessing starts */
+  size_t d_realAssertionsEnd;
 }; /* class AssertionPipeline */
 
 /**