From ba175a951064250907494b7b5112f3882889df5e Mon Sep 17 00:00:00 2001 From: makaimann Date: Fri, 18 Oct 2019 11:42:15 -0700 Subject: [PATCH] Update overflow check to handle negative numbers (#3396) --- src/api/cvc4cpp.cpp | 16 +++++++++++++--- test/unit/api/solver_black.h | 4 ++++ 2 files changed, 17 insertions(+), 3 deletions(-) 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(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() -- 2.30.2