From ad39811dc0a9ebd11b62b59693142a5c9518d6f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:36:37 -0700 Subject: [PATCH] allow coercion from Boolean to Int/Real, fixes #78 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 7cda4bf83..c1bdf2713 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1229,13 +1229,13 @@ class BoolSortRef(SortRef): return val def subsort(self, other): - return isinstance(other, ArithSortRef) + return isinstance(other, ArithSortRef) def is_int(self): - return True + return True def is_bool(self): - return True + return True class BoolRef(ExprRef): @@ -1910,10 +1910,10 @@ class ArithSortRef(SortRef): return val if val_s.is_int() and self.is_real(): return ToReal(val) - if val_s.is_bool() and self.is_int(): - return If(val, 1, 0) - if val_s.is_bool() and self.is_real(): - return ToReal(If(val, 1, 0)) + if val_s.is_bool() and self.is_int(): + return If(val, 1, 0) + if val_s.is_bool() and self.is_real(): + return ToReal(If(val, 1, 0)) if __debug__: _z3_assert(False, "Z3 Integer/Real expression expected" ) else: