diff options
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 3edff5ec3..6129ff891 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5081,6 +5081,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const { + CVC5_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; CVC5_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC5_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; @@ -5090,7 +5091,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, if (val.strictlyNegative()) { - CVC5_API_CHECK(val >= -Integer("2", 10).pow(size - 1)) + CVC5_API_CHECK(val >= -Integer(2).pow(size - 1)) << "Overflow in bitvector construction (specified bitvector size " << size << " too small to hold value " << s << ")"; } |