Update overflow check to handle negative numbers (#3396)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index d1112a9dce3fb11eec23fd444a475362848e2d6f..aed443197cef20e4f4605b33eb6e981f25369470 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2023,9 +2023,19 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
       << "base 2, 10, or 16";
 
   Integer val(s, base);
-  CVC4_API_CHECK(val.modByPow2(size) == val)
-      << "Overflow in bitvector construction (specified bitvector size " << size
-      << " too small to hold value " << s << ")";
+
+  if (val.strictlyNegative())
+  {
+    CVC4_API_CHECK(val >= -Integer("2", 10).pow(size - 1))
+        << "Overflow in bitvector construction (specified bitvector size "
+        << size << " too small to hold value " << s << ")";
+  }
+  else
+  {
+    CVC4_API_CHECK(val.modByPow2(size) == val)
+        << "Overflow in bitvector construction (specified bitvector size "
+        << size << " too small to hold value " << s << ")";
+  }
 
   return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
 }

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 9dd913ea26cf9f26436dfa23830f3099e6b0c887..41c4a86dd12c95ebefce9dd09d46bafc1ee71e92 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -286,12 +286,14 @@ void SolverBlack::testMkBitVector()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(8, "-127", 10));
   TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkBitVector(8, "-256", 10), CVC4ApiException&);
   TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
                    d_solver->mkBitVector("10", 10));
   TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
@@ -300,6 +302,8 @@ void SolverBlack::testMkBitVector()
                    "0bin01010101");
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(),
                    "0bin00001111");
+  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "-1", 10),
+                   d_solver->mkBitVector(8, "FF", 16));
 }
 
 void SolverBlack::testMkVar()