From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Feb 2021 13:01:18 +0000 (-0600)
Subject: Fix datatypes inference manager when proofs are enabled (#5937)
X-Git-Tag: cvc5-1.0.0~2255
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0fc7cca0af4885b9636b9bc8c3b4773cbd2b929f;p=cvc5.git

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 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);
 }