5 files changed, 8 insertions, 6 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 3c96f7cf3..49e0e8e2f 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -1054,7 +1054,7 @@ bool LFSCBitVectorProof::hasAlias(Expr expr) {
   return d_assignedAliases.find(expr) != d_assignedAliases.end();
 }
 
-void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   Assert (c1.isConst());
   Assert (c2.isConst());
   Assert (utils::getSize(c1) == utils::getSize(c2));
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index f89774945..6b952e35c 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -157,7 +157,7 @@ public:
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
   void calculateAtomsInBitblastingProof();
   const std::set<Node>* getAtomsInBitblastingProof();
-  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
   void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 };
 
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 546d419fc..b172217d8 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -33,7 +33,8 @@ typedef std::pair<Node, Node> NodePair;
 typedef std::set<NodePair> NodePairSet;
 
 
-struct ProofLetCount {
+class ProofLetCount {
+public:
   static unsigned counter;
   static void resetCounter() { counter = 0; }
   static unsigned newId() { return ++counter; }
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eae8a68df..8aefaae45 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1167,7 +1167,8 @@ void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream&
 
 void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                              std::ostream& os,
-                                             std::ostream& paren) {
+                                             std::ostream& paren,
+                                             const ProofLetMap& map) {
   Unreachable("No boolean lemmas yet!");
 }
 
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index c622fabee..80a737580 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -308,7 +308,7 @@ public:
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 
   virtual void printOwnedSort(Type type, std::ostream& os) = 0;
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) = 0;
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
@@ -322,7 +322,7 @@ public:
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);