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

Fix #3439, print type of value in exception msg (#3498)

Browse source
This commit is contained in:
rashchedrin 2020-03-23 22:36:36 +03:00 • committed by GitHub
parent 519c0d5f11
commit b34f72dd00
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1405,7 +1405,7 @@ class BoolSortRef(SortRef):
return BoolVal(val, self.ctx)
if z3_debug():
if not is_expr(val):
_z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
_z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s of type %s" % (val, type(val)))
if not self.eq(val.sort()):
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
return val