diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 22:08:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 22:08:54 +0000 |
commit | 900b7443455dd44398e580b957064d8fb98bd8fb (patch) | |
tree | d13ba7f38d04be1ed2bb45e60e67c35ed084a709 /src/main | |
parent | a47b818c883eafb74afe066915bbbedf760c31e1 (diff) |
with --stats, statistics are dumped for memouts and (normal) exceptions.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/main.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
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); } |