summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/proof/sat_proof_implementation.h2
1 files changed, 1 insertions, 1 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback