3 files changed, 11 insertions, 14 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index ea5f18c9..df55d126 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -12,6 +12,7 @@
 
 #include "Machine.h"
 #include "klee/util/Bits.h"
+#include "klee/util/Ref.h"
 
 #include "llvm/Support/Streams.h"
 #include "llvm/ADT/SmallVector.h"
@@ -188,6 +189,7 @@ public:
 
   ///
 
+  bool isConstant() const { return getKind() == Expr::Constant; }
   uint64_t getConstantValue() const;
 
   /* Static utility methods */
@@ -224,11 +226,6 @@ public:
   static bool isValidKidWidth(unsigned kid, Width w) { return true; }
   static bool needsResultType() { return false; }
 };
-// END class Expr
-
-
-
-#include "klee/util/Ref.h"
 
 struct Expr::CreateArg {
   ref<Expr> expr;
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 54f6b0af..36f4739d 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -90,7 +90,7 @@ namespace klee {
     AssignmentEvaluator v(*this);
     for (; begin!=end; ++begin) {
       ref<Expr> res = v.visit(*begin);
-      if (!res.isConstant() || !res->getConstantValue())
+      if (!res->isConstant() || !res->getConstantValue())
         return false;
     }
     return true;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index e2421bb0..1a633fb5 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -10,10 +10,11 @@
 #ifndef KLEE_REF_H
 #define KLEE_REF_H
 
+#include "llvm/Support/Streams.h"
+
 #include <assert.h>
 
-class Expr;
-class ConstantExpr;
+namespace klee {
 
 template<class T>
 class ref {
@@ -68,11 +69,6 @@ public:
     return ptr;
   }
 
-  // method calls for the constant optimization
-  bool isConstant() const {
-    return ptr && ptr->getKind() == Expr::Constant;
-  }
-
   /* The copy assignment operator must also explicitly be defined,
    * despite a redundant template. */
   ref<T> &operator= (const ref<T> &r) {
@@ -116,10 +112,12 @@ public:
 
 template<class T>
 inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
-  os << *e.get();
+  os << *e;
   return os;
 }
 
+class Expr;
+
 template<class U>
 U* dyn_ref_cast(ref<Expr> &src) {
   return dynamic_cast<U*>(src.ptr);
@@ -140,4 +138,6 @@ const U* static_ref_cast(const ref<Expr> &src) {
   return static_cast<const U*>(src.ptr);
 }
 
+}
+
 #endif /* KLEE_REF_H */