Fix datatypes inference manager when proofs are enabled (#5937)

Accidentally was not sending lemmas in one interface when proofs are enabled due to recent refactoring.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 8c12258afba571d169044387053b4cb55c0a78ed..9702a558464dc7a029578f151e62e71fb4890f73 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -74,10 +74,11 @@ void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p)
 {
   if (isProofEnabled())
   {
-    processDtLemma(lem, Node::null(), id);
+    TrustNode trn = processDtLemma(lem, Node::null(), id);
+    trustedLemma(trn, id);
     return;
   }
-  // otherwise send as a normal lemma
+  // otherwise send as a normal lemma directly
   lemma(lem, id, p);
 }