Initial work towards -Wshadow (#3817)

38 files changed, 573 insertions, 421 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index d8dd2cf58..4f93ba745 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -639,14 +639,16 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
 RewriteResponse ArithRewriter::postRewrite(TNode t){
   if(isTerm(t)){
     RewriteResponse response = postRewriteTerm(t);
-    if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) {
-      Polynomial::parsePolynomial(response.node);
+    if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE)
+    {
+      Polynomial::parsePolynomial(response.d_node);
     }
     return response;
   }else if(isAtom(t)){
     RewriteResponse response = postRewriteAtom(t);
-    if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) {
-      Comparison::parseNormalForm(response.node);
+    if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE)
+    {
+      Comparison::parseNormalForm(response.d_node);
     }
     return response;
   }else{
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 94c925131..2d530d602 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -645,7 +645,7 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
   {
     nassertions++;
     const Assertion& assertion = *it;
-    Node lit = assertion.assertion;
+    Node lit = assertion.d_assertion;
     init_assertions.insert(lit);
     // check for concrete bounds
     bool pol = lit.getKind() != NOT;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 534a019c3..d721b7e7a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1327,14 +1327,15 @@ void TheoryArrays::check(Effort e) {
   {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
 
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
 
-    if (!assertion.isPreregistered) {
+    if (!assertion.d_isPreregistered)
+    {
       if (atom.getKind() == kind::EQUAL) {
         if (!d_equalityEngine.hasTerm(atom[0])) {
           Assert(atom[0].isConst());
diff --git a/src/theory/assertion.cpp b/src/theory/assertion.cpp
index 4f428e85c..97b3dcbbb 100644
--- a/src/theory/assertion.cpp
+++ b/src/theory/assertion.cpp
@@ -20,7 +20,7 @@ namespace CVC4 {
 namespace theory {
 
 std::ostream& operator<<(std::ostream& out, const Assertion& a) {
-  return out << a.assertion;
+  return out << a.d_assertion;
 }
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/assertion.h b/src/theory/assertion.h
index 863a7e893..797ff3372 100644
--- a/src/theory/assertion.h
+++ b/src/theory/assertion.h
@@ -28,19 +28,21 @@ namespace theory {
 /** Information about an assertion for the theories. */
 struct Assertion {
   /** The assertion expression. */
-  const Node assertion;
+  const Node d_assertion;
 
   /** Has this assertion been preregistered with this theory. */
-  const bool isPreregistered;
+  const bool d_isPreregistered;
 
   Assertion(TNode assertion, bool isPreregistered)
-      : assertion(assertion), isPreregistered(isPreregistered) {}
+      : d_assertion(assertion), d_isPreregistered(isPreregistered)
+  {
+  }
 
   /** Convert the assertion to a TNode. */
-  operator TNode() const { return assertion; }
+  operator TNode() const { return d_assertion; }
 
   /** Convert the assertion to a Node. */
-  operator Node() const { return assertion; }
+  operator Node() const { return d_assertion; }
 
 }; /* struct Assertion */
 
diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp
index 6054ac603..821c2384c 100644
--- a/src/theory/atom_requests.cpp
+++ b/src/theory/atom_requests.cpp
@@ -65,15 +65,13 @@ void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toT
   d_triggerToRequestMap[triggerAtom] = index;
 }
 
-bool AtomRequests::atom_iterator::done() const {
-  return index == null_index;
-}
+bool AtomRequests::atom_iterator::done() const { return d_index == null_index; }
 
 void AtomRequests::atom_iterator::next() {
-  index = requests.d_requests[index].previous;
+  d_index = d_requests.d_requests[d_index].d_previous;
 }
 
 const AtomRequests::Request& AtomRequests::atom_iterator::get() const {
-  return requests.d_requests[index].request;
+  return d_requests.d_requests[d_index].d_request;
 }
 
diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h
index 6a3ffe5e9..b96b042af 100644
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -34,24 +34,18 @@ public:
   /** Which atom and where to send it */
   struct Request {
     /** Atom */
-    Node atom;
+    Node d_atom;
     /** Where to send it */
-    theory::TheoryId toTheory;
+    theory::TheoryId d_toTheory;
 
-    Request(TNode atom, theory::TheoryId toTheory)
-    : atom(atom), toTheory(toTheory) {}
-    Request()
-    : toTheory(theory::THEORY_LAST)
-    {}
+    Request(TNode a, theory::TheoryId tt) : d_atom(a), d_toTheory(tt) {}
+    Request() : d_toTheory(theory::THEORY_LAST) {}
 
     bool operator == (const Request& other) const {
-      return atom == other.atom && toTheory == other.toTheory;
-    }
-
-    size_t hash() const {
-      return atom.getId();
+      return d_atom == other.d_atom && d_toTheory == other.d_toTheory;
     }
 
+    size_t hash() const { return d_atom.getId(); }
   };
 
   AtomRequests(context::Context* context);
@@ -66,11 +60,14 @@ public:
   typedef size_t element_index;
 
   class atom_iterator {
-    const AtomRequests& requests;
-    element_index index;
+    const AtomRequests& d_requests;
+    element_index d_index;
     friend class AtomRequests;
     atom_iterator(const AtomRequests& requests, element_index start)
-    : requests(requests), index(start) {}
+        : d_requests(requests), d_index(start)
+    {
+    }
+
   public:
     /** Is this iterator done  */
     bool done() const;
@@ -97,13 +94,11 @@ private:
 
   struct Element {
     /** Current request */
-    Request request;
+    Request d_request;
     /** Previous request */
-    element_index previous;
+    element_index d_previous;
 
-    Element(const Request& request, element_index previous)
-    : request(request), previous(previous)
-    {}
+    Element(const Request& r, element_index p) : d_request(r), d_previous(p) {}
   };
 
   /** We index the requests in this vector, it's a list */
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 1c5eab364..ca22467d4 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -169,7 +169,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     }
     if (!done) {
       RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt);
-      Debug("bool-flatten") << n << ": " << ret.node << std::endl;
+      Debug("bool-flatten") << n << ": " << ret.d_node << std::endl;
       return ret;
     }
     break;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 033a50916..94fc1e34c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -338,7 +338,7 @@ void TheoryBV::check(Effort e)
 
     std::vector<TNode> assertions;
     while (!done()) {
-      TNode fact = get().assertion;
+      TNode fact = get().d_assertion;
       Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
       assertions.push_back(fact);
       d_eagerSolver->assertFormula(fact[0]);
@@ -369,7 +369,7 @@ void TheoryBV::check(Effort e)
   }
 
   while (!done()) {
-    TNode fact = get().assertion;
+    TNode fact = get().d_assertion;
 
     checkForLemma(fact);
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 153f785ca..a7638325c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1382,12 +1382,11 @@ bool RewriteRule<BitwiseSlicing>::applies(TNode node) {
     if (node[i].getKind() == kind::CONST_BITVECTOR) {
       BitVector constant = node[i].getConst<BitVector>();
       // we do not apply the rule if the constant is all 0s or all 1s
-      if (constant == BitVector(utils::getSize(node), 0u)) 
-        return false; 
-      
-      for (unsigned i = 0; i < constant.getSize(); ++i) {
-        if (!constant.isBitSet(i)) 
-          return true; 
+      if (constant == BitVector(utils::getSize(node), 0u)) return false;
+
+      for (unsigned j = 0, csize = constant.getSize(); j < csize; ++j)
+      {
+        if (!constant.isBitSet(j)) return true;
       }
       return false; 
     }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 282ae2e27..6a04d6e4e 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -33,18 +33,22 @@ TheoryBVRewriter::TheoryBVRewriter() { initializeRewrites(); }
 
 RewriteResponse TheoryBVRewriter::preRewrite(TNode node) {
   RewriteResponse res = d_rewriteTable[node.getKind()](node, true);
-  if(res.node != node) {
+  if (res.d_node != node)
+  {
     Debug("bitvector-rewrite") << "TheoryBV::preRewrite    " << node << std::endl;
-    Debug("bitvector-rewrite") << "TheoryBV::preRewrite to " << res.node << std::endl;
+    Debug("bitvector-rewrite")
+        << "TheoryBV::preRewrite to " << res.d_node << std::endl;
   }
   return res; 
 }
 
 RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   RewriteResponse res = d_rewriteTable[node.getKind()](node, false);
-  if(res.node!= node) {
+  if (res.d_node != node)
+  {
     Debug("bitvector-rewrite") << "TheoryBV::postRewrite    " << node << std::endl;
-    Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl;
+    Debug("bitvector-rewrite")
+        << "TheoryBV::postRewrite to " << res.d_node << std::endl;
   }
   return res; 
 }
diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h
index 55851c1a4..f17f67ee0 100644
--- a/src/theory/care_graph.h
+++ b/src/theory/care_graph.h
@@ -31,22 +31,25 @@ namespace theory {
  * A (ordered) pair of terms a theory cares about.
  */
 struct CarePair {
-  const TNode a, b;
-  const TheoryId theory;
+  const TNode d_a, d_b;
+  const TheoryId d_theory;
 
   CarePair(TNode a, TNode b, TheoryId theory)
-      : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {}
+      : d_a(a < b ? a : b), d_b(a < b ? b : a), d_theory(theory)
+  {
+  }
 
   bool operator==(const CarePair& other) const {
-    return (theory == other.theory) && (a == other.a) && (b == other.b);
+    return (d_theory == other.d_theory) && (d_a == other.d_a)
+           && (d_b == other.d_b);
   }
 
   bool operator<(const CarePair& other) const {
-    if (theory < other.theory) return true;
-    if (theory > other.theory) return false;
-    if (a < other.a) return true;
-    if (a > other.a) return false;
-    return b < other.b;
+    if (d_theory < other.d_theory) return true;
+    if (d_theory > other.d_theory) return false;
+    if (d_a < other.d_a) return true;
+    if (d_a > other.d_a) return false;
+    return d_b < other.d_b;
   }
 
 }; /* struct CarePair */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index cf07bc0c1..141c9476f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -154,7 +154,7 @@ void TheoryDatatypes::check(Effort e) {
   while(!done() && !d_conflict) {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
     Trace("datatypes-assert") << "Assert " << fact << std::endl;
 
     TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 788545b3c..2632a6f38 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -962,7 +962,7 @@ void TheoryFp::check(Effort level) {
   while (!done() && !d_conflict) {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
 
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 8854b400d..338c1c871 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -46,9 +46,12 @@ namespace rewrite {
   RewriteResponse then (TNode node, bool isPreRewrite) {
     RewriteResponse result(first(node, isPreRewrite));
 
-    if (result.status == REWRITE_DONE) {
-      return second(result.node, isPreRewrite);
-    } else {
+    if (result.d_status == REWRITE_DONE)
+    {
+      return second(result.d_node, isPreRewrite);
+    }
+    else
+    {
       return result;
     }
   }
@@ -1268,9 +1271,11 @@ TheoryFpRewriter::TheoryFpRewriter()
   RewriteResponse TheoryFpRewriter::preRewrite(TNode node) {
     Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl;
     RewriteResponse res = d_preRewriteTable[node.getKind()](node, true);
-    if (res.node != node) {
+    if (res.d_node != node)
+    {
       Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl;
-      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  " << res.node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  "
+                          << res.d_node << std::endl;
     }
     return res;
   }
@@ -1301,46 +1306,52 @@ TheoryFpRewriter::TheoryFpRewriter()
   RewriteResponse TheoryFpRewriter::postRewrite(TNode node) {
     Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl;
     RewriteResponse res = d_postRewriteTable[node.getKind()](node, false);
-    if (res.node != node) {
+    if (res.d_node != node)
+    {
       Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl;
-      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  " << res.node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  "
+                          << res.d_node << std::endl;
     }
 
-    if (res.status == REWRITE_DONE) {
+    if (res.d_status == REWRITE_DONE)
+    {
       bool allChildrenConst = true;
       bool apartFromRoundingMode = false;
       bool apartFromPartiallyDefinedArgument = false;
-      for (Node::const_iterator i = res.node.begin();
-	   i != res.node.end();
-	   ++i) {
-
-	if ((*i).getMetaKind() != kind::metakind::CONSTANT) {
+      for (Node::const_iterator i = res.d_node.begin(); i != res.d_node.end();
+           ++i)
+      {
+        if ((*i).getMetaKind() != kind::metakind::CONSTANT) {
 	  if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) {
 	    apartFromRoundingMode = true;
-	  } else if ((res.node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) &&
-		     ((*i).getType().isBitVector() ||
-		      (*i).getType().isReal()) &&
-		     !apartFromPartiallyDefinedArgument) {
-	    apartFromPartiallyDefinedArgument = true;
-	  } else {
-	    allChildrenConst = false;
+          }
+          else if ((res.d_node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL
+                    || res.d_node.getKind()
+                           == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+                   && ((*i).getType().isBitVector() || (*i).getType().isReal())
+                   && !apartFromPartiallyDefinedArgument)
+          {
+            apartFromPartiallyDefinedArgument = true;
+          }
+          else
+          {
+            allChildrenConst = false;
 	    break;
-	  }
-	}
+          }
+        }
       }
 
       if (allChildrenConst) {
 	RewriteStatus rs = REWRITE_DONE;    // This is a bit messy because
-	Node rn = res.node;                 // RewriteResponse is too functional..
+        Node rn = res.d_node;  // RewriteResponse is too functional..
 
-	if (apartFromRoundingMode) {
-          if (!(res.node.getKind() == kind::EQUAL)
+        if (apartFromRoundingMode) {
+          if (!(res.d_node.getKind() == kind::EQUAL)
               &&  // Avoid infinite recursion...
-              !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST))
+              !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST))
           {  // Don't eliminate the bit-blast
             // We are close to being able to constant fold this
             // and in many cases the rounding mode really doesn't matter.
@@ -1354,16 +1365,15 @@ TheoryFpRewriter::TheoryFpRewriter()
 	    Node RTN(nm->mkConst(roundTowardNegative));
 	    Node RTP(nm->mkConst(roundTowardZero));
 
-	    TNode RM(res.node[0]);
-
-	    Node wRNE(res.node.substitute(RM, TNode(RNE)));
-	    Node wRNA(res.node.substitute(RM, TNode(RNA)));
-	    Node wRTZ(res.node.substitute(RM, TNode(RTZ)));
-	    Node wRTN(res.node.substitute(RM, TNode(RTN)));
-	    Node wRTP(res.node.substitute(RM, TNode(RTP)));
+            TNode RM(res.d_node[0]);
 
+            Node wRNE(res.d_node.substitute(RM, TNode(RNE)));
+            Node wRNA(res.d_node.substitute(RM, TNode(RNA)));
+            Node wRTZ(res.d_node.substitute(RM, TNode(RTZ)));
+            Node wRTN(res.d_node.substitute(RM, TNode(RTN)));
+            Node wRTP(res.d_node.substitute(RM, TNode(RTP)));
 
-	    rs = REWRITE_AGAIN_FULL;
+            rs = REWRITE_AGAIN_FULL;
 	    rn = nm->mkNode(kind::ITE,
 			    nm->mkNode(kind::EQUAL, RM, RNE),
 			    wRNE,
@@ -1380,19 +1390,24 @@ TheoryFpRewriter::TheoryFpRewriter()
 	  }
 	} else {
           RewriteResponse tmp =
-              d_constantFoldTable[res.node.getKind()](res.node, false);
-          rs = tmp.status;
-          rn = tmp.node;
-	}
+              d_constantFoldTable[res.d_node.getKind()](res.d_node, false);
+          rs = tmp.d_status;
+          rn = tmp.d_node;
+        }
 
 	RewriteResponse constRes(rs,rn);
 
-	if (constRes.node != res.node) {
-	  Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before constant fold " << res.node << std::endl;
-	  Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after constant fold " << constRes.node << std::endl;
-	}
-
-	return constRes;
+        if (constRes.d_node != res.d_node)
+        {
+          Debug("fp-rewrite")
+              << "TheoryFpRewriter::postRewrite(): before constant fold "
+              << res.d_node << std::endl;
+          Debug("fp-rewrite")
+              << "TheoryFpRewriter::postRewrite(): after constant fold "
+              << constRes.d_node << std::endl;
+        }
+
+        return constRes;
       }
     }
 
diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
index 790e9d83d..732eeab0a 100644
--- a/src/theory/fp/theory_fp_rewriter.h
+++ b/src/theory/fp/theory_fp_rewriter.h
@@ -42,7 +42,7 @@ class TheoryFpRewriter : public TheoryRewriter
   Node rewriteEquality(TNode equality)
   {
     // often this will suffice
-    return postRewrite(equality).node;
+    return postRewrite(equality).d_node;
   }
 
  protected:
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 12ac1e802..f92738bcb 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -62,10 +62,11 @@ void TheoryIdl::check(Effort level) {
 
     // Get the next assertion
     Assertion assertion = get();
-    Debug("theory::idl") << "TheoryIdl::check(): processing " << assertion.assertion << std::endl;
+    Debug("theory::idl") << "TheoryIdl::check(): processing "
+                         << assertion.d_assertion << std::endl;
 
     // Convert the assertion into the internal representation
-    IDLAssertion idlAssertion(assertion.assertion);
+    IDLAssertion idlAssertion(assertion.d_assertion);
     Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl;
 
     if (idlAssertion.ok()) {
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 4f3ce4327..34e66da9e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1448,7 +1448,7 @@ void CegInstantiator::processAssertions() {
       d_curr_asserts[tid].clear();
       //collect all assertions from theory
       for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
-        Node lit = (*it).assertion;
+        Node lit = (*it).d_assertion;
         Node atom = lit.getKind()==NOT ? lit[0] : lit;
         if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
           d_curr_asserts[tid].push_back( lit );
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index aa3efca19..fecefb8e1 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -211,8 +211,8 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
         }
       }else{
         //simplify term
-        std::map<Node, Node> visited;
-        getConstraints(n, constraints, visited);
+        std::map<Node, Node> visitedT;
+        getConstraints(n, constraints, visitedT);
       }
       if( !constraints.empty() && isBool && hasPol ){
         //conjoin with current
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 1d1eb9751..11b9bd14b 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -339,7 +339,6 @@ bool Instantiate::addInstantiation(
   }
   if (options::trackInstLemmas())
   {
-    bool recorded;
     if (options::incrementalSolving())
     {
       recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index d1bd5db63..ad281b009 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -823,9 +823,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
             //   "Let W be a subset of D such that S ^ W is unsat."
             // and uasserts is set to W.
             uasserts.clear();
-            std::unordered_set<Node, NodeHashFunction> queryAsserts;
-            queryAsserts.insert(d_sc);
-            getUnsatCore(checkSc, queryAsserts, uasserts);
+            std::unordered_set<Node, NodeHashFunction> queryAsserts2;
+            queryAsserts2.insert(d_sc);
+            getUnsatCore(checkSc, queryAsserts2, uasserts);
             falseCore = true;
           }
         }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index dc290d4ba..7c1451771 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -229,9 +229,9 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
         // the lemmas must be guarded by the active guard of the enumerator
         Node g = d_tds->getActiveGuardForEnumerator(e);
         Assert(!g.isNull());
-        for (unsigned j = 0, size = enum_lems.size(); j < size; j++)
+        for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
         {
-          enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
+          enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]);
         }
         lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
       }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b78263f0e..444d6f329 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1100,8 +1100,9 @@ bool TermDb::reset( Theory::Effort effort ){
       if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (unsigned i = 0; it != it_end; ++ it, ++i) {
-          if( (*it).assertion.getKind()!=INST_CLOSURE ){
-            setHasTerm( (*it).assertion );
+          if ((*it).d_assertion.getKind() != INST_CLOSURE)
+          {
+            setHasTerm((*it).d_assertion);
           }
         }
       }
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 1682b4d0c..227f4d5b5 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -95,13 +95,17 @@ void TheoryQuantifiers::ppNotifyAssertions(
 bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
 {
   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
-    if((*i).assertion.getKind() == kind::NOT) {
-      Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
-      if (!m->assertPredicate((*i).assertion[0], false))
+    if ((*i).d_assertion.getKind() == kind::NOT)
+    {
+      Debug("quantifiers::collectModelInfo")
+          << "got quant FALSE: " << (*i).d_assertion[0] << endl;
+      if (!m->assertPredicate((*i).d_assertion[0], false))
       {
         return false;
       }
-    } else {
+    }
+    else
+    {
       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
       if (!m->assertPredicate(*i, true))
       {
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 2a7c3ff0d..e5d6748aa 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -156,11 +156,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
               d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite(
                   rewriteStackTop.node);
           // Put the rewritten node to the top of the stack
-          rewriteStackTop.node = response.node;
+          rewriteStackTop.node = response.d_node;
           TheoryId newTheory = theoryOf(rewriteStackTop.node);
           // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
           if (newTheory == rewriteStackTop.getTheoryId()
-              && response.status == REWRITE_DONE)
+              && response.d_status == REWRITE_DONE)
           {
             break;
           }
@@ -225,41 +225,42 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
             d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite(
                 rewriteStackTop.node);
         // We continue with the response we got
-        TheoryId newTheoryId = theoryOf(response.node);
+        TheoryId newTheoryId = theoryOf(response.d_node);
         if (newTheoryId != rewriteStackTop.getTheoryId()
-            || response.status == REWRITE_AGAIN_FULL)
+            || response.d_status == REWRITE_AGAIN_FULL)
         {
           // In the post rewrite if we've changed theories, we must do a full rewrite
-          Assert(response.node != rewriteStackTop.node);
+          Assert(response.d_node != rewriteStackTop.node);
           //TODO: this is not thread-safe - should make this assertion dependent on sequential build
 #ifdef CVC4_ASSERTIONS
-          Assert(d_rewriteStack->find(response.node) == d_rewriteStack->end());
-          d_rewriteStack->insert(response.node);
+          Assert(d_rewriteStack->find(response.d_node)
+                 == d_rewriteStack->end());
+          d_rewriteStack->insert(response.d_node);
 #endif
-          Node rewritten = rewriteTo(newTheoryId, response.node);
+          Node rewritten = rewriteTo(newTheoryId, response.d_node);
           rewriteStackTop.node = rewritten;
 #ifdef CVC4_ASSERTIONS
-          d_rewriteStack->erase(response.node);
+          d_rewriteStack->erase(response.d_node);
 #endif
           break;
         }
-        else if (response.status == REWRITE_DONE)
+        else if (response.d_status == REWRITE_DONE)
         {
 #ifdef CVC4_ASSERTIONS
           RewriteResponse r2 =
-              d_theoryRewriters[newTheoryId]->postRewrite(response.node);
-          Assert(r2.node == response.node);
+              d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
+          Assert(r2.d_node == response.d_node);
 #endif
-	  rewriteStackTop.node = response.node;
+          rewriteStackTop.node = response.d_node;
           break;
         }
         // Check for trivial rewrite loops of size 1 or 2
-        Assert(response.node != rewriteStackTop.node);
+        Assert(response.d_node != rewriteStackTop.node);
         Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
-                   ->postRewrite(response.node)
-                   .node
+                   ->postRewrite(response.d_node)
+                   .d_node
                != rewriteStackTop.node);
-        rewriteStackTop.node = response.node;
+        rewriteStackTop.node = response.d_node;
       }
       // We're done with the post rewrite, so we add to the cache
       setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index b5fc1cbc9..0b6e7a5fb 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -317,7 +317,7 @@ void TheorySep::check(Effort e) {
   while( !done() && !d_conflict ){
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl;
 
@@ -806,7 +806,7 @@ void TheorySep::check(Effort e) {
         d_heap_locs_nptos.clear();
         //collect data points that are not pointed to
         for( context::CDList<Assertion>::const_iterator it = facts_begin(); it != facts_end(); ++ it) {
-          Node lit = (*it).assertion;
+          Node lit = (*it).d_assertion;
           if( lit.getKind()==kind::NOT && lit[0].getKind()==kind::SEP_PTO ){
             Node s_atom = lit[0];
             Node v1 = d_valuation.getModel()->getRepresentative( s_atom[0] );
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f1a11baf8..df6f76cbf 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -955,7 +955,7 @@ void TheorySetsPrivate::check(Theory::Effort level)
   {
     // Get all the assertions
     Assertion assertion = d_external.get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
     Trace("sets-assert") << "Assert from input " << fact << std::endl;
     // assert the fact
     assertFact(fact, fact);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d8f5f8c4f..114dfa9a6 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -62,7 +62,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   case kind::MEMBER: {
     if(node[0].isConst() && node[1].isConst()) {
       // both are constants
-      TNode S = preRewrite(node[1]).node;
+      TNode S = preRewrite(node[1]).d_node;
       bool isMember = checkConstantMembership(node[0], S);
       return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
     }else if( node[1].getKind()==kind::EMPTYSET ){
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index b6c14e30a..3d96e4ece 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -68,7 +68,7 @@ class TheorySetsRewriter : public TheoryRewriter
   Node rewriteEquality(TNode equality)
   {
     // often this will suffice
-    return postRewrite(equality).node;
+    return postRewrite(equality).d_node;
   }
 
 }; /* class TheorySetsRewriter */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 92af3cc0a..c2790fe42 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -620,7 +620,7 @@ void TheoryStrings::check(Effort e) {
   {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
     polarity = fact.getKind() != kind::NOT;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 36db0fda8..d6b02e070 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -867,7 +867,7 @@ inline theory::Assertion Theory::get() {
   Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
 
   if(Dump.isOn("state")) {
-    Dump("state") << AssertCommand(fact.assertion.toExpr());
+    Dump("state") << AssertCommand(fact.d_assertion.toExpr());
   }
 
   return fact;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index dec648688..d176b015d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -472,12 +472,15 @@ void TheoryEngine::printAssertions(const char* tag) {
         Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (unsigned i = 0; it != it_end; ++ it, ++i) {
-            if ((*it).isPreregistered) {
-              Trace(tag) << "[" << i << "]: ";
-            } else {
-              Trace(tag) << "(" << i << "): ";
-            }
-            Trace(tag) << (*it).assertion << endl;
+          if ((*it).d_isPreregistered)
+          {
+            Trace(tag) << "[" << i << "]: ";
+          }
+          else
+          {
+            Trace(tag) << "(" << i << "): ";
+          }
+          Trace(tag) << (*it).d_assertion << endl;
         }
 
         if (d_logicInfo.isSharingEnabled()) {
@@ -517,12 +520,15 @@ void TheoryEngine::dumpAssertions(const char* tag) {
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (; it != it_end; ++ it) {
           // Get the assertion
-          Node assertionNode = (*it).assertion;
+          Node assertionNode = (*it).d_assertion;
           // Purify all the terms
 
-          if ((*it).isPreregistered) {
+          if ((*it).d_isPreregistered)
+          {
             Dump(tag) << CommentCommand("Preregistered");
-          } else {
+          }
+          else
+          {
             Dump(tag) << CommentCommand("Shared assertion");
           }
           Dump(tag) << AssertCommand(assertionNode.toExpr());
@@ -725,14 +731,16 @@ void TheoryEngine::combineTheories() {
   for (; care_it != care_it_end; ++ care_it) {
     const CarePair& carePair = *care_it;
 
-    Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl;
+    Debug("combineTheories")
+        << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
+        << carePair.d_b << " from " << carePair.d_theory << endl;
 
-    Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst());
-    Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst());
+    Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst());
+    Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst());
 
     // The equality in question (order for no repetition)
-    Node equality = carePair.a.eqNode(carePair.b);
-    // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b);
+    Node equality = carePair.d_a.eqNode(carePair.d_b);
+    // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
     // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
     //   (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
     //   es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
@@ -746,7 +754,12 @@ void TheoryEngine::combineTheories() {
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
 
-    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory);
+    lemma(equality.orNode(equality.notNode()),
+          RULE_INVALID,
+          false,
+          false,
+          false,
+          carePair.d_theory);
 
     // This code is supposed to force preference to follow what the theory models already have
     // but it doesn't seem to make a big difference - need to explore more -Clark
@@ -1440,9 +1453,11 @@ void TheoryEngine::assertFact(TNode literal)
       AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
       while (!it.done()) {
         const AtomRequests::Request& request = it.get();
-        Node toAssert = polarity ? (Node) request.atom : request.atom.notNode();
+        Node toAssert =
+            polarity ? (Node)request.d_atom : request.d_atom.notNode();
         Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
-        assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER);
+        assertToTheory(
+            toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
         it.next();
       }
 
@@ -1621,8 +1636,8 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;
   for (unsigned i = 0; i < explanation.size(); ++ i) {
-    Assert(explanation[i].theory == THEORY_SAT_SOLVER);
-    all.insert(explanation[i].node);
+    Assert(explanation[i].d_theory == THEORY_SAT_SOLVER);
+    all.insert(explanation[i].d_node);
   }
 
   if (all.size() == 0) {
@@ -1632,7 +1647,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   if (all.size() == 1) {
     // All the same, or just one
-    return explanation[0].node;
+    return explanation[0].d_node;
   }
 
   NodeBuilder<> conjunction(kind::AND);
@@ -1710,10 +1725,11 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
 
   NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
-  Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
-                           << nodeExplainerPair.node
-                           << " is theory: " << nodeExplainerPair.theory << std::endl;
-  TheoryId explainer = nodeExplainerPair.theory;
+  Debug("theory::explain")
+      << "TheoryEngine::getExplanation: explainer for node "
+      << nodeExplainerPair.d_node
+      << " is theory: " << nodeExplainerPair.d_theory << std::endl;
+  TheoryId explainer = nodeExplainerPair.d_theory;
 
   // Create the workplace for explanations
   std::vector<NodeTheoryPair> explanationVector;
@@ -2061,31 +2077,42 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     // Get the current literal to explain
     NodeTheoryPair toExplain = explanationVector[i];
 
-    Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
-
+    Debug("theory::explain")
+        << "[i=" << i << "] TheoryEngine::explain(): processing ["
+        << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
+        << toExplain.d_theory << endl;
 
     // If a true constant or a negation of a false constant we can ignore it
-    if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
+    if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
+    {
       ++ i;
       continue;
     }
-    if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
+    if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
+        && !toExplain.d_node[0].getConst<bool>())
+    {
       ++ i;
       continue;
     }
 
     // If from the SAT solver, keep it
-    if (toExplain.theory == THEORY_SAT_SOLVER) {
+    if (toExplain.d_theory == THEORY_SAT_SOLVER)
+    {
       Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
       explanationVector[j++] = explanationVector[i++];
       continue;
     }
 
     // If an and, expand it
-    if (toExplain.node.getKind() == kind::AND) {
-      Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl;
-      for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) {
-        NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp);
+    if (toExplain.d_node.getKind() == kind::AND)
+    {
+      Debug("theory::explain")
+          << "TheoryEngine::explain(): expanding " << toExplain.d_node
+          << " got from " << toExplain.d_theory << endl;
+      for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k)
+      {
+        NodeTheoryPair newExplain(
+            toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
         explanationVector.push_back(newExplain);
       }
       ++ i;
@@ -2097,24 +2124,31 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     if (find != d_propagationMap.end()) {
       Debug("theory::explain")
           << "\tTerm was propagated by another theory (theory = "
-          << getTheoryString((*find).second.theory) << ")" << std::endl;
+          << getTheoryString((*find).second.d_theory) << ")" << std::endl;
       // There is some propagation, check if its a timely one
-      if ((*find).second.timestamp < toExplain.timestamp) {
-        Debug("theory::explain") << "\tRelevant timetsamp, pushing "
-                                 << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
+      if ((*find).second.d_timestamp < toExplain.d_timestamp)
+      {
+        Debug("theory::explain")
+            << "\tRelevant timetsamp, pushing " << (*find).second.d_node
+            << "to index = " << explanationVector.size() << std::endl;
         explanationVector.push_back((*find).second);
         ++i;
 
         PROOF({
-            if (toExplain.node != (*find).second.node) {
-              Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
-                                   << ", toExplain = " << (*find).second.node << std::endl;
+          if (toExplain.d_node != (*find).second.d_node)
+          {
+            Debug("pf::explain")
+                << "TheoryEngine::getExplanation: Rewrite alert! toAssert = "
+                << toExplain.d_node << ", toExplain = " << (*find).second.d_node
+                << std::endl;
 
-              if (proofRecipe) {
-                proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
-              }
+            if (proofRecipe)
+            {
+              proofRecipe->addRewriteRule(toExplain.d_node,
+                                          (*find).second.d_node);
             }
-          })
+          }
+        })
 
         continue;
       }
@@ -2122,21 +2156,27 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
     // It was produced by the theory, so ask for an explanation
     Node explanation;
-    if (toExplain.theory == THEORY_BUILTIN) {
-      explanation = d_sharedTerms.explain(toExplain.node);
+    if (toExplain.d_theory == THEORY_BUILTIN)
+    {
+      explanation = d_sharedTerms.explain(toExplain.d_node);
       Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
-    } else {
-      explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
+    }
+    else
+    {
+      explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
       Debug("theory::explain") << "\tTerm was propagated by owner theory: "
-                               << theoryOf(toExplain.theory)->getId()
+                               << theoryOf(toExplain.d_theory)->getId()
                                << ". Explanation: " << explanation << std::endl;
     }
 
-    Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
-    Assert(explanation != toExplain.node)
+    Debug("theory::explain")
+        << "TheoryEngine::explain(): got explanation " << explanation
+        << " got from " << toExplain.d_theory << endl;
+    Assert(explanation != toExplain.d_node)
         << "wasn't sent to you, so why are you explaining it trivially";
     // Mark the explanation
-    NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
+    NodeTheoryPair newExplain(
+        explanation, toExplain.d_theory, toExplain.d_timestamp);
     explanationVector.push_back(newExplain);
 
     ++ i;
@@ -2147,10 +2187,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         // If we're expanding the target node of the explanation (this is the
         // first expansion...), we don't want to add it as a separate proof
         // step. It is already part of the assertions.
-        if (!ContainsKey(*inputAssertions, toExplain.node))
+        if (!ContainsKey(*inputAssertions, toExplain.d_node))
         {
-          LemmaProofRecipe::ProofStep proofStep(toExplain.theory,
-                                                toExplain.node);
+          LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory,
+                                                toExplain.d_node);
           if (explanation.getKind() == kind::AND)
           {
             Node flat = flattenAnd(explanation);
@@ -2189,7 +2229,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
       if (proofRecipe) {
         // The remaining literals are the base of the proof
         for (unsigned k = 0; k < explanationVector.size(); ++k) {
-          proofRecipe->addBaseAssertion(explanationVector[k].node.negate());
+          proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate());
         }
       }
     });
@@ -2224,7 +2264,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
             it_end = theory->facts_end();
           it != it_end;
           ++it) {
-        Node assertion = (*it).assertion;
+        Node assertion = (*it).d_assertion;
         Node val = getModel()->getValue(assertion);
         if (val != d_true)
         {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a5631059f..1757d7a6d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -60,15 +60,17 @@ class LemmaProofRecipe;
  * propagations between theories.
  */
 struct NodeTheoryPair {
-  Node node;
-  theory::TheoryId theory;
-  size_t timestamp;
-  NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0)
-  : node(node), theory(theory), timestamp(timestamp) {}
-  NodeTheoryPair() : theory(theory::THEORY_LAST), timestamp() {}
+  Node d_node;
+  theory::TheoryId d_theory;
+  size_t d_timestamp;
+  NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0)
+      : d_node(n), d_theory(t), d_timestamp(ts)
+  {
+  }
+  NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {}
   // Comparison doesn't take into account the timestamp
   bool operator == (const NodeTheoryPair& pair) const {
-    return node == pair.node && theory == pair.theory;
+    return d_node == pair.d_node && d_theory == pair.d_theory;
   }
 };/* struct NodeTheoryPair */
 
@@ -76,8 +78,8 @@ struct NodeTheoryPairHashFunction {
   NodeHashFunction hashFunction;
   // Hash doesn't take into account the timestamp
   size_t operator()(const NodeTheoryPair& pair) const {
-    uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.node));
-    return static_cast<size_t>(fnv1a::fnv1a_64(pair.theory, hash));
+    uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
+    return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
   }
 };/* struct NodeTheoryPairHashFunction */
 
diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index 61f0fc27a..e7dc782bb 100644
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -46,11 +46,9 @@ enum RewriteStatus
  */
 struct RewriteResponse
 {
-  const RewriteStatus status;
-  const Node node;
-  RewriteResponse(RewriteStatus status, Node node) : status(status), node(node)
-  {
-  }
+  const RewriteStatus d_status;
+  const Node d_node;
+  RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
 }; /* struct RewriteResponse */
 
 /**
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 8e0c96ae3..63aa81097 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -24,22 +24,22 @@ namespace theory {
 namespace eq {
 
 EqualityEngine::Statistics::Statistics(std::string name)
-    : mergesCount(name + "::mergesCount", 0),
-      termsCount(name + "::termsCount", 0),
-      functionTermsCount(name + "::functionTermsCount", 0),
-      constantTermsCount(name + "::constantTermsCount", 0)
+    : d_mergesCount(name + "::mergesCount", 0),
+      d_termsCount(name + "::termsCount", 0),
+      d_functionTermsCount(name + "::functionTermsCount", 0),
+      d_constantTermsCount(name + "::constantTermsCount", 0)
 {
-  smtStatisticsRegistry()->registerStat(&mergesCount);
-  smtStatisticsRegistry()->registerStat(&termsCount);
-  smtStatisticsRegistry()->registerStat(&functionTermsCount);
-  smtStatisticsRegistry()->registerStat(&constantTermsCount);
+  smtStatisticsRegistry()->registerStat(&d_mergesCount);
+  smtStatisticsRegistry()->registerStat(&d_termsCount);
+  smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
+  smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
 }
 
 EqualityEngine::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&mergesCount);
-  smtStatisticsRegistry()->unregisterStat(&termsCount);
-  smtStatisticsRegistry()->unregisterStat(&functionTermsCount);
-  smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
+  smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
+  smtStatisticsRegistry()->unregisterStat(&d_termsCount);
+  smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
+  smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
 }
 
 /**
@@ -47,28 +47,31 @@ EqualityEngine::Statistics::~Statistics() {
  */
 struct BfsData {
   // The current node
-  EqualityNodeId nodeId;
+  EqualityNodeId d_nodeId;
   // The index of the edge we traversed
-  EqualityEdgeId edgeId;
+  EqualityEdgeId d_edgeId;
   // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
   // of the biggest equivalence class
-  size_t previousIndex;
+  size_t d_previousIndex;
 
-  BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0)
-  : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {}
+  BfsData(EqualityNodeId nodeId = null_id,
+          EqualityEdgeId edgeId = null_edge,
+          size_t prev = 0)
+      : d_nodeId(nodeId), d_edgeId(edgeId), d_previousIndex(prev)
+  {
+  }
 };
 
 class ScopedBool {
-  bool& watch;
-  bool oldValue;
-public:
-  ScopedBool(bool& watch, bool newValue)
-  : watch(watch), oldValue(watch) {
-    watch = newValue;
-  }
-  ~ScopedBool() {
-    watch = oldValue;
+  bool& d_watch;
+  bool d_oldValue;
+
+ public:
+  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
+  {
+    d_watch = newValue;
   }
+  ~ScopedBool() { d_watch = d_oldValue; }
 };
 
 EqualityEngineNotifyNone EqualityEngine::s_notifyNone;
@@ -158,7 +161,10 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
-  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl;
+  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.d_t1Id]
+                    << ", " << d_nodes[candidate.d_t2Id] << ", "
+                    << candidate.d_type << "). reason: " << candidate.d_reason
+                    << std::endl;
   if (back) {
     d_propagationQueue.push_back(candidate);
   } else {
@@ -169,7 +175,7 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
 EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) {
   Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
 
-  ++ d_stats.functionTermsCount;
+  ++d_stats.d_functionTermsCount;
 
   // Get another id for this
   EqualityNodeId funId = newNode(original);
@@ -211,7 +217,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
   Debug("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl;
 
-  ++ d_stats.termsCount;
+  ++d_stats.d_termsCount;
 
   // Register the new id of the term
   EqualityNodeId newId = d_nodes.size();
@@ -477,8 +483,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
       TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef);
       TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef);
       // Go through and notify the shared dis-equalities
-      Theory::Set aTags = aTriggerTerms.tags;
-      Theory::Set bTags = bTriggerTerms.tags;
+      Theory::Set aTags = aTriggerTerms.d_tags;
+      Theory::Set bTags = bTriggerTerms.d_tags;
       TheoryId aTag = Theory::setPop(aTags);
       TheoryId bTag = Theory::setPop(bTags);
       int a_i = 0, b_i = 0;
@@ -491,8 +497,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
           ++ b_i;
         } else {
           // Same tags, notify
-          EqualityNodeId aSharedId = aTriggerTerms.triggers[a_i++];
-          EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++];
+          EqualityNodeId aSharedId = aTriggerTerms.d_triggers[a_i++];
+          EqualityNodeId bSharedId = bTriggerTerms.d_triggers[b_i++];
           // Propagate
           if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) {
             // Store a proof if not there already
@@ -533,7 +539,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   Assert(triggersFired.empty());
 
-  ++ d_stats.mergesCount;
+  ++d_stats.d_mergesCount;
 
   EqualityNodeId class1Id = class1.getFind();
   EqualityNodeId class2Id = class2.getFind();
@@ -562,10 +568,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // Trigger set of class 1
   TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
-  Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).tags;
+  Theory::Set class1Tags = class1triggerRef == null_set_id
+                               ? 0
+                               : getTriggerTermSet(class1triggerRef).d_tags;
   // Trigger set of class 2
   TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
-  Theory::Set class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).tags;
+  Theory::Set class2Tags = class2triggerRef == null_set_id
+                               ? 0
+                               : getTriggerTermSet(class2triggerRef).d_tags;
 
   // Disequalities coming from class2
   TaggedEqualitiesSet class2disequalitiesToNotify;
@@ -600,17 +610,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
 
       // If the two are not already in the same class
-      if (otherTrigger.classId != trigger.classId) {
-        trigger.classId = class1Id;
+      if (otherTrigger.d_classId != trigger.d_classId)
+      {
+        trigger.d_classId = class1Id;
         // If they became the same, call the trigger
-        if (otherTrigger.classId == class1Id) {
+        if (otherTrigger.d_classId == class1Id)
+        {
           // Id of the real trigger is half the internal one
           triggersFired.push_back(currentTrigger);
         }
       }
 
       // Go to the next trigger
-      currentTrigger = trigger.nextTrigger;
+      currentTrigger = trigger.d_nextTrigger;
     }
 
     // Move to the next node
@@ -635,17 +647,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         // Get the function application
         EqualityNodeId funId = useNode.getApplicationId();
         Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
-        const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
+        const FunctionApplication& fun =
+            d_applications[useNode.getApplicationId()].d_normalized;
         // If it's interpreted and we can interpret
-  if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
-    // Get the actual term id
-    TNode term = d_nodes[funId];
-    subtermEvaluates(getNodeId(term));
-  }
-  // Check if there is an application with find arguments
-        EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
-        EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
-        FunctionApplication funNormalized(fun.type, aNormalized, bNormalized);
+        if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId])
+        {
+          // Get the actual term id
+          TNode term = d_nodes[funId];
+          subtermEvaluates(getNodeId(term));
+        }
+        // Check if there is an application with find arguments
+        EqualityNodeId aNormalized = getEqualityNode(fun.d_a).getFind();
+        EqualityNodeId bNormalized = getEqualityNode(fun.d_b).getFind();
+        FunctionApplication funNormalized(fun.d_type, aNormalized, bNormalized);
         ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
         if (find != d_applicationLookup.end()) {
           // Applications fun and the funNormalized can be merged due to congruence
@@ -696,14 +710,15 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
 
       // Initialize the merged set
-      Theory::Set newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags);
+      Theory::Set newSetTags =
+          Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags);
       EqualityNodeId newSetTriggers[THEORY_LAST];
       unsigned newSetTriggersSize = 0;
 
       int i1 = 0;
       int i2 = 0;
-      Theory::Set tags1 = class1triggers.tags;
-      Theory::Set tags2 = class2triggers.tags;
+      Theory::Set tags1 = class1triggers.d_tags;
+      Theory::Set tags2 = class2triggers.d_tags;
       TheoryId tag1 = Theory::setPop(tags1);
       TheoryId tag2 = Theory::setPop(tags2);
 
@@ -713,18 +728,21 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       {
         if (tag1 < tag2) {
           // copy tag1
-          newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++];
+          newSetTriggers[newSetTriggersSize++] =
+              class1triggers.d_triggers[i1++];
           tag1 = Theory::setPop(tags1);
         } else if (tag1 > tag2) {
           // copy tag2
-          newSetTriggers[newSetTriggersSize++] = class2triggers.triggers[i2++];
+          newSetTriggers[newSetTriggersSize++] =
+              class2triggers.d_triggers[i2++];
           tag2 = Theory::setPop(tags2);
         } else {
           // copy tag1
-          EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++];
+          EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] =
+              class1triggers.d_triggers[i1++];
           // since they are both tagged notify of merge
           if (d_performNotify) {
-            EqualityNodeId tag2id = class2triggers.triggers[i2++];
+            EqualityNodeId tag2id = class2triggers.d_triggers[i2++];
             if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
               return false;
             }
@@ -736,7 +754,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       }
 
       // Add the new trigger set, if different from previous one
-      if (class1triggers.tags != class2triggers.tags) {
+      if (class1triggers.d_tags != class2triggers.d_tags)
+      {
         // Add it to the list for backtracking
         d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef));
         d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
@@ -771,8 +790,8 @@ void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, Equal
     TriggerId currentTrigger = d_nodeTriggers[currentId];
     while (currentTrigger != null_trigger) {
       Trigger& trigger = d_equalityTriggers[currentTrigger];
-      trigger.classId = class2Id;
-      currentTrigger = trigger.nextTrigger;
+      trigger.d_classId = class2Id;
+      currentTrigger = trigger.d_nextTrigger;
     }
 
     // Move to the next node
@@ -800,8 +819,10 @@ void EqualityEngine::backtrack() {
       // Get the ids of the merged classes
       Equality& eq = d_assertedEqualities[i];
       // Undo the merge
-      if (eq.lhs != null_id) {
-        undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
+      if (eq.d_lhs != null_id)
+      {
+        undoMerge(
+            d_equalityNodes[eq.d_lhs], d_equalityNodes[eq.d_rhs], eq.d_rhs);
       }
     }
 
@@ -823,7 +844,7 @@ void EqualityEngine::backtrack() {
     // Unset the individual triggers
     for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) {
       const TriggerSetUpdate& update = d_triggerTermSetUpdates[i];
-      d_nodeIndividualTrigger[update.classId] = update.oldValue;
+      d_nodeIndividualTrigger[update.d_classId] = update.d_oldValue;
     }
     d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
   }
@@ -832,7 +853,7 @@ void EqualityEngine::backtrack() {
     // Unlink the triggers from the lists
     for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
       const Trigger& trigger = d_equalityTriggers[i];
-      d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+      d_nodeTriggers[trigger.d_classId] = trigger.d_nextTrigger;
     }
     // Get rid of the triggers
     d_equalityTriggers.resize(d_equalityTriggersCount);
@@ -860,12 +881,12 @@ void EqualityEngine::backtrack() {
       Debug("equality") << d_name << "::eq::backtrack(): removing node " << d_nodes[i] << std::endl;
       d_nodeIds.erase(d_nodes[i]);
 
-      const FunctionApplication& app = d_applications[i].original;
+      const FunctionApplication& app = d_applications[i].d_original;
       if (!app.isNull()) {
         // Remove b from use-list
-        getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
+        getEqualityNode(app.d_b).removeTopFromUseList(d_useListNodes);
         // Remove a from use-list
-        getEqualityNode(app.a).removeTopFromUseList(d_useListNodes);
+        getEqualityNode(app.d_a).removeTopFromUseList(d_useListNodes);
       }
     }
 
@@ -959,8 +980,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
         << "Don't ask for stuff I didn't notify you about";
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
 
-    for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
-
+    for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i)
+    {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
       std::shared_ptr<EqProof> eqpc;
 
@@ -1143,7 +1164,7 @@ void EqualityEngine::getExplanation(
 
     // The next node to visit
     BfsData current = bfsQueue[currentIndex];
-    EqualityNodeId currentNode = current.nodeId;
+    EqualityNodeId currentNode = current.d_nodeId;
 
     Debug("equality") << d_name << "::eq::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
 
@@ -1159,8 +1180,8 @@ void EqualityEngine::getExplanation(
       const EqualityEdge& edge = d_equalityEdges[currentEdge];
 
       // If not just the backwards edge
-      if ((currentEdge | 1u) != (current.edgeId | 1u)) {
-
+      if ((currentEdge | 1u) != (current.d_edgeId | 1u))
+      {
         Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
 
         // Did we find the path
@@ -1173,7 +1194,7 @@ void EqualityEngine::getExplanation(
           // Reconstruct the path
           do {
             // The current node
-            currentNode = bfsQueue[currentIndex].nodeId;
+            currentNode = bfsQueue[currentIndex].d_nodeId;
             EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
             unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
             Node reason = d_equalityEdges[currentEdge].getReason();
@@ -1195,18 +1216,20 @@ void EqualityEngine::getExplanation(
             case MERGED_THROUGH_CONGRUENCE: {
               // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
               Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl;
-              const FunctionApplication& f1 = d_applications[currentNode].original;
-              const FunctionApplication& f2 = d_applications[edgeNode].original;
+              const FunctionApplication& f1 =
+                  d_applications[currentNode].d_original;
+              const FunctionApplication& f2 =
+                  d_applications[edgeNode].d_original;
 
               Debug("equality") << push;
               Debug("equality") << "Explaining left hand side equalities" << std::endl;
               std::shared_ptr<EqProof> eqpc1 =
                   eqpc ? std::make_shared<EqProof>() : nullptr;
-              getExplanation(f1.a, f2.a, equalities, cache, eqpc1.get());
+              getExplanation(f1.d_a, f2.d_a, equalities, cache, eqpc1.get());
               Debug("equality") << "Explaining right hand side equalities" << std::endl;
               std::shared_ptr<EqProof> eqpc2 =
                   eqpc ? std::make_shared<EqProof>() : nullptr;
-              getExplanation(f1.b, f2.b, equalities, cache, eqpc2.get());
+              getExplanation(f1.d_b, f2.d_b, equalities, cache, eqpc2.get());
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
@@ -1214,25 +1237,35 @@ void EqualityEngine::getExplanation(
                   //leave node null for now
                   eqpc->d_node = Node::null();
                 } else {
-                  if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
-                     d_nodes[f1.a].getKind() == kind::SELECT ||
-                     d_nodes[f1.a].getKind() == kind::STORE) {
-                    eqpc->d_node = d_nodes[f1.a];
-                  } else {
-                    if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) {
-                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
+                  if (d_nodes[f1.d_a].getKind() == kind::APPLY_UF
+                      || d_nodes[f1.d_a].getKind() == kind::SELECT
+                      || d_nodes[f1.d_a].getKind() == kind::STORE)
+                  {
+                    eqpc->d_node = d_nodes[f1.d_a];
+                  }
+                  else
+                  {
+                    if (d_nodes[f1.d_a].getKind() == kind::BUILTIN
+                        && d_nodes[f1.d_a].getConst<Kind>() == kind::SELECT)
+                    {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(
+                          kind::PARTIAL_SELECT_1, d_nodes[f1.d_b]);
                       // The first child is a PARTIAL_SELECT_0.
                       // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
                       Assert(eqpc->d_children[0]->d_node.getKind()
                              == kind::PARTIAL_SELECT_0);
                       Assert(eqpc->d_children[0]->d_children.size() == 0);
 
-                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
-                                                                                     d_nodes[f1.b]);
-                    } else {
-                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
-                                                                      ProofManager::currentPM()->mkOp(d_nodes[f1.a]),
-                                                                      d_nodes[f1.b]);
+                      eqpc->d_children[0]->d_node =
+                          NodeManager::currentNM()->mkNode(
+                              kind::PARTIAL_SELECT_0, d_nodes[f1.d_b]);
+                    }
+                    else
+                    {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(
+                          kind::PARTIAL_APPLY_UF,
+                          ProofManager::currentPM()->mkOp(d_nodes[f1.d_a]),
+                          d_nodes[f1.d_b]);
                     }
                   }
                 }
@@ -1245,14 +1278,14 @@ void EqualityEngine::getExplanation(
               // x1 == x1
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
               EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
-              const FunctionApplication& eq = d_applications[eqId].original;
+              const FunctionApplication& eq = d_applications[eqId].d_original;
               Assert(eq.isEquality()) << "Must be an equality";
 
               // Explain why a = b constant
               Debug("equality") << push;
               std::shared_ptr<EqProof> eqpc1 =
                   eqpc ? std::make_shared<EqProof>() : nullptr;
-              getExplanation(eq.a, eq.b, equalities, cache, eqpc1.get());
+              getExplanation(eq.d_a, eq.d_b, equalities, cache, eqpc1.get());
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
               }
@@ -1335,8 +1368,8 @@ void EqualityEngine::getExplanation(
             }
 
             // Go to the previous
-            currentEdge = bfsQueue[currentIndex].edgeId;
-            currentIndex = bfsQueue[currentIndex].previousIndex;
+            currentEdge = bfsQueue[currentIndex].d_edgeId;
+            currentIndex = bfsQueue[currentIndex].d_previousIndex;
 
             //---from Morgan---
             if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
@@ -1577,8 +1610,8 @@ void EqualityEngine::propagate() {
     d_propagationQueue.pop_front();
 
     // Get the representatives
-    EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind();
-    EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind();
+    EqualityNodeId t1classId = getEqualityNode(current.d_t1Id).getFind();
+    EqualityNodeId t2classId = getEqualityNode(current.d_t2Id).getFind();
 
     // If already the same, we're done
     if (t1classId == t2classId) {
@@ -1596,7 +1629,8 @@ void EqualityEngine::propagate() {
     Assert(node2.getFind() == t2classId);
 
     // Add the actual equality to the equality graph
-    addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+    addGraphEdge(
+        current.d_t1Id, current.d_t2Id, current.d_type, current.d_reason);
 
     // If constants are being merged we're done
     if (d_isConstant[t1classId] && d_isConstant[t2classId]) {
@@ -1642,14 +1676,18 @@ void EqualityEngine::propagate() {
     }
 
     if (mergeInto == t2classId) {
-      Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
+      Debug("equality") << d_name << "::eq::propagate(): merging "
+                        << d_nodes[current.d_t1Id] << " into "
+                        << d_nodes[current.d_t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
       d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
       if (!merge(node2, node1, triggers)) {
         d_done = true;
       }
     } else {
-      Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
+      Debug("equality") << d_name << "::eq::propagate(): merging "
+                        << d_nodes[current.d_t2Id] << " into "
+                        << d_nodes[current.d_t1Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t1classId, t2classId));
       d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
     if (!merge(node1, node2, triggers)) {
@@ -1667,11 +1705,13 @@ void EqualityEngine::propagate() {
     if (d_performNotify && !d_done) {
       for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
         const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]];
-        if (triggerInfo.trigger.getKind() == kind::EQUAL) {
+        if (triggerInfo.d_trigger.getKind() == kind::EQUAL)
+        {
           // Special treatment for disequalities
-          if (!triggerInfo.polarity) {
+          if (!triggerInfo.d_polarity)
+          {
             // Store that we are propagating a diseauality
-            TNode equality = triggerInfo.trigger;
+            TNode equality = triggerInfo.d_trigger;
             EqualityNodeId original = getNodeId(equality);
             TNode lhs = equality[0];
             TNode rhs = equality[1];
@@ -1685,18 +1725,28 @@ void EqualityEngine::propagate() {
                 d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
               }
               storePropagatedDisequality(THEORY_LAST, lhsId, rhsId);
-              if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
+              if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
+                                                    triggerInfo.d_polarity))
+              {
                 d_done = true;
               }
             }
-          } else {
+          }
+          else
+          {
             // Equalities are simple
-            if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
+            if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
+                                                  triggerInfo.d_polarity))
+            {
               d_done = true;
             }
           }
-        } else {
-          if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) {
+        }
+        else
+        {
+          if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
+                                                 triggerInfo.d_polarity))
+          {
             d_done = true;
           }
         }
@@ -1776,10 +1826,13 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
   if (find != d_applicationLookup.end()) {
     if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) {
       if (ensureProof) {
-        const FunctionApplication original = d_applications[find->second].original;
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.a));
+        const FunctionApplication original =
+            d_applications[find->second].d_original;
+        nonConst->d_deducedDisequalityReasons.push_back(
+            EqualityPair(t1Id, original.d_a));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
+        nonConst->d_deducedDisequalityReasons.push_back(
+            EqualityPair(t2Id, original.d_b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       Debug("equality") << "\t(YES)" << std::endl;
@@ -1788,15 +1841,18 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
   }
 
   // Check the symmetric disequality
-  std::swap(eqNormalized.a, eqNormalized.b);
+  std::swap(eqNormalized.d_a, eqNormalized.d_b);
   find = d_applicationLookup.find(eqNormalized);
   if (find != d_applicationLookup.end()) {
     if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) {
       if (ensureProof) {
-        const FunctionApplication original = d_applications[find->second].original;
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.a));
+        const FunctionApplication original =
+            d_applications[find->second].d_original;
+        nonConst->d_deducedDisequalityReasons.push_back(
+            EqualityPair(t2Id, original.d_a));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
+        nonConst->d_deducedDisequalityReasons.push_back(
+            EqualityPair(t1Id, original.d_b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       Debug("equality") << "\t(YES)" << std::endl;
@@ -1875,7 +1931,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
       // Get the existing set
       TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
       // Initialize the new set for copy/insert
-      newSetTags = Theory::setInsert(tag, triggerSet.tags);
+      newSetTags = Theory::setInsert(tag, triggerSet.d_tags);
       newSetTriggersSize = 0;
       // Copy into to new one, and insert the new tag/id
       unsigned i = 0;
@@ -1886,7 +1942,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
         tags = Theory::setRemove(current, tags);
         // Insert the id into the triggers
         newSetTriggers[newSetTriggersSize++] =
-          current == tag ? eqNodeId : triggerSet.triggers[i++];
+            current == tag ? eqNodeId : triggerSet.d_triggers[i++];
       }
     } else {
       // Setup a singleton
@@ -1920,11 +1976,11 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const
   EqualityNodeId classId = getEqualityNode(t).getFind();
   const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]);
   unsigned i = 0;
-  Theory::Set tags = triggerSet.tags;
+  Theory::Set tags = triggerSet.d_tags;
   while (Theory::setPop(tags) != tag) {
     ++ i;
   }
-  return d_nodes[triggerSet.triggers[i]];
+  return d_nodes[triggerSet.d_triggers[i]];
 }
 
 void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) {
@@ -1938,9 +1994,12 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized,
 
   // If an equality over constants we merge to false
   if (funNormalized.isEquality()) {
-    if (funNormalized.a == funNormalized.b) {
+    if (funNormalized.d_a == funNormalized.d_b)
+    {
       enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
-    } else if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
+    }
+    else if (d_isConstant[funNormalized.d_a] && d_isConstant[funNormalized.d_b])
+    {
       enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
     }
   }
@@ -1988,9 +2047,9 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set
   d_triggerDatabaseSize = d_triggerDatabaseSize + size;
   // Copy the information
   TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef);
-  newSet.tags = newSetTags;
+  newSet.d_tags = newSetTags;
   for (unsigned i = 0; i < newSetTriggersSize; ++i) {
-    newSet.triggers[i] = newSetTriggers[i];
+    newSet.d_triggers[i] = newSetTriggers[i];
   }
   // Return the new reference
   return newTriggerSetRef;
@@ -2055,19 +2114,20 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs
     DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size());
 #ifdef CVC4_ASSERTIONS
     // Check that the reasons are valid
-    for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
+    for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
+    {
       Assert(
           getEqualityNode(d_deducedDisequalityReasons[i].first).getFind()
           == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
     }
 #endif
     if (Debug.isOn("equality::disequality")) {
-      for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
+      for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
+      {
         TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first];
         TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second];
         Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl;
       }
-
     }
 
     // Store for backtracking
@@ -2089,7 +2149,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
   // The class we are looking for, shouldn't have any of the tags we are looking for already set
   Assert(d_nodeIndividualTrigger[classId] == null_set_id
          || Theory::setIntersection(
-                getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags,
+                getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags,
                 inputTags)
                 == 0);
 
@@ -2117,14 +2177,15 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
 
       Debug("equality::trigger") << d_name << "::getDisequalities() : checking " << d_nodes[funId] << std::endl;
 
-      const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original;
+      const FunctionApplication& fun =
+          d_applications[useListNode.getApplicationId()].d_original;
       // If it's an equality asserted to false, we do the work
       if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
         // Get the other equality member
         bool lhs = false;
-        EqualityNodeId toCompare = fun.b;
+        EqualityNodeId toCompare = fun.d_b;
         if (toCompare == currentId) {
-          toCompare = fun.a;
+          toCompare = fun.d_a;
           lhs = true;
         }
         // Representative of the other member
@@ -2145,7 +2206,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
             // Tags of the other gey
             TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
             // We only care if there are things in inputTags that is also in toCompareTags
-            Theory::Set commonTags = Theory::setIntersection(inputTags, toCompareTriggerSet.tags);
+            Theory::Set commonTags =
+                Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags);
             if (commonTags) {
               out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs));
             }
@@ -2178,14 +2240,17 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
   for (; !d_done && it != it_end; ++ it) {
     // The information about the equality that is asserted to false
     const TaggedEquality& disequalityInfo = *it;
-    const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef);
-    Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags);
+    const TriggerTermSet& disequalityTriggerSet =
+        getTriggerTermSet(disequalityInfo.d_triggerSetRef);
+    Theory::Set commonTags =
+        Theory::setIntersection(disequalityTriggerSet.d_tags, tags);
     Assert(commonTags);
     // This is the actual function
-    const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original;
+    const FunctionApplication& fun =
+        d_applications[disequalityInfo.d_equalityId].d_original;
     // Figure out who we are comparing to in the original equality
-    EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b;
-    EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a;
+    EqualityNodeId toCompare = disequalityInfo.d_lhs ? fun.d_a : fun.d_b;
+    EqualityNodeId myCompare = disequalityInfo.d_lhs ? fun.d_b : fun.d_a;
     if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) {
       // We're propagating a != a, which means we're inconsistent, just bail and let it go into
       // a regular conflict
@@ -2203,7 +2268,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
         if (!hasPropagatedDisequality(myRep, tagRep)) {
           d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep));
           d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
-          d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId));
+          d_deducedDisequalityReasons.push_back(
+              EqualityPair(disequalityInfo.d_equalityId, d_falseId));
         }
         // Store the propagation
         storePropagatedDisequality(currentTag, myRep, tagRep);
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 73d8bd4e9..041625568 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -211,13 +211,13 @@ public:
   /** Statistics about the equality engine instance */
   struct Statistics {
     /** Total number of merges */
-    IntStat mergesCount;
+    IntStat d_mergesCount;
     /** Number of terms managed by the system */
-    IntStat termsCount;
+    IntStat d_termsCount;
     /** Number of function terms managed by the system */
-    IntStat functionTermsCount;
+    IntStat d_functionTermsCount;
     /** Number of constant terms managed by the system */
-    IntStat constantTermsCount;
+    IntStat d_constantTermsCount;
 
     Statistics(std::string name);
 
@@ -300,12 +300,14 @@ private:
    */
   struct Equality {
     /** Left hand side of the equality */
-    EqualityNodeId lhs;
+    EqualityNodeId d_lhs;
     /** Right hand side of the equality */
-    EqualityNodeId rhs;
+    EqualityNodeId d_rhs;
     /** Equality constructor */
-    Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id)
-    : lhs(lhs), rhs(rhs) {}
+    Equality(EqualityNodeId l = null_id, EqualityNodeId r = null_id)
+        : d_lhs(l), d_rhs(r)
+    {
+    }
   };/* struct EqualityEngine::Equality */
 
   /** The ids of the classes we have merged */
@@ -402,12 +404,15 @@ private:
    */
   struct Trigger {
     /** The current class id of the LHS of the trigger */
-    EqualityNodeId classId;
+    EqualityNodeId d_classId;
     /** Next trigger for class */
-    TriggerId nextTrigger;
+    TriggerId d_nextTrigger;
 
-    Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger)
-    : classId(classId), nextTrigger(nextTrigger) {}
+    Trigger(EqualityNodeId classId = null_id,
+            TriggerId nextTrigger = null_trigger)
+        : d_classId(classId), d_nextTrigger(nextTrigger)
+    {
+    }
   };/* struct EqualityEngine::Trigger */
 
   /**
@@ -573,14 +578,17 @@ private:
   /** Set of trigger terms */
   struct TriggerTermSet {
     /** Set of theories in this set */
-    Theory::Set tags;
+    Theory::Set d_tags;
     /** The trigger terms */
-    EqualityNodeId triggers[0];
+    EqualityNodeId d_triggers[0];
     /** Returns the theory tags */
-    Theory::Set hasTrigger(TheoryId tag) const { return Theory::setContains(tag, tags); }
+    Theory::Set hasTrigger(TheoryId tag) const
+    {
+      return Theory::setContains(tag, d_tags);
+    }
     /** Returns a trigger by tag */
     EqualityNodeId getTrigger(TheoryId tag) const {
-      return triggers[Theory::setIndex(tag, tags)];
+      return d_triggers[Theory::setIndex(tag, d_tags)];
     }
   };/* struct EqualityEngine::TriggerTermSet */
 
@@ -618,10 +626,13 @@ private:
   context::CDO<DefaultSizeType> d_triggerDatabaseSize;
 
   struct TriggerSetUpdate {
-    EqualityNodeId classId;
-    TriggerTermSetRef oldValue;
-    TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id)
-    : classId(classId), oldValue(oldValue) {}
+    EqualityNodeId d_classId;
+    TriggerTermSetRef d_oldValue;
+    TriggerSetUpdate(EqualityNodeId classId = null_id,
+                     TriggerTermSetRef oldValue = null_set_id)
+        : d_classId(classId), d_oldValue(oldValue)
+    {
+    }
   };/* struct EqualityEngine::TriggerSetUpdate */
 
   /**
@@ -693,14 +704,18 @@ private:
    */
   struct TaggedEquality {
     /** Id of the equality */
-    EqualityNodeId equalityId;
+    EqualityNodeId d_equalityId;
     /** TriggerSet reference for the class of one of the sides */
-    TriggerTermSetRef triggerSetRef;
+    TriggerTermSetRef d_triggerSetRef;
     /** Is trigger equivalent to the lhs (rhs otherwise) */
-    bool lhs;
+    bool d_lhs;
 
-    TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true)
-    : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {}
+    TaggedEquality(EqualityNodeId equalityId = null_id,
+                   TriggerTermSetRef triggerSetRef = null_set_id,
+                   bool lhs = true)
+        : d_equalityId(equalityId), d_triggerSetRef(triggerSetRef), d_lhs(lhs)
+    {
+    }
   };
 
   /** A map from equivalence class id's to tagged equalities */
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 402b21a02..0e6d283fe 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -109,11 +109,14 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
  * additional information.
  */
 struct MergeCandidate {
-  EqualityNodeId t1Id, t2Id;
-  unsigned type;
-  TNode reason;
-  MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason)
-  : t1Id(x), t2Id(y), type(type), reason(reason)
+  EqualityNodeId d_t1Id, d_t2Id;
+  unsigned d_type;
+  TNode d_reason;
+  MergeCandidate(EqualityNodeId x,
+                 EqualityNodeId y,
+                 unsigned type,
+                 TNode reason)
+      : d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason)
   {}
 };
 
@@ -121,10 +124,13 @@ struct MergeCandidate {
  * Just an index into the reasons array, and the number of merges to consume.
  */
 struct DisequalityReasonRef {
-  DefaultSizeType mergesStart;
-  DefaultSizeType mergesEnd;
-  DisequalityReasonRef(DefaultSizeType mergesStart = 0, DefaultSizeType mergesEnd = 0)
-  : mergesStart(mergesStart), mergesEnd(mergesEnd) {}
+  DefaultSizeType d_mergesStart;
+  DefaultSizeType d_mergesEnd;
+  DisequalityReasonRef(DefaultSizeType mergesStart = 0,
+                       DefaultSizeType mergesEnd = 0)
+      : d_mergesStart(mergesStart), d_mergesEnd(mergesEnd)
+  {
+  }
 };
 
 /**
@@ -289,41 +295,38 @@ enum FunctionApplicationType {
  */
 struct FunctionApplication {
   /** Type of application */
-  FunctionApplicationType type;
+  FunctionApplicationType d_type;
   /** The actual application elements */
-  EqualityNodeId a, b;
+  EqualityNodeId d_a, d_b;
 
   /** Construct an application */
-  FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
-  : type(type), a(a), b(b) {}
+  FunctionApplication(FunctionApplicationType type = APP_EQUALITY,
+                      EqualityNodeId a = null_id,
+                      EqualityNodeId b = null_id)
+      : d_type(type), d_a(a), d_b(b)
+  {
+  }
 
   /** Equality of two applications */
   bool operator == (const FunctionApplication& other) const {
-    return type == other.type && a == other.a && b == other.b;
+    return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b;
   }
 
   /** Is this a null application */
-  bool isNull() const {
-    return a == null_id || b == null_id;
-  }
+  bool isNull() const { return d_a == null_id || d_b == null_id; }
 
   /** Is this an equality */
-  bool isEquality() const {
-    return type == APP_EQUALITY;
-  }
+  bool isEquality() const { return d_type == APP_EQUALITY; }
 
   /** Is this an interpreted application (equality is special, i.e. not interpreted) */
-  bool isInterpreted() const {
-    return type == APP_INTERPRETED;
-  }
-
+  bool isInterpreted() const { return d_type == APP_INTERPRETED; }
 };
 
 struct FunctionApplicationHashFunction {
   size_t operator () (const FunctionApplication& app) const {
     size_t hash = 0;
-    hash = 0x9e3779b9 + app.a;
-    hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2);
+    hash = 0x9e3779b9 + app.d_a;
+    hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2);
     return hash;
   }
 };
@@ -333,14 +336,15 @@ struct FunctionApplicationHashFunction {
  * we keep both the original, and the normalized version.
  */
 struct FunctionApplicationPair {
-  FunctionApplication original;
-  FunctionApplication normalized;
+  FunctionApplication d_original;
+  FunctionApplication d_normalized;
   FunctionApplicationPair() {}
-  FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized)
-  : original(original), normalized(normalized) {}
-  bool isNull() const {
-    return original.isNull();
+  FunctionApplicationPair(const FunctionApplication& original,
+                          const FunctionApplication& normalized)
+      : d_original(original), d_normalized(normalized)
+  {
   }
+  bool isNull() const { return d_original.isNull(); }
 };
 
 /**
@@ -348,12 +352,14 @@ struct FunctionApplicationPair {
  */
 struct TriggerInfo {
   /** The trigger itself */
-  Node trigger;
+  Node d_trigger;
   /** Polarity of the trigger */
-  bool polarity;
-  TriggerInfo() : polarity(false) {}
+  bool d_polarity;
+  TriggerInfo() : d_polarity(false) {}
   TriggerInfo(Node trigger, bool polarity)
-      : trigger(trigger), polarity(polarity) {}
+      : d_trigger(trigger), d_polarity(polarity)
+  {
+  }
 };
 
 } // namespace eq
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e336d1630..3b42fa6a1 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -124,7 +124,7 @@ void TheoryUF::check(Effort level) {
   {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
     Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;