1 files changed, 30 insertions, 1 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 0bce3b8cd..7d4351baa 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -22,7 +22,36 @@
 namespace CVC4 {
 namespace preprocessing {
 
-AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {}
+AssertionPipeline::AssertionPipeline()
+    : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0)
+{
+}
+
+void AssertionPipeline::clear()
+{
+  d_nodes.clear();
+  d_realAssertionsEnd = 0;
+  d_assumptionsStart = 0;
+  d_numAssumptions = 0;
+}
+
+void AssertionPipeline::push_back(Node n, bool isAssumption)
+{
+  d_nodes.push_back(n);
+  if (isAssumption)
+  {
+    if (d_numAssumptions == 0)
+    {
+      d_assumptionsStart = d_nodes.size() - 1;
+    }
+    // Currently, we assume that assumptions are all added one after another
+    // and that we store them in the same vector as the assertions. Once we
+    // split the assertions up into multiple vectors (see issue #2473), we will
+    // not have this limitation anymore.
+    Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
+    d_numAssumptions++;
+  }
+}
 
 void AssertionPipeline::replace(size_t i, Node n)
 {