From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 12 Oct 2010 22:08:54 +0000 (+0000)
Subject: with --stats, statistics are dumped for memouts and (normal) exceptions.
X-Git-Tag: cvc5-1.0.0~8803
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=900b7443455dd44398e580b957064d8fb98bd8fb;p=cvc5.git

with --stats, statistics are dumped for memouts and (normal) exceptions.
---

diff --git a/src/main/main.cpp b/src/main/main.cpp
index f78637d82..d879e81df 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -73,12 +73,18 @@ int main(int argc, char* argv[]) {
     cout << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
+    if(options.statistics) {
+      StatisticsRegistry::flushStatistics(cerr);
+    }
     exit(1);
   } catch(bad_alloc) {
 #ifdef CVC4_COMPETITION_MODE
     cout << "unknown" << endl;
 #endif
     cerr << "CVC4 ran out of memory." << endl;
+    if(options.statistics) {
+      StatisticsRegistry::flushStatistics(cerr);
+    }
     exit(1);
   } catch(...) {
 #ifdef CVC4_COMPETITION_MODE
@@ -224,7 +230,7 @@ int runCvc4(int argc, char* argv[]) {
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
   StatisticsRegistry::registerStat(&s_statSatResult);
 
-  if(options.statistics){
+  if(options.statistics) {
     StatisticsRegistry::flushStatistics(cerr);
   }