From d46c49088d7b9f1725d4d8624717f7209022c632 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 9 Jul 2012 22:44:38 -0700
Subject: Bug fix in the recent changes to the SAT solver.

---
 src/sat/bsat/satSolver.c | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src')

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;
-- 
cgit v1.2.3