Fix a small problem in clang builds due to namespaces and symbol lookup

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 474abfea37bddbba1c1e9de15bbc379e4af04833..af90886632dc3a3a5fc707033d14e80878463142 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -613,6 +613,8 @@ public:
 
 };/* class StatisticsRegistry */
 
+}/* CVC4 namespace */
+
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
@@ -621,6 +623,7 @@ 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);
@@ -643,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);
@@ -719,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;
 
 /**