From ac409b3152bf0bb6fd49c243ae635ca288d92b06 Mon Sep 17 00:00:00 2001
From: Bruno Schmitt <bruno@oschmitt.com>
Date: Sat, 18 Feb 2017 15:24:56 -0800
Subject: Bug fix in analyze_final method.
---
src/sat/satoko/solver.c | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
(limited to 'src/sat/satoko')
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 21a4860d..6554f653 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -362,13 +362,13 @@ static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref)
static inline void solver_analyze_final(solver_t *s, unsigned lit)
{
- unsigned i;
+ int i;
vec_uint_push_back(s->final_conflict, lit);
if (solver_dlevel(s) == 0)
return;
vec_char_assign(s->seen, lit2var(lit), 1);
- for (i = vec_uint_size(s->trail) - 1; i <= vec_uint_at(s->trail_lim, 0); i--) {
+ for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, 0); i--) {
unsigned var = lit2var(vec_uint_at(s->trail, i));
if (vec_char_at(s->seen, var)) {
--
cgit v1.2.3