Version abc80202

2 files changed, 10 insertions, 0 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index fbc9874d..8a13d203 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -946,6 +946,7 @@ sat_solver* sat_solver_new(void)
     veci_new(&s->stack);
     veci_new(&s->model);
     veci_new(&s->act_vars);
+    veci_new(&s->temp_clause);
 
     // initialize arrays
     s->wlists    = 0;
@@ -1020,6 +1021,7 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->stack);
     veci_delete(&s->model);
     veci_delete(&s->act_vars);
+    veci_delete(&s->temp_clause);
     free(s->binary);
 
     // delete arrays
@@ -1052,6 +1054,12 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     lbool* values;
     lit last;
 
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = begin; i < end; i++ )
+        veci_push( &s->temp_clause, *i );
+    begin = veci_begin( &s->temp_clause );
+    end = begin + veci_size( &s->temp_clause );
+
     if (begin == end) return false;
 
     //printlits(begin,end); printf("\n");
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index c1bf32a7..9ffc2b75 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -187,6 +187,8 @@ struct sat_solver_t
     FILE *   pFile;
     int      nClauses;
     int      nRoots;
+
+    veci     temp_clause;    // temporary storage for a CNF clause
 };
 
 static int sat_solver_var_value( sat_solver* s, int v )