1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f8eece3df..2411956f5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -36,18 +36,18 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
+namespace theory {
+
 /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-struct Registered {};
+struct RegisteredAttrTag {};
 /** The "registerTerm()-has-been-called" flag on Nodes */
-typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
-
-namespace theory {
+typedef CVC4::expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr;
 
-struct PreRegisteredTag {};
-typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
+struct PreRegisteredAttrTag {};
+typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegistered;
 
-struct IteRewriteTag {};
-typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
+struct IteRewriteAttrTag {};
+typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
 
 }/* CVC4::theory namespace */
 
@@ -136,7 +136,6 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
-  d_valuation(this),
   d_opts(opts),
   d_statistics() {
 
@@ -347,7 +346,7 @@ Node TheoryEngine::getValue(TNode node) {
   }
 
   // otherwise ask the theory-in-charge
-  return theoryOf(node)->getValue(node, &d_valuation);
+  return theoryOf(node)->getValue(node);
 }/* TheoryEngine::getValue(TNode node) */
 
 bool TheoryEngine::presolve() {