Commit d46c4908 by Alan Mishchenko

Bug fix in the recent changes to the SAT solver.

parent b2f1d21d
......@@ -1092,11 +1092,14 @@ void sat_solver_rollback( sat_solver* s )
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->binary = clause_read( s, s->hBinary );
veci_resize(&s->act_clas, 0);
veci_resize(&s->trail_lim, 0);
veci_resize(&s->order, 0);
for ( i = 0; i < s->size*2; i++ )
s->wlists[i].size = 0;
s->nLearntMax = s->nLearntStart;
// initialize other vars
s->size = 0;
// s->cap = 0;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment