From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 19 Oct 2020 07:55:25 +0000 (-0500)
Subject: Safer version of pending lemma processing in inference manager buffered (#5286)
X-Git-Tag: cvc5-1.0.0~2696
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=46b55d615e32ab48065dde0187adeb760cdac949;p=cvc5.git

Safer version of pending lemma processing in inference manager buffered (#5286)

This ensures we don't segfault if the pending lemma vector is cleared while we are processing it. This is potentially possible in datatypes currently. Fixes #5236.
---

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 7985f7de0..cdba5dfd6 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -100,10 +100,13 @@ void InferenceManagerBuffered::doPendingLemmas()
     return;
   }
   d_processingPendingLemmas = true;
-  for (const std::unique_ptr<TheoryInference>& plem : d_pendingLem)
+  size_t i = 0;
+  while (i < d_pendingLem.size())
   {
-    // process this lemma
-    plem->process(this, true);
+    // process this lemma, which notice may enqueue more pending lemmas in this
+    // loop, or clear the lemmas.
+    d_pendingLem[i]->process(this, true);
+    i++;
   }
   d_pendingLem.clear();
   d_processingPendingLemmas = false;