From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 15 Oct 2021 20:45:03 +0000 (-0700)
Subject: Fix bad cast in the python API (#7359)
X-Git-Tag: cvc5-1.0.0~1059
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=66a3314ce9a92112c6a89667f343085aca565ae5;p=cvc5.git

Fix bad cast in the python API (#7359)
---

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)