diff options
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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); |