1 files changed, 10 insertions, 14 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index aa615f90e..4a292fc92 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -23,9 +23,9 @@
 
 namespace CVC4 {
 
-unsigned ProofArray::d_reasonRow;
-unsigned ProofArray::d_reasonRow1;
-unsigned ProofArray::d_reasonExt;
+unsigned ProofArray::s_reasonRow;
+unsigned ProofArray::s_reasonRow1;
+unsigned ProofArray::s_reasonExt;
 
 inline static Node eqNode(TNode n1, TNode n2) {
   return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
@@ -84,15 +84,15 @@ inline static bool match(TNode n1, TNode n2) {
 }
 
 void ProofArray::setRowMergeTag(unsigned tag) {
-  d_reasonRow = tag;
+  s_reasonRow = tag;
 }
 
 void ProofArray::setRow1MergeTag(unsigned tag) {
-  d_reasonRow1 = tag;
+  s_reasonRow1 = tag;
 }
 
 void ProofArray::setExtMergeTag(unsigned tag) {
-  d_reasonExt = tag;
+  s_reasonExt = tag;
 }
 
 void ProofArray::toStream(std::ostream& out) {
@@ -117,10 +117,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                                  unsigned tb,
                                  const LetMap& map) {
 
-  Debug("gk::temp") << "d_reasonExt = " << d_reasonExt << std::endl;
-  Debug("gk::temp") << "d_reasonRow = " << d_reasonRow << std::endl;
-  Debug("gk::temp") << "d_reasonRow1 = " << d_reasonRow1 << std::endl;
-
   Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::array");
   Debug("pf::array") << std::endl;
@@ -251,7 +247,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
     if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
 
-    if (pf->d_children[neg]->d_id == d_reasonExt) {
+    if (pf->d_children[neg]->d_id == s_reasonExt) {
       // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
 
       //      	    (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
@@ -828,7 +824,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return n1;
   }
 
-  else if (pf->d_id == d_reasonRow) {
+  else if (pf->d_id == s_reasonRow) {
     Debug("mgd") << "row lemma: " << pf->d_node << std::endl;
     Assert(pf->d_node.getKind() == kind::EQUAL);
 
@@ -974,7 +970,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     }
   }
 
-  else if (pf->d_id == d_reasonRow1) {
+  else if (pf->d_id == s_reasonRow1) {
     Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl;
     Assert(pf->d_node.getKind() == kind::EQUAL);
     TNode t1, t2, t3;
@@ -1009,7 +1005,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return ret;
   }
 
-  else if (pf->d_id == d_reasonExt) {
+  else if (pf->d_id == s_reasonExt) {
     theory::eq::EqProof *child_proof;
 
     Assert(pf->d_node.getKind() == kind::NOT);