From 27169eb0f756e7f320928fa97eaa7e21076b9427 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Feb 2026 03:05:06 +0000
Subject: [PATCH] Fix BOUNDS and ASSERT_FAIL issues in Python API

- Add negative index support to AstVector.__setitem__, ModelRef.__getitem__, ApplyResult.__getitem__
- Replace bare assertions with proper Z3Exception in z3num.Numeral methods
- All changes tested and validated with comprehensive test suite

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/python/z3/z3.py    | 12 +++++++++---
 src/api/python/z3/z3num.py | 12 ++++++++----
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 838a4c7ff..50b4fa836 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6138,7 +6138,9 @@ class AstVector(Z3PPObject):
         >>> A[0]
         x
         """
-        if i >= self.__len__():
+        if i < 0:
+            i += self.__len__()
+        if i < 0 or i >= self.__len__():
             raise IndexError
         Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
 
@@ -6827,7 +6829,9 @@ class ModelRef(Z3PPObject):
         f -> [else -> 0]
         """
         if _is_int(idx):
-            if idx >= len(self):
+            if idx < 0:
+                idx += len(self)
+            if idx < 0 or idx >= len(self):
                 raise IndexError
             num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
             if (idx < num_consts):
@@ -8434,7 +8438,9 @@ class ApplyResult(Z3PPObject):
         >>> r[1]
         [a == 1, Or(b == 0, b == 1), a > b]
         """
-        if idx >= len(self):
+        if idx < 0:
+            idx += len(self)
+        if idx < 0 or idx >= len(self):
             raise IndexError
         return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
 
diff --git a/src/api/python/z3/z3num.py b/src/api/python/z3/z3num.py
index 09415d474..dff0e8e18 100644
--- a/src/api/python/z3/z3num.py
+++ b/src/api/python/z3/z3num.py
@@ -142,7 +142,8 @@ class Numeral:
         >>> Numeral("2/3").denominator()
         3
         """
-        assert(self.is_rational())
+        if not self.is_rational():
+            raise Z3Exception("denominator() requires a rational numeral")
         return Numeral(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
 
     def numerator(self):
@@ -151,7 +152,8 @@ class Numeral:
         >>> Numeral("2/3").numerator()
         2
         """
-        assert(self.is_rational())
+        if not self.is_rational():
+            raise Z3Exception("numerator() requires a rational numeral")
         return Numeral(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
 
     def is_irrational(self):
@@ -170,7 +172,8 @@ class Numeral:
         """ Return a numeral (that is an integer) as a Python long.
 
         """
-        assert(self.is_integer())
+        if not self.is_integer():
+            raise Z3Exception("as_long() requires an integer numeral")
         if sys.version_info.major >= 3:
             return int(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
         else:
@@ -181,7 +184,8 @@ class Numeral:
         >>> Numeral("1/5").as_fraction()
         Fraction(1, 5)
         """
-        assert(self.is_rational())
+        if not self.is_rational():
+            raise Z3Exception("as_fraction() requires a rational numeral")
         return Fraction(self.numerator().as_long(), self.denominator().as_long())
 
     def approx(self, precision=10):