bugfix
authorbdemsky <bdemsky@uci.edu>
Wed, 31 Dec 2014 12:42:55 +0000 (21:42 +0900)
committerbdemsky <bdemsky@uci.edu>
Wed, 31 Dec 2014 12:42:55 +0000 (21:42 +0900)
glucose-syrup/incremental/Main.cc

index 5ea6c13..acb61b6 100644 (file)
@@ -153,6 +153,7 @@ void processCommands(SimpSolver *solver) {
       if (ret == l_True) {
         putInt(IS_SAT);
         putInt(solver->nVars());
       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);
         }
         for(int i=0;i<solver->nVars();i++) {
           putInt(solver->model[i]==l_True);
         }