Fix bad cast in the python API (#7359)

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 0f6b54dc6a0f20e2cd5e86fda60c931dfa44c676..e45f0206ea49d6a6041c41cf1eaf591f0119dc89 100644 (file)
--- 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 07a57a5c6c8ff0b012fb0114d5551d19fc32633c..5126a481dba3e99ec21fd1224fee0ef6461a2d3e 100644 (file)
--- 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)