diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-03-03 18:35:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-03-03 18:35:17 +0000 |
commit | 3dbabefa475f034f07276dc0bb0d86f61f2239c3 (patch) | |
tree | af815c0324caafe10eeb21d2fba29ddac315a846 /src/main | |
parent | 43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a (diff) |
fix for bug #244, "Segfault if file cannot be found and --stats is on"
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/main.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index fcd322e99..563fa472e 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -181,7 +181,7 @@ int runCvc4(int argc, char* argv[]) { const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; ReferenceStat< const char* > s_statFilename("filename", filename); - StatisticsRegistry::registerStat(&s_statFilename); + RegisterStatistic statFilenameReg(&s_statFilename); if(options.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { @@ -273,15 +273,12 @@ int runCvc4(int argc, char* argv[]) { #endif ReferenceStat< Result > s_statSatResult("sat/unsat", result); - StatisticsRegistry::registerStat(&s_statSatResult); + RegisterStatistic statSatResultReg(&s_statSatResult); if(options.statistics) { StatisticsRegistry::flushStatistics(*options.err); } - StatisticsRegistry::unregisterStat(&s_statSatResult); - StatisticsRegistry::unregisterStat(&s_statFilename); - return returnValue; } |