From: makaimann <makaim@stanford.edu>
Date: Fri, 18 Oct 2019 18:42:15 +0000 (-0700)
Subject: Update overflow check to handle negative numbers (#3396)
X-Git-Tag: cvc5-1.0.0~3878
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba175a951064250907494b7b5112f3882889df5e;p=cvc5.git

Update overflow check to handle negative numbers (#3396)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index d1112a9dc..aed443197 100644
--- 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 9dd913ea2..41c4a86dd 100644
--- 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()