Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

1 files changed, 11 insertions, 1 deletions

diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index ef6b99715..042a8ef1d 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
- ** Minor contributors (to current version): barrett, dejan, taking
+ ** Minor contributors (to current version): barrett, dejan, taking, kshitij
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011, 2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -82,6 +82,10 @@ void printUsage(Options& options, bool full) {
 
 int runCvc4(int argc, char* argv[], Options& options) {
 
+  // Timer statistic
+  TimerStat s_totalTime("totalTime");
+  s_totalTime.start();
+
   // For the signal handlers' benefit
   pOptions = &options;
 
@@ -161,6 +165,10 @@ int runCvc4(int argc, char* argv[], Options& options) {
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
+  // Timer statistic
+  RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
+
+  // Filename statistics
   ReferenceStat< const char* > s_statFilename("filename", filename);
   RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 
@@ -308,6 +316,8 @@ int runCvc4(int argc, char* argv[], Options& options) {
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
   RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
 
+  s_totalTime.stop();
+
   if(options.statistics) {
     pStatistics->flushInformation(*options.err);
   }