diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-12-01 14:28:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-01 22:28:37 +0000 |
| commit | 1339d73750e15422a5c2085c4819c15b77bededd (patch) | |
| tree | 9da606eccb8238f4ddfae526c6fecf1a147a02e1 | |
| parent | d676cc2b2d279041d26804c47494a2206bb74874 (diff) | |
api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)
| -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 << ")"; } |