diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-02 14:04:38 -0800 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-02 14:06:42 -0800 |
| commit | d5a512ff2567390035ae1cac590ea02232ab3abe (patch) | |
| tree | 17b425a7949a528e2d749ac29524743858478ea8 /src | |
| parent | 98a4c2cd8f04cc7026990f3a4da4b5d43f161546 (diff) | |
Fix Wshadow warnings in group 57
Diffstat (limited to 'src')
| -rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 10 | ||||
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 3 |
2 files changed, 5 insertions, 8 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; } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index d9c959ae4..8d7ab6151 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -285,8 +285,7 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { typename Solver::TLit var = steps[i].lit; LitSet clause2; createLitSet(steps[i].id, clause2); - bool res = resolve<Solver>(var, clause1, clause2, steps[i].sign); - if (res == false) { + if (!resolve<Solver>(var, clause1, clause2, steps[i].sign)) { validRes = false; break; } |