From: Guy <katz911@gmail.com>
Date: Mon, 25 Jul 2016 23:52:27 +0000 (-0700)
Subject: Bug fix
X-Git-Tag: cvc5-1.0.0~6040^2~33
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df8c922b3d212bc5fadcd5cd26ebe868a9fe0f47;p=cvc5.git

Bug fix
---

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index f544f5ff5..8c74d0c2c 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1087,7 +1087,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
       }
 
       // The let map should already have the current expression.
-      ProofLetMap::const_iterator it = map.find(term);
+      ProofLetMap::const_iterator it = map.find(currentExpression.toExpr());
       if (it != map.end()) {
         unsigned id = it->second.id;
         unsigned count = it->second.count;