From cb835bd526296d97f8ceb001569493723a59f86b Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Mon, 25 Jul 2016 17:24:39 -0700
Subject: [PATCH] Bug fix

---
 src/proof/theory_proof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 9753844a1..eae8a68df 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1080,7 +1080,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;
-- 
2.30.2