fix #7501

Z3Prover · Jan 5, 2025 · cd41b21 · cd41b21
1 parent f6e3c5a
commit cd41b21
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
@@ -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)