From 900b7443455dd44398e580b957064d8fb98bd8fb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Oct 2010 22:08:54 +0000 Subject: [PATCH] with --stats, statistics are dumped for memouts and (normal) exceptions. --- src/main/main.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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); } -- 2.30.2