mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

Improve documentation for RatVal division by zero handling

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-18 00:44:40 +00:00
parent ae328dc006
commit 064122a123
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/python/z3/z3.py
View file

@ -3376,6 +3376,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
@ -3385,8 +3388,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))