Remove more uses of Expr (#5357)

This PR removes more uses of Expr, mostly related to UnsatCore.

It makes UnsatCore a cvc4_private object storing Node instead of Expr.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d0906ce98..dc5338199 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1028,7 +1028,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   std::vector<Node>& assumps = d_asserts->getAssumptions();
   for (const Node& e : assumps)
   {
-    if (std::find(core.begin(), core.end(), e.toExpr()) != core.end())
+    if (std::find(core.begin(), core.end(), e) != core.end())
     {
       res.push_back(e);
     }
@@ -1490,7 +1490,7 @@ void SmtEngine::checkUnsatCore() {
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    Node assertionAfterExpansion = expandDefinitions(Node::fromExpr(*i));
+    Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
              << ", expanded to " << assertionAfterExpansion << "\n";
     coreChecker.assertFormula(assertionAfterExpansion);