1 files changed, 10 insertions, 6 deletions

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index bc409901c..139ce5ed2 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -67,13 +67,17 @@ inline static bool match(TNode n1, TNode n2) {
 
 
 void ProofUF::toStream(std::ostream& out) {
+  ProofLetMap map;
+  toStream(out, map);
+}
+
+void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) {
   Trace("theory-proof-debug") << "; Print UF proof..." << std::endl;
   //AJR : carry this further?
-  LetMap map;
   toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map);
 }
 
-void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) {
+void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
   Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl;
   Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl;
   pf->debug_print("lfsc-uf");
@@ -81,7 +85,7 @@ void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqPr
   toStreamRecLFSC( out, tp, pf, 0, map );
 }
 
-Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) {
+Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
   Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::uf");
   Debug("pf::uf") << std::endl;
@@ -693,7 +697,7 @@ void UFProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
 
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
@@ -732,14 +736,14 @@ void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
   os << type <<" ";
 }
 
-void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
   os << " ;; UF Theory Lemma \n;;";
   for (unsigned i = 0; i < lemma.size(); ++i) {
     os << lemma[i] <<" ";
   }
   os <<"\n";
   //os << " (clausify_false trust)";
-  UFProof::printTheoryLemmaProof( lemma, os, paren );
+  UFProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {