From c6eb27513043ba47cc288abbd7fd3e4b05f51a3b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 04:45:35 +0000 Subject: [PATCH] Fix 9 critical assert statements and RatVal division by zero (Priority 1) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/python/test_critical_fixes.py | 210 ++++++++++++++++++++++++++ src/api/python/z3/z3.py | 53 ++++--- 2 files changed, 246 insertions(+), 17 deletions(-) create mode 100644 src/api/python/test_critical_fixes.py diff --git a/src/api/python/test_critical_fixes.py b/src/api/python/test_critical_fixes.py new file mode 100644 index 000000000..bd0366232 --- /dev/null +++ b/src/api/python/test_critical_fixes.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python +""" +Test suite for critical Python API bug fixes identified by a3-python analysis. + +These tests validate: +1. Bare assert statements replaced with proper exceptions (9 issues) +2. Division by zero check in RatVal +3. Bounds checking and negative index support in Goal.__getitem__ +""" + +import sys +import os + +# Add the z3 module to the path +sys.path.insert(0, os.path.join(os.path.dirname(__file__), 'z3')) + +import z3 + + +def test_ratval_division_by_zero(): + """Test that RatVal raises ValueError when denominator is zero.""" + print("Testing RatVal division by zero...") + try: + result = z3.RatVal(5, 0) + print(" FAILED: Expected ValueError but got result:", result) + return False + except ValueError as e: + if "Denominator cannot be zero" in str(e): + print(" PASSED: Correctly raised ValueError with proper message") + return True + else: + print(" FAILED: ValueError raised but with wrong message:", str(e)) + return False + except Exception as e: + print(" FAILED: Wrong exception type:", type(e).__name__, str(e)) + return False + + +def test_goal_getitem_negative_index(): + """Test that Goal.__getitem__ supports negative indexing.""" + print("Testing Goal.__getitem__ negative index...") + try: + g = z3.Goal() + x, y, z = z3.Ints('x y z') + g.add(x == 0, y > x, z < y) + + # Test negative indices + last = g[-1] + second_last = g[-2] + first = g[-3] + + # Verify they match positive indices + if str(last) == str(g[2]) and str(second_last) == str(g[1]) and str(first) == str(g[0]): + print(" PASSED: Negative indexing works correctly") + return True + else: + print(" FAILED: Negative indexing returned wrong values") + return False + except Exception as e: + print(" FAILED: Exception raised:", type(e).__name__, str(e)) + return False + + +def test_goal_getitem_bounds(): + """Test that Goal.__getitem__ raises IndexError for out of bounds access.""" + print("Testing Goal.__getitem__ bounds checking...") + try: + g = z3.Goal() + x, y = z3.Ints('x y') + g.add(x == 0, y > x) + + # Test out of bounds positive index + try: + item = g[10] + print(" FAILED: Expected IndexError for positive out of bounds") + return False + except IndexError: + pass # Expected + + # Test out of bounds negative index + try: + item = g[-10] + print(" FAILED: Expected IndexError for negative out of bounds") + return False + except IndexError: + pass # Expected + + print(" PASSED: Bounds checking works correctly") + return True + except Exception as e: + print(" FAILED: Unexpected exception:", type(e).__name__, str(e)) + return False + + +def test_user_propagate_double_registration(): + """Test that UserPropagateBase raises Z3Exception on double registration.""" + print("Testing UserPropagateBase double registration...") + try: + # Create a minimal UserPropagateBase subclass + class TestPropagator(z3.UserPropagateBase): + def push(self): + pass + def pop(self, num_scopes): + pass + def fresh(self, new_ctx): + return TestPropagator() + + prop = TestPropagator() + + # Test double registration of fixed callback + def fixed_callback(x, v): + pass + + prop.add_fixed(fixed_callback) + try: + prop.add_fixed(fixed_callback) # Second registration + print(" FAILED: Expected Z3Exception for double fixed registration") + return False + except z3.Z3Exception as e: + if "already registered" in str(e): + print(" PASSED: Correctly raised Z3Exception for double registration") + return True + else: + print(" FAILED: Z3Exception raised but with wrong message:", str(e)) + return False + except Exception as e: + print(" FAILED: Unexpected exception:", type(e).__name__, str(e)) + return False + + +def test_ratval_valid_cases(): + """Test that RatVal still works for valid inputs.""" + print("Testing RatVal valid cases...") + try: + # Test valid rational number creation + r1 = z3.RatVal(3, 5) + r2 = z3.RatVal(1, 2) + r3 = z3.RatVal(-7, 3) + + # Verify they are created correctly + if r1 is not None and r2 is not None and r3 is not None: + print(" PASSED: Valid RatVal cases work correctly") + return True + else: + print(" FAILED: Valid RatVal returned None") + return False + except Exception as e: + print(" FAILED: Exception raised for valid case:", type(e).__name__, str(e)) + return False + + +def test_goal_getitem_valid_cases(): + """Test that Goal.__getitem__ still works for valid positive indices.""" + print("Testing Goal.__getitem__ valid positive indices...") + try: + g = z3.Goal() + x, y, z = z3.Ints('x y z') + g.add(x == 0, y > x, z < y) + + # Test valid positive indices + first = g[0] + second = g[1] + third = g[2] + + if first is not None and second is not None and third is not None: + print(" PASSED: Valid positive indexing works correctly") + return True + else: + print(" FAILED: Valid indexing returned None") + return False + except Exception as e: + print(" FAILED: Exception raised for valid case:", type(e).__name__, str(e)) + return False + + +def main(): + """Run all tests and report results.""" + print("=" * 60) + print("Running Critical Python API Bug Fix Tests") + print("=" * 60) + print() + + tests = [ + test_ratval_division_by_zero, + test_ratval_valid_cases, + test_goal_getitem_negative_index, + test_goal_getitem_bounds, + test_goal_getitem_valid_cases, + test_user_propagate_double_registration, + ] + + passed = 0 + failed = 0 + + for test in tests: + if test(): + passed += 1 + else: + failed += 1 + print() + + print("=" * 60) + print(f"Results: {passed} passed, {failed} failed") + print("=" * 60) + + return 0 if failed == 0 else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 50b4fa836..422f28d15 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -870,7 +870,7 @@ class FuncDeclRef(AstRef): elif k == Z3_PARAMETER_ZSTRING: result[i] = "internal string" else: - assert(False) + raise Z3Exception("Unexpected parameter kind") return result def __call__(self, *args): @@ -3374,6 +3374,8 @@ def RatVal(a, b, ctx=None): if z3_debug(): _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") + if b == 0: + raise ValueError("Denominator cannot be zero") return simplify(RealVal(a, ctx) / RealVal(b, ctx)) @@ -5896,7 +5898,9 @@ class Goal(Z3PPObject): >>> g[1] y > x """ - if arg >= len(self): + if arg < 0: + arg += len(self) + if arg < 0 or arg >= len(self): raise IndexError return self.get(arg) @@ -12014,50 +12018,64 @@ class UserPropagateBase: return self.ctx().ref() def add_fixed(self, fixed): - assert not self.fixed - assert not self._ctx + if self.fixed: + raise Z3Exception("Fixed callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed) self.fixed = fixed def add_created(self, created): - assert not self.created - assert not self._ctx + if self.created: + raise Z3Exception("Created callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created) self.created = created def add_final(self, final): - assert not self.final - assert not self._ctx + if self.final: + raise Z3Exception("Final callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final) self.final = final def add_eq(self, eq): - assert not self.eq - assert not self._ctx + if self.eq: + raise Z3Exception("Eq callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq) self.eq = eq def add_diseq(self, diseq): - assert not self.diseq - assert not self._ctx + if self.diseq: + raise Z3Exception("Diseq callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq) self.diseq = diseq def add_decide(self, decide): - assert not self.decide - assert not self._ctx + if self.decide: + raise Z3Exception("Decide callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide) self.decide = decide def add_on_binding(self, binding): - assert not self.binding - assert not self._ctx + if self.binding: + raise Z3Exception("Binding callback already registered") + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding) self.binding = binding @@ -12072,7 +12090,8 @@ class UserPropagateBase: raise Z3Exception("fresh needs to be overwritten") def add(self, e): - assert not self._ctx + if self._ctx: + raise Z3Exception("Context already initialized") if self.solver: Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast) else: