From cd41b21fa2e46ffe3c51f2089931dec20ddbdabc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Jan 2025 11:59:59 -0800
Subject: [PATCH] fix #7501

---
 src/api/python/z3/z3.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 5d8dc6649..0fbe2a5c3 100644
--- 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)