From 10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 6 Jan 2012 11:34:06 +0700
Subject: Bug fix related to not properly resizing SAT solver's model array.

---
 src/sat/bsat/satSolver2.c | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'src/sat/bsat/satSolver2.c')

diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index a4166fef..0da59fda 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1087,7 +1087,6 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
     s->stats.starts++;
 //    s->var_decay = (float)(1 / 0.95   );
 //    s->cla_decay = (float)(1 / 0.999);
-    veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
     for (;;){
@@ -1158,9 +1157,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
             if (next == var_Undef){
                 // Model found:
                 int i;
-                veci_resize(&s->model, 0);
                 for (i = 0; i < s->size; i++) 
-                    veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
+                    s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
                 solver2_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
 
@@ -1197,7 +1195,6 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
     veci_new(&s->stack);
-    veci_new(&s->model);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
     veci_new(&s->mark_levels);
@@ -1276,6 +1273,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
 #endif
+        s->model     = ABC_REALLOC(int,      s->model,    s->cap);
         memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
     }
 
@@ -1326,7 +1324,6 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
     veci_delete(&s->stack);
-    veci_delete(&s->model);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
     veci_delete(&s->mark_levels);
@@ -1354,6 +1351,7 @@ void sat_solver2_delete(sat_solver2* s)
         ABC_FREE(s->reasons  );
         ABC_FREE(s->units    );
         ABC_FREE(s->activity );
+        ABC_FREE(s->model    );
     }
     ABC_FREE(s);
 }
-- 
cgit v1.2.3