From b782ec35ccaf59cac1294b7bb2f7714dd9854ac2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 May 2017 10:35:59 -0700 Subject: [PATCH] avoid print statements from assertions when the assertion does not trigger. Stackoverflow question http://stackoverflow.com/questions/44094927/creating-formula-taking-too-much-time-in-z3py Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b4cdf834b..84a80ddf7 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1300,8 +1300,10 @@ class BoolSortRef(SortRef): if isinstance(val, bool): return BoolVal(val, self.ctx) if __debug__: - _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) - _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") + if not is_expr(val): + _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) + if not self.eq(val.sort()): + _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") return val def subsort(self, other):