mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27: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 • committed by Nikolaj Bjorner
parent 92d684e942
commit 7e71ee9eb6
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

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