From 47ddb344f317496928dddd4b017867b8c07dbded Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sun, 31 Oct 2021 12:47:28 -0700
Subject: [PATCH] api: Add guard against querying value from term with free
 vars. (#7529)

---
 src/api/cpp/cvc5.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);
-- 
2.30.2