diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a7cc8e17f..1112530d3 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5160,11 +5160,11 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get value when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Cannot get value unless after a SAT or unknown response."; std::vector<Term> res; for (size_t i = 0, n = terms.size(); i < n; ++i) { @@ -5222,8 +5222,8 @@ Term Solver::getSeparationHeap() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get separtion heap term when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only get separtion heap term after sat or unknown response."; return Term(this, d_smtEngine->getSepHeapExpr()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5239,8 +5239,8 @@ Term Solver::getSeparationNilTerm() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get separtion nil term when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only get separtion nil term after sat or unknown response."; return Term(this, d_smtEngine->getSepNilExpr()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5330,8 +5330,8 @@ void Solver::printModel(std::ostream& out) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get value when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only get value after sat or unknown response."; out << *d_smtEngine->getModel(); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5343,8 +5343,8 @@ void Solver::blockModel() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get value when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only block model after sat or unknown response."; d_smtEngine->blockModel(); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5355,8 +5355,8 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) - << "Cannot get value when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only block model values after sat or unknown response."; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; for (size_t i = 0, tsize = terms.size(); i < tsize; ++i) |