diff options
Diffstat (limited to 'src/main/main.h')
| -rw-r--r-- | src/main/main.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/main/main.h b/src/main/main.h index 37430b507..b769bee7d 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -20,9 +20,6 @@ #include "base/exception.h" #include "cvc4autoconfig.h" #include "options/options.h" -#include "util/statistics.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" #ifndef CVC4__MAIN__MAIN_H #define CVC4__MAIN__MAIN_H @@ -41,9 +38,6 @@ extern const std::string* progName; /** A reference for use by the signal handlers to print statistics */ extern CVC4::main::CommandExecutor* pExecutor; -/** A reference for use by the signal handlers to print statistics */ -extern CVC4::TimerStat* pTotalTime; - /** * If true, will not spin on segfault even when CVC4_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs |