diff options
Diffstat (limited to 'src/main/main.h')
| -rw-r--r-- | src/main/main.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/main/main.h b/src/main/main.h index 5b202c532..56cd866da 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -23,6 +23,7 @@ #include "util/exception.h" #include "util/statistics.h" #include "util/tls.h" +#include "util/statistics_registry.h" #include "cvc4autoconfig.h" #ifndef __CVC4__MAIN__MAIN_H @@ -42,6 +43,9 @@ extern const char* 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 |