From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sun, 31 Oct 2021 19:47:28 +0000 (-0700)
Subject: api: Add guard against querying value from term with free vars. (#7529)
X-Git-Tag: cvc5-1.0.0~923
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=47ddb344f317496928dddd4b017867b8c07dbded;p=cvc5.git

api: Add guard against querying value from term with free vars. (#7529)
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index addfeb0da..d1be25bb4 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5056,6 +5056,8 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
 Term Solver::getValueHelper(const Term& term) const
 {
   // Note: Term is checked in the caller to avoid double checks
+  CVC5_API_RECOVERABLE_CHECK(!expr::hasFreeVar(term.getNode()))
+      << "Cannot get value of term containing free variables";
   //////// all checks before this line
   Node value = d_slv->getValue(*term.d_node);
   Term res = Term(this, value);