X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=blobdiff_plain;f=glucose-syrup%2Fincremental%2FMain.cc;h=6b7ed12b82935246a1c696f4f11cadb91f59088a;hp=acb61b68b07c52e642ef076ee77ffcca02172554;hb=00598b79d3bc3d604a611ccd19a0f23f5f997597;hpb=33cbe1ee74163e94f6c5b6ede980d4f30037e86a

diff --git a/glucose-syrup/incremental/Main.cc b/glucose-syrup/incremental/Main.cc
index acb61b6..6b7ed12 100644
--- a/glucose-syrup/incremental/Main.cc
+++ b/glucose-syrup/incremental/Main.cc
@@ -71,13 +71,13 @@ int getInt() {
     offset = 0;
     do {
       ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
-      if (ptr == -1)
+      if (ptr == -1 || ptr == 0)
         exit(-1);
     } while(ptr==0);
     ssize_t bytestoread=(4-(ptr & 3)) & 3;
     while(bytestoread != 0) {
       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
-      if (p == -1)
+      if (p == -1 || p == 0)
         exit(-1);
       bytestoread -= p;
       ptr += p;
@@ -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);
         }
@@ -209,7 +208,7 @@ int main(int argc, char** argv) {
 #endif
     // Extra options:
     //
-    IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+    IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 0, IntRange(0, 2));
     BoolOption   mod   ("MAIN", "model",   "show model.", false);
     IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
     BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);