Process pending inferences at the beginning of datatypes post check (#5213)

This fixes a potential crash in datatypes where a pending inference is not processed on a call to Theory::check. This ensures the pending set of inferences in datatypes is empty after each check. This also ensures the pending vectors are cleared before each check in datatypes.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 5699e75ad..7985f7de0 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -118,6 +118,12 @@ void InferenceManagerBuffered::doPendingPhaseRequirements()
   }
   d_pendingReqPhase.clear();
 }
+void InferenceManagerBuffered::clearPending()
+{
+  d_pendingFact.clear();
+  d_pendingLem.clear();
+  d_pendingReqPhase.clear();
+}
 void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
 void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
 void InferenceManagerBuffered::clearPendingPhaseRequirements()