--segv-nospin is now default.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 20a9891064f90aee124403af51ab1308492047b4..d42f389c19db9a85a00c8ed0814d001ba2987765 100644 (file)
--- 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 0180c34d21b046754a5f9178ad89e82b77fe135a..154919aa9811d1ea45bf93dbb3d9f85ad024b4a7 100644 (file)
--- 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 14a7a9f3fe4c1f4fb142bb94c859ceea8039a66d..ba36e43abd46cd208ad6d40e5b7e94be3dce0bf5 100644 (file)
--- 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 5bd0c9bd4918f65237ce6e78e8e5f944dd273a5b..14ee82613665e8885b73e7bb8b6eae22c084ba6d 100644 (file)
--- 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 f9eb64ef209608ab138c0b1848768337ab729fff..a6f24c7f35c39eca9e6c81942c243eb8510fae1b 100644 (file)
--- 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