diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 16 | ||||
| -rw-r--r-- | 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>(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() |