From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 1 Dec 2021 22:28:37 +0000 (-0800)
Subject: api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)
X-Git-Tag: cvc5-1.0.0~739
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1339d73750e15422a5c2085c4819c15b77bededd;p=cvc5.git

api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)
---

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 << ")";
   }