diff options
| author | NicolaasWeideman <nhweideman@gmail.com> | 2021-04-05 09:56:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 09:56:10 -0700 |
| commit | 27ca0f4abe8da4445d07daa5b9bf4ed6f72ad1d6 (patch) | |
| tree | 25b11072747ee07de14c1b683b5e32d971dfcab9 | |
| parent | 73bc16fbba65ca8d8cdc9dd6674ae9280658ee9a (diff) | |
python: Fix type casting in mkBitVector (#6261)
Fixes #6260.
Signed-off-by: Nicolaas <nweidema@usc.edu>
| -rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
| -rw-r--r-- | 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))) |