1 files changed, 26 insertions, 13 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index ba5d06672..76ca7a925 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -47,7 +47,7 @@ using namespace CVC4::parser;
 using namespace CVC4::main;
 
 static int runCvc4(int argc, char* argv[]);
-static void doCommand(SmtEngine&, Command*);
+static bool doCommand(SmtEngine&, Command*);
 static void printUsage(bool full = false);
 
 namespace CVC4 {
@@ -277,6 +277,7 @@ static int runCvc4(int argc, char* argv[]) {
 
   // Parse and execute commands until we are done
   Command* cmd;
+  bool status = true;
   if( options.interactive ) {
     InteractiveShell shell(exprMgr, options);
     Message() << Configuration::getPackageName()
@@ -293,7 +294,7 @@ static int runCvc4(int argc, char* argv[]) {
       replayParser->useDeclarationsFrom(shell.getParser());
     }
     while((cmd = shell.readCommand())) {
-      doCommand(smt,cmd);
+      status = status && doCommand(smt, cmd);
       delete cmd;
     }
   } else {
@@ -309,7 +310,7 @@ static int runCvc4(int argc, char* argv[]) {
       replayParser->useDeclarationsFrom(parser);
     }
     while((cmd = parser->nextCommand())) {
-      doCommand(smt, cmd);
+      status = status && doCommand(smt, cmd);
       delete cmd;
     }
     // Remove the parser
@@ -322,15 +323,21 @@ static int runCvc4(int argc, char* argv[]) {
     options.replayStream = NULL;
   }
 
-  string result = smt.getInfo(":status").getValue();
   int returnValue;
-
-  if(result == "sat") {
-    returnValue = 10;
-  } else if(result == "unsat") {
-    returnValue = 20;
+  string result = "unknown";
+  if(status) {
+    result = smt.getInfo(":status").getValue();
+
+    if(result == "sat") {
+      returnValue = 10;
+    } else if(result == "unsat") {
+      returnValue = 20;
+    } else {
+      returnValue = 0;
+    }
   } else {
-    returnValue = 0;
+    // there was some kind of error
+    returnValue = 1;
   }
 
 #ifdef CVC4_COMPETITION_MODE
@@ -350,17 +357,20 @@ static int runCvc4(int argc, char* argv[]) {
 }
 
 /** Executes a command. Deletes the command after execution. */
-static void doCommand(SmtEngine& smt, Command* cmd) {
+static bool doCommand(SmtEngine& smt, Command* cmd) {
   if( options.parseOnly ) {
-    return;
+    return true;
   }
 
+  // assume no error
+  bool status = true;
+
   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
   if(seq != NULL) {
     for(CommandSequence::iterator subcmd = seq->begin();
         subcmd != seq->end();
         ++subcmd) {
-      doCommand(smt, *subcmd);
+      status = status && doCommand(smt, *subcmd);
     }
   } else {
     if(options.verbosity > 0) {
@@ -372,5 +382,8 @@ static void doCommand(SmtEngine& smt, Command* cmd) {
     } else {
       cmd->invoke(&smt);
     }
+    status = status && cmd->ok();
   }
+
+  return status;
 }