From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 13 Aug 2013 15:59:26 +0000 (-0400)
Subject: --segv-nospin is now default.
X-Git-Tag: cvc5-1.0.0~7287^2~35
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c957465176d46a7f06a96393619db5e6f4fbda38;p=cvc5.git

--segv-nospin is now default.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 20a989106..d42f389c1 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -123,7 +123,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     exit(0);
   }
 
-  segvNoSpin = opts[options::segvNoSpin];
+  segvSpin = opts[options::segvSpin];
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
diff --git a/src/main/main.h b/src/main/main.h
index 0180c34d2..154919aa9 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -51,7 +51,7 @@ extern CVC4::TimerStat* pTotalTime;
  * Useful for nightly regressions, noninteractive performance runs
  * etc.  See util.cpp.
  */
-extern bool segvNoSpin;
+extern bool segvSpin;
 
 /** A pointer to the options in play */
 extern CVC4_THREADLOCAL(Options*) pOptions;
diff --git a/src/main/options b/src/main/options
index 14a7a9f3f..ba36e43ab 100644
--- a/src/main/options
+++ b/src/main/options
@@ -38,6 +38,10 @@ option fallbackSequential  --fallback-sequential bool :default false
 option incrementalParallel --incremental-parallel bool :default false :link --incremental
  Use parallel solver even in incremental mode (may print 'unknown's at times)
 
+option segvSpin --segv-spin bool :default false
+ spin on segfault/other crash waiting for gdb
+undocumented-alias --segv-nospin = --no-segv-spin
+
 expert-option waitToJoin --wait-to-join bool :default true
  wait for other threads to join before quitting
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5bd0c9bd4..14ee82613 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -54,7 +54,7 @@ namespace main {
  * Useful for nightly regressions, noninteractive performance runs
  * etc.
  */
-bool segvNoSpin = false;
+bool segvSpin = false;
 
 #ifndef __WIN32__
 
@@ -98,8 +98,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
 
-  if(segvNoSpin) {
-    fprintf(stderr, "No-spin requested, aborting...\n");
+  if(!segvSpin) {
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
@@ -133,8 +132,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 void ill_handler(int sig, siginfo_t* info, void*) {
 #ifdef CVC4_DEBUG
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
-  if(segvNoSpin) {
-    fprintf(stderr, "No-spin requested, aborting...\n");
+  if(!segvSpin) {
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
@@ -174,8 +172,7 @@ void cvc4unexpected() {
     fprintf(stderr, "The exception is:\n%s\n\n",
             static_cast<const char*>(CVC4::s_debugLastException));
   }
-  if(segvNoSpin) {
-    fprintf(stderr, "No-spin requested.\n");
+  if(!segvSpin) {
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
diff --git a/src/options/base_options b/src/options/base_options
index f9eb64ef2..a6f24c7f3 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -114,9 +114,6 @@ option parseOnly parse-only --parse-only bool :read-write
 option preprocessOnly preprocess-only --preprocess-only bool
  exit after preprocessing input
 
-option segvNoSpin --segv-nospin bool
- don't spin on segfault waiting for gdb
-
 option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag
  trace something (e.g. -t pushpop), can repeat
 option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag