From 9b70f290bb39bdddb840e9f6d2e15edf0c6b98f6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 31 Jan 2013 16:54:22 -0500 Subject: [PATCH] Fix a small problem in clang builds due to namespaces and symbol lookup --- src/util/statistics_registry.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 474abfea3..af9088663 100644 --- 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; /** -- 2.30.2