2 files changed, 15 insertions, 15 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2fb73cbed..166546a2c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -30,9 +30,9 @@ PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
   d_de(de), d_te(te), d_sat() {
 }
 
-void PropEngine::addVars(Expr e) {
+void PropEngine::addVars(Node e) {
   Debug("prop") << "adding vars to " << e << endl;
-  for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+  for(Node::iterator i = e.begin(); i != e.end(); ++i) {
     Debug("prop") << "expr " << *i << endl;
     if(i->getKind() == VARIABLE) {
       if(d_vars.find(*i) == d_vars.end()) {
@@ -45,18 +45,18 @@ void PropEngine::addVars(Expr e) {
   }
 }
 
-static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
+static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>* c) {
   if(e.getKind() == VARIABLE) {
-    map<Expr, Var>::iterator v = vars->find(e);
+    map<Node, Var>::iterator v = vars->find(e);
     Assert(v != vars->end());
     c->push(Lit(v->second, false));
     return;
   }
   if(e.getKind() == NOT) {
     Assert(e.numChildren() == 1);
-    Expr child = *e.begin();
+    Node child = *e.begin();
     Assert(child.getKind() == VARIABLE);
-    map<Expr, Var>::iterator v = vars->find(child);
+    map<Node, Var>::iterator v = vars->find(child);
     Assert(v != vars->end());
     c->push(Lit(v->second, true));
     return;
@@ -64,14 +64,14 @@ static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>*
   Unhandled();
 }
 
-static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
+static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
   vec<Lit> c;
   Debug("prop") << "  " << e << endl;
   if(e.getKind() == VARIABLE || e.getKind() == NOT) {
     doAtom(minisat, vars, e, &c);
   } else {
     Assert(e.getKind() == OR);
-    for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
       Debug("prop") << "    " << *i << endl;
       doAtom(minisat, vars, *i, &c);
     }
@@ -86,12 +86,12 @@ static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>*
   minisat->addClause(c);
 }
 
-void PropEngine::solve(Expr e) {
+void PropEngine::solve(Node e) {
   Debug("prop") << "SOLVING " << e << endl;
   addVars(e);
   if(e.getKind() == AND) {
     Debug("prop") << "AND" << endl;
-    for(Expr::iterator i = e.begin(); i != e.end(); ++i)
+    for(Node::iterator i = e.begin(); i != e.end(); ++i)
       doClause(&d_sat, &d_vars, &d_varsReverse, *i);
   } else doClause(&d_sat, &d_vars, &d_varsReverse, e);
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a3355bf89..21a6669d7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -13,7 +13,7 @@
 #define __CVC4__PROP_ENGINE_H
 
 #include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "util/decision_engine.h"
 #include "theory/theory_engine.h"
 #include "prop/minisat/simp/SimpSolver.h"
@@ -31,10 +31,10 @@ class PropEngine {
   DecisionEngine &d_de;
   TheoryEngine &d_te;
   CVC4::prop::minisat::SimpSolver d_sat;
-  std::map<Expr, CVC4::prop::minisat::Var> d_vars;
-  std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse;
+  std::map<Node, CVC4::prop::minisat::Var> d_vars;
+  std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
 
-  void addVars(Expr);
+  void addVars(Node);
 
 public:
   /**
@@ -45,7 +45,7 @@ public:
   /**
    * Converts to CNF if necessary.
    */
-  void solve(Expr);
+  void solve(Node);
 
 };/* class PropEngine */