From 167b88a61bca69ed7bdd3b9d0aa40de059b6cb5a Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 12 Sep 2023 13:43:27 -0700
Subject: [PATCH] python: Allow Python integers for mkBitVector(). (#10021)

Fixes #10020.
---
 src/api/python/cvc5.pxi             | 2 +-
 test/unit/api/python/test_solver.py | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

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(
-                <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
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)