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.cpp | |
| parent | 55e24949a3464947d098eeeb627049b04a4af4a3 (diff) | |
driver::totalTime statistic is now reported correctly on crashes, too
Diffstat (limited to 'src/main/main.cpp')
| -rw-r--r-- | src/main/main.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 3e45b4f14..a83baf45f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -66,6 +66,7 @@ int main(int argc, char* argv[]) { #endif *opts[options::err] << "CVC4 Error:" << endl << e << endl; if(opts[options::statistics] && pExecutor != NULL) { + pTotalTime->stop(); pExecutor->flushStatistics(*opts[options::err]); } } |