python: Allow Python integers for mkBitVector(). (cvc5#10021)

Fixes cvc5#10020.
ajreynol · Sep 12, 2023 · 167b88a · 167b88a
1 parent 1a2b2d7
commit 167b88a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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(
-                <uint32_t> size, <uint32_t> val)
+                <uint32_t> size, <const string&> 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
@@ -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)