diff options
Diffstat (limited to 'src/smt/smt_engine_stats.cpp')
| -rw-r--r-- | src/smt/smt_engine_stats.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 964237499..9b25580d2 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -32,8 +32,7 @@ SmtEngineStatistics::SmtEngineStatistics() d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), - d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_numConstantProps); @@ -48,7 +47,6 @@ SmtEngineStatistics::SmtEngineStatistics() smtStatisticsRegistry()->registerStat(&d_pushPopTime); smtStatisticsRegistry()->registerStat(&d_processAssertionsTime); smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed); } SmtEngineStatistics::~SmtEngineStatistics() @@ -66,7 +64,6 @@ SmtEngineStatistics::~SmtEngineStatistics() smtStatisticsRegistry()->unregisterStat(&d_pushPopTime); smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime); smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed); } } // namespace smt |