Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)

1 files changed, 3 insertions, 3 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index f0f333598..f544f5ff5 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -406,13 +406,13 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
 
   TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
   TheoryProofTable::const_iterator end = d_theoryProofTable.end();
   for (; it != end; ++it) {
-    it->second->printAliasingDeclarations(os, paren);
+    it->second->printAliasingDeclarations(os, paren, globalLetMap);
   }
 }
 
@@ -1168,7 +1168,7 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream&
   // Nothing to do here at this point.
 }
 
-void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   // Nothing to do here at this point.
 }