From c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 25 Aug 2020 15:00:11 -0300
Subject: [PATCH] Eliminating spurious replay of commands for define funs
 expansion when checking unsat cores (#4941)

Doing it via commands being added to the coreChecker SMT engine is not necessary since we can directly add assertions after expansion from the original SMT engine.
---
 src/smt/smt_engine.cpp | 20 +++++---------------
 src/smt/smt_engine.h   |  6 ------
 2 files changed, 5 insertions(+), 21 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 59df10195..98e865478 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -157,7 +157,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_abductSolver(nullptr),
       d_quantElimSolver(nullptr),
       d_assignments(nullptr),
-      d_defineCommands(),
       d_logic(),
       d_originalOptions(),
       d_isInternalSubsolver(false),
@@ -714,10 +713,6 @@ void SmtEngine::defineFunction(Expr func,
   d_dumpm->addToModelCommandAndDump(
       c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
-  PROOF(if (options::checkUnsatCores()) {
-    d_defineCommands.push_back(c.clone());
-  });
-
   // type check body
   debugCheckFunctionBody(formula, formals, func);
 
@@ -1555,17 +1550,12 @@ void SmtEngine::checkUnsatCore() {
   coreChecker.getOptions().set(options::checkUnsatCores, false);
   coreChecker.getOptions().set(options::checkProofs, false);
 
-  PROOF(
-  std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
-  for (; itg != d_defineCommands.end();  ++itg) {
-    (*itg)->invoke(&coreChecker);
-  }
-  );
-
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
-    coreChecker.assertFormula(Node::fromExpr(*i));
+    Node assertionAfterExpansion = expandDefinitions(Node::fromExpr(*i));
+    Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
+             << ", expanded to " << assertionAfterExpansion << "\n";
+    coreChecker.assertFormula(assertionAfterExpansion);
   }
   Result r;
   try {
@@ -1618,7 +1608,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     Assert(te != nullptr);
     te->checkTheoryAssertionsWithModel(hardFailure);
   }
-  
+
   // Output the model
   Notice() << *m;
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 28dc8726b..99c4a67d3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1114,12 +1114,6 @@ class CVC4_PUBLIC SmtEngine
    */
   AssignmentSet* d_assignments;
 
-  /**
-   * A vector of command definitions to be imported in the new
-   * SmtEngine when checking unsat-cores.
-   */
-  std::vector<Command*> d_defineCommands;
-
   /**
    * The logic we're in. This logic may be an extension of the logic set by the
    * user.
-- 
2.30.2