From 676b43d08a40b7e83002461e8a76421280f8ce4f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Feb 2022 16:18:45 -0800 Subject: [PATCH] api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958) Fixes cvc5/cvc5-projects#412. --- src/api/cpp/cvc5.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4371bac8d..449ec1414 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7637,6 +7637,9 @@ void Solver::blockModelValues(const std::vector& terms) const CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; + CVC5_API_CHECK(d_slv->getOptions().smt.produceAssertions) + << "Cannot block model value unless produce-assertions is enabled " + "(try --produce-assertions)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only block model values after SAT or UNKNOWN response."; CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) -- 2.30.2