mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Modify behavior for division by zero

Browse source 
Allow division by zero in z3 expressions without raising an error.
This commit is contained in:
Nikolaj Bjorner 2026-02-12 07:10:00 -08:00 • committed by GitHub
parent dcbafa9442
commit 8077e3d031
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3375,7 +3375,7 @@ def RatVal(a, b, ctx=None):
_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")
pass # division by 0 is legal in z3 expressions.
return simplify(RealVal(a, ctx) / RealVal(b, ctx))