2 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index a276fa0ce..1c779bd79 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
+Node TheoryBuiltin::getValue(TNode n) {
   switch(n.getKind()) {
 
   case kind::VARIABLE:
@@ -39,7 +39,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
     Assert(n[0].getKind() == kind::TUPLE &&
            n[1].getKind() == kind::TUPLE);
     return NodeManager::currentNM()->
-      mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) );
+      mkConst( getValue(n[0]) == getValue(n[1]) );
   }
 
   case kind::TUPLE: { // 2+ args
@@ -48,7 +48,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
           iend = n.end();
         i != iend;
         ++i) {
-      nb << valuation->getValue(*i);
+      nb << d_valuation.getValue(*i);
     }
     return Node(nb);
   }
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 5b9810326..4e62401ff 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -29,9 +29,9 @@ namespace builtin {
 
 class TheoryBuiltin : public Theory {
 public:
-  TheoryBuiltin(context::Context* c, OutputChannel& out) :
-    Theory(THEORY_BUILTIN, c, out) {}
-  Node getValue(TNode n, Valuation* valuation);
+  TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
+    Theory(THEORY_BUILTIN, c, out, valuation) {}
+  Node getValue(TNode n);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */