From 860bcd4483e44dbd638c540ddee3da8a76a38440 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 04:42:49 +0000 Subject: [PATCH 1/6] Initial plan From 629d999fa22502fd84f5d9b0d8b9176a3a612e43 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 2/6] 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: From 69bf729a22e34e494775dce57a3e900671f84bb9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 05:01:41 +0000 Subject: [PATCH 3/6] Add comprehensive tests for Python API bug fixes Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/python/test_critical_fixes.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/python/test_critical_fixes.py b/src/api/python/test_critical_fixes.py index bd0366232..80258e35c 100644 --- a/src/api/python/test_critical_fixes.py +++ b/src/api/python/test_critical_fixes.py @@ -11,10 +11,8 @@ These tests validate: 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 +# Make sure we can import z3 from the build directory +from z3 import z3 def test_ratval_division_by_zero(): @@ -98,6 +96,9 @@ def test_user_propagate_double_registration(): try: # Create a minimal UserPropagateBase subclass class TestPropagator(z3.UserPropagateBase): + def __init__(self, s=None): + super().__init__(s, ctx=z3.Context() if s is None else None) + def push(self): pass def pop(self, num_scopes): From a8f32ed291d22e0f1e51c175aab1d627556896c6 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 05:03:07 +0000 Subject: [PATCH 4/6] Fix error message capitalization for Python conventions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/python/z3/z3.py | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 422f28d15..cbbb04289 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -12019,63 +12019,63 @@ class UserPropagateBase: def add_fixed(self, fixed): if self.fixed: - raise Z3Exception("Fixed callback already registered") + raise Z3Exception("fixed callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.created: - raise Z3Exception("Created callback already registered") + raise Z3Exception("created callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.final: - raise Z3Exception("Final callback already registered") + raise Z3Exception("final callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.eq: - raise Z3Exception("Eq callback already registered") + raise Z3Exception("eq callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.diseq: - raise Z3Exception("Diseq callback already registered") + raise Z3Exception("diseq callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.decide: - raise Z3Exception("Decide callback already registered") + raise Z3Exception("decide callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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): if self.binding: - raise Z3Exception("Binding callback already registered") + raise Z3Exception("binding callback already registered") if self._ctx: - raise Z3Exception("Context already initialized") + 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 @@ -12091,7 +12091,7 @@ class UserPropagateBase: def add(self, e): if self._ctx: - raise Z3Exception("Context already initialized") + raise Z3Exception("context already initialized") if self.solver: Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast) else: From dcbafa9442bc51b8c28fd6a86d7ec78b87bfc218 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Feb 2026 07:07:15 -0800 Subject: [PATCH 5/6] Delete src/api/python/test_critical_fixes.py --- src/api/python/test_critical_fixes.py | 211 -------------------------- 1 file changed, 211 deletions(-) delete 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 deleted file mode 100644 index 80258e35c..000000000 --- a/src/api/python/test_critical_fixes.py +++ /dev/null @@ -1,211 +0,0 @@ -#!/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 - -# Make sure we can import z3 from the build directory -from 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 __init__(self, s=None): - super().__init__(s, ctx=z3.Context() if s is None else None) - - 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()) From 8077e3d0318464333d961c58c565fb93d3af1edd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Feb 2026 07:10:00 -0800 Subject: [PATCH 6/6] Modify behavior for division by zero Allow division by zero in z3 expressions without raising an error. --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index cbbb04289..132edecde 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3375,7 +3375,7 @@ def RatVal(a, b, ctx=None): _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") + pass # division by 0 is legal in z3 expressions. return simplify(RealVal(a, ctx) / RealVal(b, ctx))