diff options
author | Tim King <taking@cs.nyu.edu> | 2010-07-06 23:48:49 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-07-06 23:48:49 +0000 |
commit | bba85281eef7daefa8a1bd6673d38e1d005cf789 (patch) | |
tree | f676686c3f7f0cd04854406e4c4f026ae44f1091 /src/main/main.cpp | |
parent | 2db22ffd1f48502a2b138b9b99ba2841a581313b (diff) |
Fixed exit status for competition mode.
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 37 |
1 files changed, 21 insertions, 16 deletions
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; } |