mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-02 16:43:45 +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 9a46074b37
commit 6743d42ea4
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] >>> A[0]
x x
""" """
if i >= self.__len__(): if i < 0:
i += self.__len__()
if i < 0 or i >= self.__len__():
raise IndexError raise IndexError
Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
@ -6827,7 +6829,9 @@ class ModelRef(Z3PPObject):
f -> [else -> 0] f -> [else -> 0]
""" """
if _is_int(idx): if _is_int(idx):
if idx >= len(self): if idx < 0:
idx += len(self)
if idx < 0 or idx >= len(self):
raise IndexError raise IndexError
num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
if (idx < num_consts): if (idx < num_consts):
@ -8434,7 +8438,9 @@ class ApplyResult(Z3PPObject):
>>> r[1] >>> r[1]
[a == 1, Or(b == 0, b == 1), a > b] [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 raise IndexError
return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx) 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() >>> Numeral("2/3").denominator()
3 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) return Numeral(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
def numerator(self): def numerator(self):
@ -151,7 +152,8 @@ class Numeral:
>>> Numeral("2/3").numerator() >>> Numeral("2/3").numerator()
2 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) return Numeral(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
def is_irrational(self): def is_irrational(self):
@ -170,7 +172,8 @@ class Numeral:
""" Return a numeral (that is an integer) as a Python long. """ 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: if sys.version_info.major >= 3:
return int(Z3_get_numeral_string(self.ctx_ref(), self.as_ast())) return int(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
else: else:
@ -181,7 +184,8 @@ class Numeral:
>>> Numeral("1/5").as_fraction() >>> Numeral("1/5").as_fraction()
Fraction(1, 5) 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()) return Fraction(self.numerator().as_long(), self.denominator().as_long())
def approx(self, precision=10): def approx(self, precision=10):