From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 3 Feb 2022 00:18:45 +0000 (-0800)
Subject: api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)
X-Git-Tag: cvc5-1.0.0~468
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=676b43d08a40b7e83002461e8a76421280f8ce4f;p=cvc5.git

api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)

Fixes cvc5/cvc5-projects#412.
---

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<Term>& 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)