diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-30 18:55:44 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 17:54:42 -0500 |
| commit | 00514e3804ebde7053ba095c678625a9035dc5e3 (patch) | |
| tree | c9de4824324698c214dd8dbbdf96b0a426ddb40d /src/main/main.h | |
| parent | 55e24949a3464947d098eeeb627049b04a4af4a3 (diff) | |
driver::totalTime statistic is now reported correctly on crashes, too
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 |