From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 15 Nov 2018 22:40:37 +0000 (-0600)
Subject:  Expand definitions prior to model core computation (#2707)
X-Git-Tag: cvc5-1.0.0~4366
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c163ebf20b2728515479e1f43d2beaa4ecf46944;p=cvc5.git

 Expand definitions prior to model core computation (#2707)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cb7766c2d..f3a6c0c9e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4306,7 +4306,16 @@ Model* SmtEngine::getModel() {
     // If we enabled model cores, we compute a model core for m based on our
     // assertions using the model core builder utility
     std::vector<Expr> easserts = getAssertions();
-    ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode());
+    // must expand definitions
+    std::vector<Expr> eassertsProc;
+    std::unordered_map<Node, Node, NodeHashFunction> cache;
+    for (unsigned i = 0, nasserts = easserts.size(); i < nasserts; i++)
+    {
+      Node ea = Node::fromExpr(easserts[i]);
+      Node eae = d_private->expandDefinitions(ea, cache);
+      eassertsProc.push_back(eae.toExpr());
+    }
+    ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
   }
   m->d_inputName = d_filename;
   return m;