mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Fix BOUNDS and ASSERT_FAIL issues in Python API

Browse source 
- 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>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-12 03:05:06 +00:00
parent f7e5cf7e0c
commit 27169eb0f7
2 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/python/z3/z3.py
View file

@ -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)

12
src/api/python/z3/z3num.py
View file

@ -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):