mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Fix #6503

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-25 17:28:57 -08:00
parent fe8034731d
commit 8efaaaf249
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1559,13 +1559,15 @@ class BoolRef(ExprRef):
def __mul__(self, other): def __mul__(self, other):
"""Create the Z3 expression `self * other`. """Create the Z3 expression `self * other`.
""" """
if other == 1: if isinstance(other, int) and other == 1:
return self return self
if other == 0: if isinstance(other, int) and other == 0:
return 0 return
if isinstance(other, BoolRef):
other = If(other, 1, 0)
return If(self, other, 0) return If(self, other, 0)
def is_bool(a): def is_bool(a):
"""Return `True` if `a` is a Z3 Boolean expression. """Return `True` if `a` is a Z3 Boolean expression.