1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 00336a1e3..e9cb56b88 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -136,6 +136,10 @@ class TheoryEngine {
     }
 
     NodeBuilder<> b(in.getKind());
+    if(in.getMetaKind() == kind::metakind::PARAMETERIZED){
+      Assert(in.hasOperator());
+      b << in.getOperator();
+    }
     for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
       b << rewrite(*c);
     }
@@ -168,6 +172,8 @@ class TheoryEngine {
     }
   }
 
+  Node removeITEs(TNode t);
+
 public:
 
   /**
@@ -220,7 +226,14 @@ public:
     Assert(k >= 0 && k < kind::LAST_KIND);
 
     if(k == kind::VARIABLE) {
-      return &d_uf;
+      TypeNode t = n.getType();
+      if(t.isBoolean()){
+        return &d_bool;
+      }else if(t.isReal()){
+        return &d_arith;
+      }else{
+        return &d_uf;
+      }
       //Unimplemented();
     } else if(k == kind::EQUAL) {
       // if LHS is a VARIABLE, use theoryOf(LHS.getType())