2 files changed, 9 insertions, 9 deletions
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 */