mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Better error message for mismatching sorts in substitutions in z3.substitute (#6093)

Browse source
This commit is contained in:
Dominic Steinhöfel 2022-06-13 22:46:30 +02:00 • committed by GitHub
parent 470bf27d1d
commit 46bc726391
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -8773,8 +8773,12 @@ def substitute(t, *m):
m = m1
if z3_debug():
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(
p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
_z3_assert(
all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) for p in m]),
"Z3 invalid substitution, expression pairs expected.")
_z3_assert(
all([p[0].sort().eq(p[1].sort()) for p in m]),
'Z3 invalid substitution, mismatching "from" and "to" sorts.')
num = len(m)
_from = (Ast * num)()
_to = (Ast * num)()