summaryrefslogtreecommitdiff
path: root/src/proof/theory_proof.cpp
diff options
context:
space:
mode:
authorGuy <katz911@gmail.com>2016-07-25 17:24:39 -0700
committerGuy <katz911@gmail.com>2016-07-25 17:24:39 -0700
commitcb835bd526296d97f8ceb001569493723a59f86b (patch)
tree4e6196f6877bcc152ac008e9d508d64d57df7a7f /src/proof/theory_proof.cpp
parentd1cdf6f1719c3d56590ef6305f70f376f4d80b57 (diff)
Bug fix
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r--src/proof/theory_proof.cpp2
1 files changed, 1 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback