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

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-21 10:35:59 -07:00
parent 691788f449
commit b782ec35cc
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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):