mirror of https://github.com/YosysHQ/abc.git
Bug fix related to not properly resizing SAT solver's model array.
This commit is contained in:
parent
fadde52dc6
commit
56cc5734a4
|
|
@ -1035,6 +1035,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
|
|||
s->tags [var] = 0;
|
||||
s->orderpos[var] = veci_size(&s->order);
|
||||
s->reasons [var] = 0;
|
||||
s->model [var] = 0;
|
||||
|
||||
/* does not hold because variables enqueued at top level will not be reinserted in the heap
|
||||
assert(veci_size(&s->order) == var);
|
||||
|
|
|
|||
|
|
@ -1296,6 +1296,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
|
|||
#else
|
||||
s->activity[var] = (1<<10);
|
||||
#endif
|
||||
s->model [var] = 0;
|
||||
// does not hold because variables enqueued at top level will not be reinserted in the heap
|
||||
// assert(veci_size(&s->order) == var);
|
||||
veci_push(&s->order,var);
|
||||
|
|
|
|||
Loading…
Reference in New Issue