From: NicolaasWeideman Date: Mon, 5 Apr 2021 16:56:10 +0000 (-0700) Subject: python: Fix type casting in mkBitVector (#6261) X-Git-Tag: cvc5-1.0.0~1972 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27ca0f4abe8da4445d07daa5b9bf4ed6f72ad1d6;p=cvc5.git python: Fix type casting in mkBitVector (#6261) Fixes #6260. Signed-off-by: Nicolaas --- 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( size_or_str) + term.cterm = self.csolver.mkBitVector( size_or_str) else: - term.cterm = self.csolver.mkBitVector( size_or_str, - val) + term.cterm = self.csolver.mkBitVector( size_or_str, + str(val).encode(), + 10) elif isinstance(size_or_str, str): # handle default value if val is None: @@ -747,7 +748,7 @@ cdef class Solver: size_or_str.encode()) else: term.cterm = self.csolver.mkBitVector( - size_or_str.encode(), val) + size_or_str.encode(), val) else: raise ValueError("Unexpected inputs {} to" " mkBitVector".format((size_or_str, val)))