diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:44:38 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:44:38 -0700 |
| commit | d46c49088d7b9f1725d4d8624717f7209022c632 (patch) | |
| tree | d40a4896df6a2cefe57ae3fce0e1243414a1c1f5 | |
| parent | b2f1d21d37c5044d069b747747ee919a6013c665 (diff) | |
| download | abc-d46c49088d7b9f1725d4d8624717f7209022c632.tar.gz abc-d46c49088d7b9f1725d4d8624717f7209022c632.tar.bz2 abc-d46c49088d7b9f1725d4d8624717f7209022c632.zip | |
Bug fix in the recent changes to the SAT solver.
| -rw-r--r-- | src/sat/bsat/satSolver.c | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 168c8bf7..0a7cb1c7 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -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; |