From dcbafa9442bc51b8c28fd6a86d7ec78b87bfc218 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Feb 2026 07:07:15 -0800 Subject: [PATCH] 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())