Return bool for lemmaTheoryInference (#7773)

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 8b4880feb312f615398115601561afaf0331ebd1..963e0b95c7a858bf1430f02b1d7593d070f65f4b 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -161,14 +161,14 @@ std::size_t InferenceManagerBuffered::numPendingFacts() const
   return d_pendingFact.size();
 }
 
-void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
+bool InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
 {
   // process this lemma
   LemmaProperty p = LemmaProperty::NONE;
   TrustNode tlem = lem->processLemma(p);
   Assert(!tlem.isNull());
   // send the lemma
-  trustedLemma(tlem, lem->getId(), p);
+  return trustedLemma(tlem, lem->getId(), p);
 }
 
 void InferenceManagerBuffered::assertInternalFactTheoryInference(

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index e93152f72cb2c32fda65429d0378fd2f1e48b7c5..579b1ae87eb432338b6f60dc320767ce7b356bab 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -149,9 +149,10 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   /**
    * Send the given theory inference as a lemma on the output channel of this
    * inference manager. This calls TheoryInferenceManager::trustedLemma based
-   * on the provided theory inference.
+   * on the provided theory inference, and returns true if the lemma was
+   * successfully sent.
    */
-  void lemmaTheoryInference(TheoryInference* lem);
+  bool lemmaTheoryInference(TheoryInference* lem);
   /**
    * Add the given theory inference as an internal fact. This calls
    * TheoryInferenceManager::assertInternalFact based on the provided theory