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

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

src/api/python/z3/z3.py

@@ -872,7 +872,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):
@@ -3380,6 +3380,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))
 
 
@@ -6133,7 +6135,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)
 
@@ -12267,50 +12271,64 @@ class UserPropagateBase:
         return self.ctx().ref()
 
     def add_fixed(self, fixed):
-        assert not self.fixed
+        if self.fixed:
-        assert not self._ctx
+            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
+        if self.created:
-        assert not self._ctx
+            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
+        if self.final:
-        assert not self._ctx
+            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
+        if self.eq:
-        assert not self._ctx
+            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
+        if self.diseq:
-        assert not self._ctx
+            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
+        if self.decide:
-        assert not self._ctx
+            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
+        if self.binding:
-        assert not self._ctx
+            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
@@ -12325,7 +12343,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: