diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d9d0ad3f68a..020a7688be3 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1458,7 +1458,7 @@ cdef class Solver: "Invalid second argument to mkBitVector '{}', " "expected integer value".format(size)) term.cterm = self.csolver.mkBitVector( - size, val) + size, str(val).encode(), 10) elif len(args) == 2: val = args[0] base = args[1] diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 94ebf95b1eb..8b69549f6a9 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -325,6 +325,7 @@ def test_mk_tuple_sort(solver): def test_mk_bit_vector(solver): solver.mkBitVector(8, 2) solver.mkBitVector(32, 2) + solver.mkBitVector(64, 2**33) solver.mkBitVector(4, "1010", 2) solver.mkBitVector(8, "0101", 2)