summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-03-03 18:35:17 +0000
committerMorgan Deters <mdeters@gmail.com>2011-03-03 18:35:17 +0000
commit3dbabefa475f034f07276dc0bb0d86f61f2239c3 (patch)
treeaf815c0324caafe10eeb21d2fba29ddac315a846 /src/main
parent43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a (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.cpp7
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback