From 0fc7cca0af4885b9636b9bc8c3b4773cbd2b929f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Feb 2021 07:01:18 -0600
Subject: [PATCH] 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.
---
 src/theory/datatypes/inference_manager.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 8c12258af..9702a5584 100644
--- 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);
 }
 
-- 
2.30.2