summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-18 15:24:56 -0800
committerBruno Schmitt <bruno@oschmitt.com>2017-02-18 15:24:56 -0800
commitac409b3152bf0bb6fd49c243ae635ca288d92b06 (patch)
tree0cdfd38394bd8e44f958147e05301bccadae01f0 /src
parent131c1613a4ca77c063cd677d0086a3b426868b3b (diff)
downloadabc-ac409b3152bf0bb6fd49c243ae635ca288d92b06.tar.gz
abc-ac409b3152bf0bb6fd49c243ae635ca288d92b06.tar.bz2
abc-ac409b3152bf0bb6fd49c243ae635ca288d92b06.zip
Bug fix in analyze_final method.
Diffstat (limited to 'src')
-rw-r--r--src/sat/satoko/solver.c4
1 files changed, 2 insertions, 2 deletions
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)) {