Work around occasional hang with -g (when timing out).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1038 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d44dd6b1cc09918336dbfcf7c1e77b369890ae0d..901e2756f91b97fdb4867fe606108d379ed41392 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -32,7 +32,21 @@ extern int smt2lex_destroy(void);
 // callback for SIGALRM.
 void handle_time_out(int parameter){
   printf("Timed Out.\n");
-  exit(0);
+
+  abort();
+  // I replaced the exit(0) with an abort().
+  // The exit was sometimes hanging, seemingly because of a bug somewhere else (e.g. loader, glibc).
+  // In strace it output:
+
+  //--- SIGVTALRM (Virtual timer expired) @ 0 (0) ---
+  //fstat(1, {st_mode=S_IFCHR|0620, st_rdev=makedev(136, 5), ...}) = 0
+  //mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fabca622000
+  //write(1, "Timed Out.\n", 11Timed Out.
+  //)            = 11
+  //futex(0x7fabc9c54e40, FUTEX_WAIT, 2, NULL
+
+  // Then it would just sit there waiting for the mutex (which never came).
+  //exit(0);
 }
 
 bool onePrintBack =false;
@@ -329,7 +343,7 @@ int main(int argc, char ** argv) {
               timeout.it_value.tv_usec    = 0;
               timeout.it_value.tv_sec     = atoi(argv[++i]);
               setitimer(ITIMER_VIRTUAL, &timeout, NULL);
-              break;            
+              break;
             case 'h':
               fprintf(stderr,usage,prog);
               cout << helpstring;