luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix in analyze_final method.

This commit is contained in:
Bruno Schmitt 2017-02-18 15:24:56 -08:00
parent 131c1613a4
commit ac409b3152
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/sat/satoko/solver.c
View File

@ -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) static inline void solver_analyze_final(solver_t *s, unsigned lit)
{ {
unsigned i; int i;
vec_uint_push_back(s->final_conflict, lit); vec_uint_push_back(s->final_conflict, lit);
if (solver_dlevel(s) == 0) if (solver_dlevel(s) == 0)
return; return;
vec_char_assign(s->seen, lit2var(lit), 1); 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)); unsigned var = lit2var(vec_uint_at(s->trail, i));
if (vec_char_at(s->seen, var)) { if (vec_char_at(s->seen, var)) {