3 files changed, 5 insertions, 4 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a66e36a07..6e3b6ae2f 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -23,6 +23,7 @@
 #include <queue>
 
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5dd57610d..76be5d6d8 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -49,14 +49,14 @@ PropEngine::~PropEngine() {
   delete d_satSolver;
 }
 
-void PropEngine::assertFormula(const Node& node) {
+void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
   d_cnfStream->convertAndAssert(node);
 }
 
-void PropEngine::assertLemma(const Node& node) {
+void PropEngine::assertLemma(TNode node) {
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as removable
   d_cnfStream->convertAndAssert(node);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d4007e73a..4ea5e3b78 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -77,14 +77,14 @@ public:
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert
    */
-  void assertFormula(const Node& node);
+  void assertFormula(TNode node);
 
   /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
    * The formula can be removed by the sat solver.
    * @param node the formula to assert
    */
-  void assertLemma(const Node& node);
+  void assertLemma(TNode node);
 
   /**
    * Checks the current context for satisfiability.