diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-10-31 12:47:28 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-31 19:47:28 +0000 |
| commit | 47ddb344f317496928dddd4b017867b8c07dbded (patch) | |
| tree | 2e6bea17492542cb7e52d97679e33db7a8ebdfab | |
| parent | 08800bd63da929fd0439d0e743ace1a71aeffa14 (diff) | |
api: Add guard against querying value from term with free vars. (#7529)
| -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); |