diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-10-15 13:45:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-15 20:45:03 +0000 |
commit | 66a3314ce9a92112c6a89667f343085aca565ae5 (patch) | |
tree | 9e11faafdb349fe1b0ace68c8573d4dc85c26a61 | |
parent | b4469530d2f6de599ddf7207a1914b88be49de5b (diff) |
Fix bad cast in the python API (#7359)
-rw-r--r-- | src/api/python/cvc5.pxi | 8 | ||||
-rw-r--r-- | test/python/unit/api/test_op.py | 3 |
2 files changed, 9 insertions, 2 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 0f6b54dc6..e45f0206e 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -907,9 +907,10 @@ cdef class Solver: - ``Op mkOp(Kind kind, const string& arg)`` - ``Op mkOp(Kind kind, uint32_t arg)`` - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)`` + - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind) """ cdef Op op = Op(self) - cdef vector[int] v + cdef vector[uint32_t] v if len(args) == 0: op.cop = self.csolver.mkOp(k.k) @@ -922,7 +923,10 @@ cdef class Solver: op.cop = self.csolver.mkOp(k.k, <int?> args[0]) elif isinstance(args[0], list): for a in args[0]: - v.push_back((<int?> a)) + if a < 0 or a >= 2 ** 31: + raise ValueError("Argument {} must fit in a uint32_t".format(a)) + + v.push_back((<uint32_t?> a)) op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v) else: raise ValueError("Unsupported signature" diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py index 07a57a5c6..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/python/unit/api/test_op.py @@ -86,6 +86,9 @@ def test_get_num_indices(solver): assert 2 == floatingpoint_to_fp_generic.getNumIndices() assert 2 == regexp_loop.getNumIndices() +def test_op_indices_list(solver): + with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): x = Op(solver) |