Add asLemma flag to theory inference process (#5030)

This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.

It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 3ba41a431..b0d092d74 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -86,7 +86,7 @@ void InferenceManagerBuffered::doPendingFacts()
   {
     // process this fact, which notice may enqueue more pending facts in this
     // loop.
-    d_pendingFact[i]->process(this);
+    d_pendingFact[i]->process(this, false);
     i++;
   }
   d_pendingFact.clear();
@@ -97,7 +97,7 @@ void InferenceManagerBuffered::doPendingLemmas()
   for (const std::unique_ptr<TheoryInference>& plem : d_pendingLem)
   {
     // process this lemma
-    plem->process(this);
+    plem->process(this, true);
   }
   d_pendingLem.clear();
 }