Enable -Wshadow and fix warnings. (#3909)

Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. 

Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>

1 files changed, 4 insertions, 6 deletions

diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
index 8d4b56d54..120397d08 100644
--- a/src/proof/resolution_bitvector_proof.cpp
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -366,10 +366,8 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof(
 
         if (possibleMatch.getKind() == kind::OR)
         {
-          for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i)
+          for (const Expr& lit : possibleMatch)
           {
-            Expr lit = possibleMatch[i];
-
             if (lit.getKind() == kind::NOT)
             {
               os << "(intro_assump_t _ _ _ ";
@@ -434,13 +432,13 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof(
     // conflict has a FALSE assertion in it; this can happen in some corner
     // cases, where the FALSE is the result of a rewrite.
 
-    for (unsigned i = 0; i < lemma.size(); ++i)
+    for (const Expr& lit : lemma)
     {
-      if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse())
+      if (lit.getKind() == kind::NOT && lit[0] == utils::mkFalse())
       {
         Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl;
         os << "(clausify_false ";
-        os << ProofManager::getLitName(lemma[i]);
+        os << ProofManager::getLitName(lit);
         os << ")";
         return;
       }