diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/system/statistics.cpp | 2 | ||||
-rw-r--r-- | test/unit/util/stats_black.h | 15 |
2 files changed, 15 insertions, 2 deletions
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 884ffb8a6..18b1e5937 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -19,9 +19,9 @@ #include <sstream> #include "expr/expr.h" -#include "expr/statistics.h" #include "smt/smt_engine.h" #include "util/sexpr.h" +#include "util/statistics.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index c0e1ea7fd..dd67429cf 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -19,11 +19,24 @@ #include <string> #include <ctime> -#include "expr/statistics_registry.h" +#include "lib/clock_gettime.h" +#include "util/statistics_registry.h" using namespace CVC4; using namespace std; +/** + * This is a duplicate of operator== in statistics_registry.h. + * This is duplicated here to try to avoid polluting top namepsace. + * + * If operator== is in the CVC4 namespace, there are some circumstances + * where clang does not find this operator. + */ +bool operator==(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} + class StatsBlack : public CxxTest::TestSuite { public: |