2 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 83082ff5d..c0cf06767 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -174,6 +174,16 @@ public:
   }
 
   /**
+   * Clear the assertion queue.
+   */
+  void clearAssertionQueue() {
+    while (d_facts.size() > 0) {
+      d_facts.pop();
+    }
+  }
+
+
+  /**
    * Check the current assignment's consistency.
    */
   virtual void check(Effort level = FULL_EFFORT) = 0;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 87a78d920..4751a584c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -150,6 +150,13 @@ public:
     return d_theoryOut.d_conflictNode;
   }
 
+  /**
+   * Clears the queues of the theories.
+   */
+  void clearAssertionQueues() {
+    d_uf.clearAssertionQueue();
+  }
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */