summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/system/statistics.cpp2
-rw-r--r--test/unit/util/stats_black.h15
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback