From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 21 Dec 2010 12:34:26 +0000 (+0000)
Subject: Work around occasional hang with -g (when timing out).
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=422764a3749be929f8e4f7f80cc7a91842e07805;p=francis%2Fstp.git

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 d44dd6b..901e275 100644
--- 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;