diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-13 00:03:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-13 00:03:35 -0600 |
| commit | 6beda739210b7bd13adbb7f62b0c4361156986ee (patch) | |
| tree | 1e86229fc763f589e22a1eab2541d87537fcea59 /src/smt/smt_engine.cpp | |
| parent | 5d0a5e5571044000fdaf0d908bace8ed7c1c536a (diff) | |
Distinguish unknown status for model printing (#3454)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7d28d8b85..073c2ebc5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3094,7 +3094,7 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (d_smtMode != SMT_MODE_SAT) + if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN) { std::stringstream ss; ss << "Cannot " << c @@ -3809,12 +3809,14 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, { d_smtMode = SMT_MODE_UNSAT; } - else + else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT) { - // Notice that unknown response moves to sat mode, since the same set - // of commands (get-model, get-value) are applicable to this case. d_smtMode = SMT_MODE_SAT; } + else + { + d_smtMode = SMT_MODE_SAT_UNKNOWN; + } Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -4410,6 +4412,7 @@ Model* SmtEngine::getModel() { ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); } m->d_inputName = d_filename; + m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT); return m; } |