diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 16 |
1 files changed, 13 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)); } |