Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

1 files changed, 1 insertions, 22 deletions

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 32aa33bed..474abfea3 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -23,6 +23,7 @@
 
 #include "util/statistics.h"
 #include "util/exception.h"
+#include "lib/clock_gettime.h"
 
 #include <sstream>
 #include <iomanip>
@@ -612,8 +613,6 @@ public:
 
 };/* class StatisticsRegistry */
 
-#ifndef __WIN32__
-
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
@@ -769,26 +768,6 @@ public:
 
 };/* class TimerStat */
 
-#else /* __WIN32__ */
-
-class CodeTimer;
-
-class TimerStat : public IntStat {
-public:
-
-  typedef CVC4::CodeTimer CodeTimer;
-
-  TimerStat(const std::string& name) :
-    IntStat(name, 0) {
-  }
-
-  void start();
-  void stop();
-
-};/* class TimerStat */
-
-#endif /* __WIN32__ */
-
 /**
  * Utility class to make it easier to call stop() at the end of a
  * code block.  When constructed, it starts the timer.  When