From 13e5f2c30c1ba823c7141b2d94caa1d216c7a040 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 31 Dec 2014 22:05:39 +0900
Subject: [PATCH] bug fix

---
 glucose-syrup/incremental/Main.cc | 1 -
 inc_solver.cc                     | 5 +++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/glucose-syrup/incremental/Main.cc b/glucose-syrup/incremental/Main.cc
index acb61b6..5ea6c13 100644
--- a/glucose-syrup/incremental/Main.cc
+++ b/glucose-syrup/incremental/Main.cc
@@ -153,7 +153,6 @@ void processCommands(SimpSolver *solver) {
       if (ret == l_True) {
         putInt(IS_SAT);
         putInt(solver->nVars());
-        putInt(0);
         for(int i=0;i<solver->nVars();i++) {
           putInt(solver->model[i]==l_True);
         }
diff --git a/inc_solver.cc b/inc_solver.cc
index 28444bc..24c6e88 100644
--- a/inc_solver.cc
+++ b/inc_solver.cc
@@ -48,9 +48,10 @@ int IncrementalSolver::solve() {
     if (numVars > solutionsize) {
       if (solution != NULL)
         free(solution);
-      solution = (int *) malloc(numVars*sizeof(int));
+      solution = (int *) malloc((numVars+1)*sizeof(int));
+      solution[0] = 0;
     }
-    readSolver(solution, numVars * sizeof(int));
+    readSolver(&solution[1], numVars * sizeof(int));
   }
   return result;
 }
-- 
2.34.1