Some fixes

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index 35fc5e348..d447cbf60 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/trust_node.h"
 
+#include "theory/proof_engine_output_channel.h"
+
 namespace CVC4 {
 namespace theory {
 
@@ -36,14 +38,14 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
 TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
 {
   // if a generator is provided, should confirm that it can prove it
-  Assert(g == nullptr || g->hasProofFor(conf));
+  Assert(g == nullptr || g->hasProofFor(ProofEngineOutputChannel::getConflictKeyValue(conf)));
   return TrustNode(TrustNodeKind::CONFLICT, conf, g);
 }
 
 TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
 {
   // if a generator is provided, should confirm that it can prove it
-  Assert(g == nullptr || g->hasProofFor(lem));
+  Assert(g == nullptr || g->hasProofFor(ProofEngineOutputChannel::getLemmaKeyValue(lem)));
   return TrustNode(TrustNodeKind::LEMMA, lem, g);
 }