diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a2dd8276b..63c970920 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1235,7 +1235,7 @@ void SmtEngine::setDefaults() { } if ((options::checkModels() || options::checkSynthSol() - || options::produceModelCores()) + || options::modelCoresMode() != MODEL_CORES_NONE) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " @@ -1432,7 +1432,7 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() && (options::produceAssignments() || options::sygusRewSynthCheck() - || options::produceModelCores() || is_sygus)) + || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); @@ -4263,12 +4263,12 @@ Model* SmtEngine::getModel() { } TheoryModel* m = d_theoryEngine->getModel(); - if (options::produceModelCores()) + if (options::modelCoresMode() != MODEL_CORES_NONE) { // 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); + ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode()); } m->d_inputName = d_filename; return m; |