From 27ca0f4abe8da4445d07daa5b9bf4ed6f72ad1d6 Mon Sep 17 00:00:00 2001
From: NicolaasWeideman <nhweideman@gmail.com>
Date: Mon, 5 Apr 2021 09:56:10 -0700
Subject: [PATCH] python: Fix type casting in mkBitVector (#6261)

Fixes #6260.

Signed-off-by: Nicolaas <nweidema@usc.edu>
---
 src/api/python/cvc4.pxd | 1 +
 src/api/python/cvc4.pxi | 9 +++++----
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 947132a89..8bcd618cf 100644
--- 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 c44fc08af..a08e50931 100644
--- 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)))
-- 
2.30.2