3 files changed, 41 insertions, 11 deletions
diff --git a/include/klee/SolverStats.h b/include/klee/SolverStats.h
new file mode 100644
index 00000000..a38c9826
--- /dev/null
+++ b/include/klee/SolverStats.h
@@ -0,0 +1,38 @@
+//===-- SolverStats.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_SOLVERSTATS_H
+#define KLEE_SOLVERSTATS_H
+
+#include "klee/Statistic.h"
+
+namespace klee {
+namespace stats {
+
+  extern Statistic cexCacheTime;
+  extern Statistic queries;
+  extern Statistic queriesInvalid;
+  extern Statistic queriesValid;
+  extern Statistic queryCacheHits;
+  extern Statistic queryCacheMisses;
+  extern Statistic queryCexCacheHits;
+  extern Statistic queryCexCacheMisses;
+  extern Statistic queryConstructTime;
+  extern Statistic queryConstructs;
+  extern Statistic queryCounterexamples;
+  extern Statistic queryTime;
+  
+#ifdef DEBUG
+  extern Statistic arrayHashTime;
+#endif
+
+}
+}
+
+#endif
diff --git a/include/klee/util/ArrayCache.h b/include/klee/util/ArrayCache.h
index 3dd88a11..56d69df6 100644
--- a/include/klee/util/ArrayCache.h
+++ b/include/klee/util/ArrayCache.h
@@ -11,6 +11,7 @@
 #define KLEE_ARRAY_CACHE_H
 
 #include "klee/Expr.h"
+#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn
 
 // FIXME: Remove this hack when we switch to C++11
 #ifdef _LIBCPP_VERSION
@@ -26,15 +27,6 @@
 
 namespace klee {
 
-// FIXME: This is copied from ``klee/util/ArrayExprHash.h``.
-// We can't include it here becaues the includes are messed up
-// in that file.
-struct EquivArrayHashFn {
-  unsigned operator()(const Array *array) const {
-    return (array ? array->hash() : 0);
-  }
-};
-
 struct EquivArrayCmpFn {
   bool operator()(const Array *array1, const Array *array2) const {
     if (array1 == NULL || array2 == NULL)
@@ -76,7 +68,7 @@ public:
                            Expr::Width _range = Expr::Int8);
 
 private:
-  typedef unordered_set<const Array *, klee::EquivArrayHashFn,
+  typedef unordered_set<const Array *, klee::ArrayHashFn,
                         klee::EquivArrayCmpFn> ArrayHashMap;
   ArrayHashMap cachedSymbolicArrays;
   typedef std::vector<const Array *> ArrayPtrVec;
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h
index da3b1d2b..23211a70 100644
--- a/include/klee/util/ArrayExprHash.h
+++ b/include/klee/util/ArrayExprHash.h
@@ -12,7 +12,7 @@
 
 #include "klee/Expr.h"
 #include "klee/TimerStatIncrementer.h"
-#include "SolverStats.h"
+#include "klee/SolverStats.h"
 
 #include <map>