Avoiding cyclic redundant steps

2 files changed, 11 insertions, 0 deletions

diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index 60c224e61..c16b2cdbc 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -81,6 +81,15 @@ void ProofStepBuffer::addStep(PfRule id,
       std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
 }
 
+void ProofStepBuffer::popStep()
+{
+  Assert (!d_steps.empty());
+  if (!d_steps.empty())
+  {
+    d_steps.pop_back();
+  }
+}
+
 size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); }
 
 const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 56dc113e1..db07f8649 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -68,6 +68,8 @@ class ProofStepBuffer
                const std::vector<Node>& children,
                const std::vector<Node>& args,
                Node expected);
+  /** pop step */
+  void popStep();
   /** Get num steps */
   size_t getNumSteps() const;
   /** Get steps */