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 addfeb0dae61baffb90a699a0f471e33d15b053f..d1be25bb47f543bdae86fb5ab46fdd90bf570434 100644 (file)
--- 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);