mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix #7501

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-05 11:59:59 -08:00
parent f6e3c5ae79
commit cd41b21fa2
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3437,9 +3437,11 @@ def ToReal(a):
>>> n.sort()
Real
"""
ctx = a.ctx
if isinstance(a, BoolRef):
return If(a, RealVal(1, ctx), RealVal(0, ctx))
if z3_debug():
_z3_assert(a.is_int(), "Z3 integer expression expected.")
ctx = a.ctx
return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)