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.

1 files changed, 5 insertions, 15 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;