2 files changed, 12 insertions, 12 deletions
diff --git a/src/util/command.cpp b/src/util/command.cpp
index ed6b61703..0953a2ba2 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -7,7 +7,7 @@
 
 #include "util/command.h"
 #include "smt/smt_engine.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "util/result.h"
 
 using namespace std;
@@ -26,7 +26,7 @@ EmptyCommand::EmptyCommand(string name) :
 void EmptyCommand::invoke(SmtEngine* smt_engine) {
 }
 
-AssertCommand::AssertCommand(const Expr& e) :
+AssertCommand::AssertCommand(const Node& e) :
   d_expr(e) {
 }
 
@@ -37,7 +37,7 @@ void AssertCommand::invoke(SmtEngine* smt_engine) {
 CheckSatCommand::CheckSatCommand() {
 }
 
-CheckSatCommand::CheckSatCommand(const Expr& e) :
+CheckSatCommand::CheckSatCommand(const Node& e) :
   d_expr(e) {
 }
 
@@ -45,7 +45,7 @@ void CheckSatCommand::invoke(SmtEngine* smt_engine) {
   smt_engine->checkSat(d_expr);
 }
 
-QueryCommand::QueryCommand(const Expr& e) :
+QueryCommand::QueryCommand(const Node& e) :
   d_expr(e) {
 }
 
diff --git a/src/util/command.h b/src/util/command.h
index 31acbc43b..189872220 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -15,12 +15,12 @@
 #include <iostream>
 
 #include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 
 namespace CVC4 {
   class SmtEngine;
   class Command;
-  class Expr;
+  class Node;
 }/* CVC4 namespace */
 
 namespace CVC4 {
@@ -46,9 +46,9 @@ private:
 
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
-  Expr d_expr;
+  Node d_expr;
 public:
-  AssertCommand(const Expr& e);
+  AssertCommand(const Node& e);
   void invoke(CVC4::SmtEngine* smt_engine);
   void toString(std::ostream& out) const;
 };/* class AssertCommand */
@@ -57,21 +57,21 @@ public:
 class CVC4_PUBLIC CheckSatCommand : public Command {
 public:
   CheckSatCommand();
-  CheckSatCommand(const Expr& e);
+  CheckSatCommand(const Node& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Expr d_expr;
+  Node d_expr;
 };/* class CheckSatCommand */
 
 
 class CVC4_PUBLIC QueryCommand : public Command {
 public:
-  QueryCommand(const Expr& e);
+  QueryCommand(const Node& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Expr d_expr;
+  Node d_expr;
 };/* class QueryCommand */