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 7985f7de05625b40952a3d90dda691b6325ea97a..cdba5dfd6726f63b81ca999315c4698595725766 100644 (file)
--- 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;