From 7e71ee9eb665c3d67e826d02ce8e08070ad94d82 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 18 Feb 2026 00:44:40 +0000
Subject: [PATCH] Improve documentation for RatVal division by zero handling

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/python/z3/z3.py | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 744396afe..8a743dcf0 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -3382,6 +3382,9 @@ def RatVal(a, b, ctx=None):
     """Return a Z3 rational a/b.
 
     If `ctx=None`, then the global context is used.
+    
+    Note: Division by zero (b == 0) is allowed in Z3 symbolic expressions.
+    Z3 can reason about such expressions symbolically.
 
     >>> RatVal(3,5)
     3/5
@@ -3391,8 +3394,7 @@ 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:
-        pass # division by 0 is legal in z3 expressions.
+    # Division by 0 is intentionally allowed - Z3 handles it symbolically
     return simplify(RealVal(a, ctx) / RealVal(b, ctx))