Fix -Wshadow warnings in common headers (#3826)

15 files changed, 121 insertions, 99 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0a365a4d5..31453b618 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1189,26 +1189,26 @@ uint32_t Op::getIndices() const
   switch (k)
   {
     case BITVECTOR_REPEAT:
-      i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
+      i = d_expr->getConst<BitVectorRepeat>().d_repeatAmount;
       break;
     case BITVECTOR_ZERO_EXTEND:
-      i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
+      i = d_expr->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
       break;
     case BITVECTOR_SIGN_EXTEND:
-      i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
+      i = d_expr->getConst<BitVectorSignExtend>().d_signExtendAmount;
       break;
     case BITVECTOR_ROTATE_LEFT:
-      i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
+      i = d_expr->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
       break;
     case BITVECTOR_ROTATE_RIGHT:
-      i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
+      i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount;
       break;
-    case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break;
+    case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break;
     case FLOATINGPOINT_TO_UBV:
-      i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
+      i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size;
       break;
     case FLOATINGPOINT_TO_SBV:
-      i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
+      i = d_expr->getConst<FloatingPointToSBV>().bvs.d_size;
       break;
     case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
     default:
@@ -1232,7 +1232,7 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
   if (k == BITVECTOR_EXTRACT)
   {
     CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
-    indices = std::make_pair(ext.high, ext.low);
+    indices = std::make_pair(ext.d_high, ext.d_low);
   }
   else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
   {
diff --git a/src/expr/node.h b/src/expr/node.h
index 616e256ab..e07499b69 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -825,10 +825,15 @@ public:
    * (might break language compliance, but good for debugging expressions)
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
-                       OutputLanguage language = language::output::LANG_AUTO) const {
+  inline void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dagThreshold = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const
+  {
     assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, types, dag, language);
+    d_nv->toStream(out, toDepth, types, dagThreshold, language);
   }
 
   /**
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 14eb9064c..dcafef9c0 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -798,9 +798,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
       // push the operator
       nb << TypeNode(d_nv->d_children[0]);
     }
-    for (TypeNode::const_iterator it = begin(), iend = end(); it != iend; ++it)
+    for (const TypeNode& tn : *this)
     {
-      nb << (*it).substitute(
+      nb << tn.substitute(
           typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache);
     }
     TypeNode tn = nb.constructTypeNode();
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f3f43220c..70324d313 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -138,7 +138,7 @@ void CvcPrinter::toStream(
   if(n.getMetaKind() == kind::metakind::CONSTANT) {
     switch(n.getKind()) {
     case kind::BITVECTOR_TYPE:
-      out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";
+      out << "BITVECTOR(" << n.getConst<BitVectorSize>().d_size << ")";
       break;
     case kind::CONST_BITVECTOR: {
       const BitVector& bv = n.getConst<BitVector>();
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6fdbd4adb..13a64a2c3 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -138,9 +138,9 @@ void Smt2Printer::toStream(std::ostream& out,
       break;
     case kind::BITVECTOR_TYPE:
       if(d_variant == sygus_variant ){
-        out << "(BitVec " << n.getConst<BitVectorSize>().size << ")";
+        out << "(BitVec " << n.getConst<BitVectorSize>().d_size << ")";
       }else{
-        out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
+        out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
       }
       break;
     case kind::FLOATINGPOINT_TYPE:
@@ -270,30 +270,31 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::BITVECTOR_EXTRACT_OP:
     {
       BitVectorExtract p = n.getConst<BitVectorExtract>();
-      out << "(_ extract " << p.high << ' ' << p.low << ")";
+      out << "(_ extract " << p.d_high << ' ' << p.d_low << ")";
       break;
     }
     case kind::BITVECTOR_REPEAT_OP:
-      out << "(_ repeat " << n.getConst<BitVectorRepeat>().repeatAmount << ")";
+      out << "(_ repeat " << n.getConst<BitVectorRepeat>().d_repeatAmount
+          << ")";
       break;
     case kind::BITVECTOR_ZERO_EXTEND_OP:
       out << "(_ zero_extend "
-          << n.getConst<BitVectorZeroExtend>().zeroExtendAmount << ")";
+          << n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount << ")";
       break;
     case kind::BITVECTOR_SIGN_EXTEND_OP:
       out << "(_ sign_extend "
-          << n.getConst<BitVectorSignExtend>().signExtendAmount << ")";
+          << n.getConst<BitVectorSignExtend>().d_signExtendAmount << ")";
       break;
     case kind::BITVECTOR_ROTATE_LEFT_OP:
       out << "(_ rotate_left "
-          << n.getConst<BitVectorRotateLeft>().rotateLeftAmount << ")";
+          << n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount << ")";
       break;
     case kind::BITVECTOR_ROTATE_RIGHT_OP:
       out << "(_ rotate_right "
-          << n.getConst<BitVectorRotateRight>().rotateRightAmount << ")";
+          << n.getConst<BitVectorRotateRight>().d_rotateRightAmount << ")";
       break;
     case kind::INT_TO_BITVECTOR_OP:
-      out << "(_ int2bv " << n.getConst<IntToBitVector>().size << ")";
+      out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
       // out << "to_fp_bv "
@@ -334,20 +335,20 @@ void Smt2Printer::toStream(std::ostream& out,
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_UBV_OP:
-      out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.size
+      out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.d_size
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_SBV_OP:
-      out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.size
+      out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.d_size
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
       out << "(_ fp.to_ubv_total "
-          << n.getConst<FloatingPointToUBVTotal>().bvs.size << ")";
+          << n.getConst<FloatingPointToUBVTotal>().bvs.d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
       out << "(_ fp.to_sbv_total "
-          << n.getConst<FloatingPointToSBVTotal>().bvs.size << ")";
+          << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")";
       break;
     default:
       // fall back on whatever operator<< does on underlying type; we
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index e75b94c8e..fddcb9e78 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -235,7 +235,7 @@ void BitVectorProof::printBitOf(Expr term,
                                 const ProofLetMap& map)
 {
   Assert(term.getKind() == kind::BITVECTOR_BITOF);
-  unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
+  unsigned bit = term.getOperator().getConst<BitVectorBitOf>().d_bitIndex;
   Expr var = term[0];
 
   Debug("pf::bv") << "BitVectorProof::printBitOf( " << term << " ), "
@@ -319,16 +319,19 @@ void BitVectorProof::printOperatorParametric(Expr term,
   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
   os <<" ";
   if (term.getKind() == kind::BITVECTOR_REPEAT) {
-    unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+    unsigned amount =
+        term.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
     os << amount <<" _ ";
   }
   if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
-    unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+    unsigned amount =
+        term.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
     os << amount <<" _ ";
   }
 
   if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+    unsigned amount =
+        term.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
     os << amount<<" _ ";
   }
   if (term.getKind() == kind::BITVECTOR_EXTRACT) {
@@ -523,16 +526,19 @@ void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os)
     os << "(bv_bbl_" << utils::toLFSCKind(kind) << " ";
     os << utils::getSize(term) << " ";
     if (term.getKind() == kind::BITVECTOR_REPEAT) {
-      unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+      unsigned amount =
+          term.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
       os << amount;
     }
     if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
-      unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+      unsigned amount =
+          term.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
       os << amount;
     }
 
     if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-      unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+      unsigned amount =
+          term.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
       os << amount;
     }
 
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 66e20069d..23f221cf6 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -93,11 +93,11 @@ std::string toLFSCKind(Kind kind);
 std::string toLFSCKindTerm(Expr node);
 
 inline unsigned getExtractHigh(Expr node) {
-  return node.getOperator().getConst<BitVectorExtract>().high;
+  return node.getOperator().getConst<BitVectorExtract>().d_high;
 }
 
 inline unsigned getExtractLow(Expr node) {
-  return node.getOperator().getConst<BitVectorExtract>().low;
+  return node.getOperator().getConst<BitVectorExtract>().d_low;
 }
 
 inline unsigned getSize(Type type) {
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 047396506..463203118 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -867,8 +867,9 @@ void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>*
   std::vector<T> bits;
   bb->bbTerm(node[0], bits);
   
-  T sign_bit = bits.back(); 
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
+  T sign_bit = bits.back();
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 
   for (unsigned i = 0; i < bits.size(); ++i ) {
     res_bits.push_back(bits[i]); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 22a12cc10..27fad165f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -452,7 +452,8 @@ template<> inline
 Node RewriteRule<EvalSignExtend>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   BitVector res = a.signExtend(amount);
   
   return utils::mkConst(res);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index aef20ee0a..6be1e7203 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -200,7 +200,8 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
   Assert(amount >= 1);
   if(amount == 1) {
     return a; 
@@ -224,7 +225,8 @@ inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
   amount = amount % utils::getSize(a); 
   if (amount == 0) {
     return a; 
@@ -248,7 +250,8 @@ inline Node RewriteRule<RotateRightEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRotateRight>().d_rotateRightAmount;
   amount = amount % utils::getSize(a); 
   if (amount == 0) {
     return a; 
@@ -506,7 +509,8 @@ inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node)
   Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
 
   TNode bv = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
   if (amount == 0) {
     return node[0]; 
   }
@@ -527,7 +531,8 @@ inline Node RewriteRule<SignExtendEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
 
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   if(amount == 0) {
     return node[0]; 
   }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index c3e1b316c..9e6c31061 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1619,12 +1619,14 @@ template<> inline
 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
   unsigned amount1 =
-      node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 
   NodeManager* nm = NodeManager::currentNM();
   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    unsigned amount2 =
-        node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+    unsigned amount2 = node[0]
+                           .getOperator()
+                           .getConst<BitVectorZeroExtend>()
+                           .d_zeroExtendAmount;
     if (amount2 == 0)
     {
       NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
@@ -1642,7 +1644,7 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   }
   Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
   unsigned amount2 =
-      node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+      node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   return utils::mkSignExtend(node[0][0], amount1 + amount2);
 }
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 9d5c6f396..97b7a8a8f 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -240,7 +240,7 @@ class BitVectorBitOfTypeRule
       {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
-      if (info.bitIndex >= t.getBitVectorSize())
+      if (info.d_bitIndex >= t.getBitVectorSize())
       {
         throw TypeCheckingExceptionPrivate(
             n, "extract index is larger than the bitvector size");
@@ -262,7 +262,7 @@ class BitVectorExtractTypeRule
     // NOTE: We're throwing a type-checking exception here even
     // if check is false, bc if we allow high < low the resulting
     // type will be illegal
-    if (extractInfo.high < extractInfo.low)
+    if (extractInfo.d_high < extractInfo.d_low)
     {
       throw TypeCheckingExceptionPrivate(
           n, "high extract index is smaller than the low extract index");
@@ -275,13 +275,14 @@ class BitVectorExtractTypeRule
       {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
-      if (extractInfo.high >= t.getBitVectorSize())
+      if (extractInfo.d_high >= t.getBitVectorSize())
       {
         throw TypeCheckingExceptionPrivate(
             n, "high extract index is bigger than the size of the bit-vector");
       }
     }
-    return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
+    return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
+                                        + 1);
   }
 }; /* class BitVectorExtractTypeRule */
 
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 44510c26b..b98aacb2f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -43,17 +43,17 @@ const bool getBit(TNode node, unsigned i)
 
 unsigned getExtractHigh(TNode node)
 {
-  return node.getOperator().getConst<BitVectorExtract>().high;
+  return node.getOperator().getConst<BitVectorExtract>().d_high;
 }
 
 unsigned getExtractLow(TNode node)
 {
-  return node.getOperator().getConst<BitVectorExtract>().low;
+  return node.getOperator().getConst<BitVectorExtract>().d_low;
 }
 
 unsigned getSignExtendAmount(TNode node)
 {
-  return node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+  return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 }
 
 /* ------------------------------------------------------------------------- */
@@ -483,7 +483,7 @@ Node eliminateBv2Nat(TNode node)
 
 Node eliminateInt2Bv(TNode node)
 {
-  const uint32_t size = node.getOperator().getConst<IntToBitVector>().size;
+  const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
   NodeManager* const nm = NodeManager::currentNM();
   const Node bvzero = utils::mkZero(1);
   const Node bvone = utils::mkOne(1);
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 59e9aedcb..92f3e6d0d 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -619,14 +619,14 @@ struct SortBvExtractInterval
     Assert(j.getKind() == BITVECTOR_EXTRACT);
     BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
     BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
-    if (ie.high > je.high)
+    if (ie.d_high > je.d_high)
     {
       return true;
     }
-    else if (ie.high == je.high)
+    else if (ie.d_high == je.d_high)
     {
-      Assert(ie.low != je.low);
-      return ie.low > je.low;
+      Assert(ie.d_low != je.d_low);
+      return ie.d_low > je.d_low;
     }
     return false;
   }
@@ -675,15 +675,15 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
         Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
         BitVectorExtract e =
             curr_vec[i].getOperator().getConst<BitVectorExtract>();
-        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+        if (std::find(boundaries.begin(), boundaries.end(), e.d_high + 1)
             == boundaries.end())
         {
-          boundaries.push_back(e.high + 1);
+          boundaries.push_back(e.d_high + 1);
         }
-        if (std::find(boundaries.begin(), boundaries.end(), e.low)
+        if (std::find(boundaries.begin(), boundaries.end(), e.d_low)
             == boundaries.end())
         {
-          boundaries.push_back(e.low);
+          boundaries.push_back(e.d_low);
         }
       }
       std::sort(boundaries.rbegin(), boundaries.rend());
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index f13db5417..a75339112 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -273,15 +273,15 @@ class CVC4_PUBLIC BitVector
 struct CVC4_PUBLIC BitVectorExtract
 {
   /** The high bit of the range for this extract */
-  unsigned high;
+  unsigned d_high;
   /** The low bit of the range for this extract */
-  unsigned low;
+  unsigned d_low;
 
-  BitVectorExtract(unsigned high, unsigned low) : high(high), low(low) {}
+  BitVectorExtract(unsigned high, unsigned low) : d_high(high), d_low(low) {}
 
   bool operator==(const BitVectorExtract& extract) const
   {
-    return high == extract.high && low == extract.low;
+    return d_high == extract.d_high && d_low == extract.d_low;
   }
 }; /* struct BitVectorExtract */
 
@@ -291,74 +291,74 @@ struct CVC4_PUBLIC BitVectorExtract
 struct CVC4_PUBLIC BitVectorBitOf
 {
   /** The index of the bit */
-  unsigned bitIndex;
-  BitVectorBitOf(unsigned i) : bitIndex(i) {}
+  unsigned d_bitIndex;
+  BitVectorBitOf(unsigned i) : d_bitIndex(i) {}
 
   bool operator==(const BitVectorBitOf& other) const
   {
-    return bitIndex == other.bitIndex;
+    return d_bitIndex == other.d_bitIndex;
   }
 }; /* struct BitVectorBitOf */
 
 struct CVC4_PUBLIC BitVectorSize
 {
-  unsigned size;
-  BitVectorSize(unsigned size) : size(size) {}
-  operator unsigned() const { return size; }
+  unsigned d_size;
+  BitVectorSize(unsigned size) : d_size(size) {}
+  operator unsigned() const { return d_size; }
 }; /* struct BitVectorSize */
 
 struct CVC4_PUBLIC BitVectorRepeat
 {
-  unsigned repeatAmount;
-  BitVectorRepeat(unsigned repeatAmount) : repeatAmount(repeatAmount) {}
-  operator unsigned() const { return repeatAmount; }
+  unsigned d_repeatAmount;
+  BitVectorRepeat(unsigned repeatAmount) : d_repeatAmount(repeatAmount) {}
+  operator unsigned() const { return d_repeatAmount; }
 }; /* struct BitVectorRepeat */
 
 struct CVC4_PUBLIC BitVectorZeroExtend
 {
-  unsigned zeroExtendAmount;
+  unsigned d_zeroExtendAmount;
   BitVectorZeroExtend(unsigned zeroExtendAmount)
-      : zeroExtendAmount(zeroExtendAmount)
+      : d_zeroExtendAmount(zeroExtendAmount)
   {
   }
-  operator unsigned() const { return zeroExtendAmount; }
+  operator unsigned() const { return d_zeroExtendAmount; }
 }; /* struct BitVectorZeroExtend */
 
 struct CVC4_PUBLIC BitVectorSignExtend
 {
-  unsigned signExtendAmount;
+  unsigned d_signExtendAmount;
   BitVectorSignExtend(unsigned signExtendAmount)
-      : signExtendAmount(signExtendAmount)
+      : d_signExtendAmount(signExtendAmount)
   {
   }
-  operator unsigned() const { return signExtendAmount; }
+  operator unsigned() const { return d_signExtendAmount; }
 }; /* struct BitVectorSignExtend */
 
 struct CVC4_PUBLIC BitVectorRotateLeft
 {
-  unsigned rotateLeftAmount;
+  unsigned d_rotateLeftAmount;
   BitVectorRotateLeft(unsigned rotateLeftAmount)
-      : rotateLeftAmount(rotateLeftAmount)
+      : d_rotateLeftAmount(rotateLeftAmount)
   {
   }
-  operator unsigned() const { return rotateLeftAmount; }
+  operator unsigned() const { return d_rotateLeftAmount; }
 }; /* struct BitVectorRotateLeft */
 
 struct CVC4_PUBLIC BitVectorRotateRight
 {
-  unsigned rotateRightAmount;
+  unsigned d_rotateRightAmount;
   BitVectorRotateRight(unsigned rotateRightAmount)
-      : rotateRightAmount(rotateRightAmount)
+      : d_rotateRightAmount(rotateRightAmount)
   {
   }
-  operator unsigned() const { return rotateRightAmount; }
+  operator unsigned() const { return d_rotateRightAmount; }
 }; /* struct BitVectorRotateRight */
 
 struct CVC4_PUBLIC IntToBitVector
 {
-  unsigned size;
-  IntToBitVector(unsigned size) : size(size) {}
-  operator unsigned() const { return size; }
+  unsigned d_size;
+  IntToBitVector(unsigned size) : d_size(size) {}
+  operator unsigned() const { return d_size; }
 }; /* struct IntToBitVector */
 
 /* -----------------------------------------------------------------------
@@ -380,8 +380,8 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction
 {
   size_t operator()(const BitVectorExtract& extract) const
   {
-    size_t hash = extract.low;
-    hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+    size_t hash = extract.d_low;
+    hash ^= extract.d_high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     return hash;
   }
 }; /* struct BitVectorExtractHashFunction */
@@ -391,7 +391,7 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction
  */
 struct CVC4_PUBLIC BitVectorBitOfHashFunction
 {
-  size_t operator()(const BitVectorBitOf& b) const { return b.bitIndex; }
+  size_t operator()(const BitVectorBitOf& b) const { return b.d_bitIndex; }
 }; /* struct BitVectorBitOfHashFunction */
 
 template <typename T>
@@ -415,21 +415,21 @@ inline std::ostream& operator<<(std::ostream& os,
                                 const BitVectorExtract& bv) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
 {
-  return os << "[" << bv.high << ":" << bv.low << "]";
+  return os << "[" << bv.d_high << ":" << bv.d_low << "]";
 }
 
 inline std::ostream& operator<<(std::ostream& os,
                                 const BitVectorBitOf& bv) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
 {
-  return os << "[" << bv.bitIndex << "]";
+  return os << "[" << bv.d_bitIndex << "]";
 }
 
 inline std::ostream& operator<<(std::ostream& os,
                                 const IntToBitVector& bv) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
 {
-  return os << "[" << bv.size << "]";
+  return os << "[" << bv.d_size << "]";
 }
 
 }  // namespace CVC4