From: Tim King <taking@cs.nyu.edu>
Date: Tue, 6 Jul 2010 23:48:49 +0000 (+0000)
Subject: Fixed exit status for competition mode.
X-Git-Tag: cvc5-1.0.0~8934
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bba85281eef7daefa8a1bd6673d38e1d005cf789;p=cvc5.git

Fixed exit status for competition mode.
---

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 0cf712e3b..0b962bc9b 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -182,10 +182,28 @@ int runCvc4(int argc, char* argv[]) {
     delete cmd;
   }
 
+  Result asSatResult = lastResult.asSatisfiabilityResult();
+  
+
+  int returnValue;
+
+  switch(asSatResult.isSAT()) {
+
+  case Result::SAT:
+    returnValue = 10;
+    break;
+  case Result::UNSAT:
+    returnValue = 20;
+    break;
+  default:
+    returnValue = 0;
+    break;
+  }
+
 #ifdef CVC4_COMPETITION_MODE
   // exit, don't return
   // (don't want destructors to run)
-  exit(0);
+  exit(returnValue);
 #endif
 
   // Get ready for tear-down
@@ -193,27 +211,14 @@ int runCvc4(int argc, char* argv[]) {
 
   // Remove the parser
   delete parser;
-
-  Result asSatResult = lastResult.asSatisfiabilityResult();
-  ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
+ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
   StatisticsRegistry::registerStat(&s_statSatResult);
 
   if(options.statistics){
     StatisticsRegistry::flushStatistics(cerr);
   }
 
-  switch(lastResult.asSatisfiabilityResult().isSAT()) {
-
-  case Result::SAT:
-    return 10;
-
-  case Result::UNSAT:
-    return 20;
-
-  default:
-    return 0;
-
-  }
+  return returnValue;
 
 }