From: Andres Noetzli <noetzli@stanford.edu>
Date: Tue, 8 Aug 2017 01:16:02 +0000 (-0700)
Subject: Fix compiler warning in sat_proof_implementation
X-Git-Tag: cvc5-1.0.0~5689
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7415a23edde7cc115fea19e8084ec15baa01c311;p=cvc5.git

Fix compiler warning in sat_proof_implementation
---

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index c115bab4a..daf98ceea 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -903,7 +903,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
   ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
   // Here, the call to resolveUnit() can reallocate memory in the
   // clause allocator.  So reload conflict ptr each time.
-  for (size_t i = 0; i < getClause(conflict_ref).size(); ++i) {
+  for (int i = 0; i < getClause(conflict_ref).size(); ++i) {
     const typename Solver::TClause& conflict = getClause(conflict_ref);
     typename Solver::TLit lit = conflict[i];
     ClauseId res_id = resolveUnit(~lit);