python: Fix type casting in mkBitVector (#6261)

Fixes #6260.

Signed-off-by: Nicolaas <nweidema@usc.edu>

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 947132a896929ed532e55ae11ee94f28cb49f755..8bcd618cfe526a20bc417523a61310a27b128a09 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -187,6 +187,7 @@ cdef extern from "api/cvc4cpp.h" namespace "cvc5::api":
         Term mkBitVector(uint32_t size, uint64_t val) except +
         Term mkBitVector(const string& s) except +
         Term mkBitVector(const string& s, uint32_t base) except +
+        Term mkBitVector(uint32_t size, string& s, uint32_t base) except +
         Term mkConstArray(Sort sort, Term val) except +
         Term mkPosInf(uint32_t exp, uint32_t sig) except +
         Term mkNegInf(uint32_t exp, uint32_t sig) except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index c44fc08af73d377950e6f033f6d6680a489a64fc..a08e50931244164a13f1781c640172a36fa7bc94 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -736,10 +736,11 @@ cdef class Solver:
         cdef Term term = Term(self)
         if isinstance(size_or_str, int):
             if val is None:
-                term.cterm = self.csolver.mkBitVector(<int> size_or_str)
+                term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str)
             else:
-                term.cterm = self.csolver.mkBitVector(<int> size_or_str,
-                                                      <int> val)
+                term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str,
+                                                      <const string &> str(val).encode(),
+                                                      10)
         elif isinstance(size_or_str, str):
             # handle default value
             if val is None:
@@ -747,7 +748,7 @@ cdef class Solver:
                     <const string &> size_or_str.encode())
             else:
                 term.cterm = self.csolver.mkBitVector(
-                    <const string &> size_or_str.encode(), <int> val)
+                    <const string &> size_or_str.encode(), <uint32_t> val)
         else:
             raise ValueError("Unexpected inputs {} to"
                              " mkBitVector".format((size_or_str, val)))