diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-15 16:40:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-15 16:40:37 -0600 |
commit | c163ebf20b2728515479e1f43d2beaa4ecf46944 (patch) | |
tree | 2987c8219d4189728e070bab00d7262d300fe46d | |
parent | 61e8e59b1cc27d555f8381809c2e313a79c83ddc (diff) |
Expand definitions prior to model core computation (#2707)
-rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
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; |