From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 2 Oct 2010 22:14:44 +0000 (+0000)
Subject: dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout...
X-Git-Tag: cvc5-1.0.0~8835
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=999b496fbf50525b7245ee28e972d7f0f04a1025;p=cvc5.git

dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout...
---

diff --git a/src/main/util.cpp b/src/main/util.cpp
index e91e80c3f..65f6ed329 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -78,6 +78,9 @@ void segv_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 suffered a segfault.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   abort();
 #endif /* CVC4_DEBUG */
 }
@@ -88,6 +91,9 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
+    if(options.statistics) {
+      StatisticsRegistry::flushStatistics(cerr);
+    }
     abort();
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
@@ -98,6 +104,9 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   abort();
 #endif /* CVC4_DEBUG */
 }
@@ -119,6 +128,9 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
+    if(options.statistics) {
+      StatisticsRegistry::flushStatistics(cerr);
+    }
     set_terminate(default_terminator);
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
@@ -129,6 +141,9 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
 }
@@ -139,11 +154,17 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   default_terminator();
 #endif /* CVC4_DEBUG */
 }