From 8efaaaf24982ce810b8ea85fdf74eedc3dea29ad Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Dec 2022 17:28:57 -0800
Subject: [PATCH] Fix #6503
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/python/z3/z3.py | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index e829fdafb..ca3486ac5 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1559,13 +1559,15 @@ class BoolRef(ExprRef):
def __mul__(self, other):
"""Create the Z3 expression `self * other`.
"""
- if other == 1:
+ if isinstance(other, int) and other == 1:
return self
- if other == 0:
- return 0
+ if isinstance(other, int) and other == 0:
+ return
+ if isinstance(other, BoolRef):
+ other = If(other, 1, 0)
return If(self, other, 0)
-
+
def is_bool(a):
"""Return `True` if `a` is a Z3 Boolean expression.