1 files changed, 9 insertions, 2 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3bf990dbb..af9088663 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,12 +613,17 @@ public:
 
 };/* class StatisticsRegistry */
 
+}/* CVC4 namespace */
+
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /** Compute the sum of two timespecs. */
 inline timespec& operator+=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -640,6 +646,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
 
 /** Compute the difference of two timespecs. */
 inline timespec& operator-=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -716,6 +723,8 @@ inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 }
 
+namespace CVC4 {
+
 class CodeTimer;
 
 /**
@@ -765,7 +774,6 @@ public:
 
 };/* class TimerStat */
 
-
 /**
  * Utility class to make it easier to call stop() at the end of a
  * code block.  When constructed, it starts the timer.  When
@@ -788,7 +796,6 @@ public:
   }
 };/* class CodeTimer */
 
-
 /**
  * To use a statistic, you need to declare it, initialize it in your
  * constructor, register it in your constructor, and deregister it in