1 files changed, 13 insertions, 9 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 93b07b762..20b0e8a92 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -95,17 +95,18 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
   d_cnfProof->popCurrentAssertion();
 }
 
-
-void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
+void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions)
+{
   Debug("cores") << "trace deps " << n << std::endl;
   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
     return;
   }
-  if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+  if (d_inputCoreFormulas.find(n) != d_inputCoreFormulas.end())
+  {
     // originating formula was in core set
     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
-    coreAssertions->insert(n.toExpr());
+    coreAssertions->insert(n);
   } else {
     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
     if(d_deps.find(n) == d_deps.end()) {
@@ -151,8 +152,9 @@ bool ProofManager::unsatCoreAvailable() const {
   return d_satProof->derivedEmptyClause();
 }
 
-std::vector<Expr> ProofManager::extractUnsatCore() {
-  std::vector<Expr> result;
+std::vector<Node> ProofManager::extractUnsatCore()
+{
+  std::vector<Node> result;
   output_core_iterator it = begin_unsat_core();
   output_core_iterator end = end_unsat_core();
   while ( it != end ) {
@@ -190,9 +192,10 @@ void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
   }
 }
 
-void ProofManager::addCoreAssertion(Expr formula) {
+void ProofManager::addCoreAssertion(Node formula)
+{
   Debug("cores") << "assert: " << formula << std::endl;
-  d_deps[Node::fromExpr(formula)]; // empty vector of deps
+  d_deps[formula];  // empty vector of deps
   d_inputCoreFormulas.insert(formula);
 }
 
@@ -208,7 +211,8 @@ void ProofManager::addDependence(TNode n, TNode dep) {
   }
 }
 
-void ProofManager::addUnsatCore(Expr formula) {
+void ProofManager::addUnsatCore(Node formula)
+{
   Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
   d_outputCoreFormulas.insert(formula);
 }