summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/main/main.cpp37
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback