Fix -Wshadow warnings in common headers (#3826)

1 files changed, 13 insertions, 7 deletions

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;
     }