From 46bc726391a6f154b39262e66c9e22821ea335a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominic=20Steinh=C3=B6fel?= Date: Mon, 13 Jun 2022 22:46:30 +0200 Subject: [PATCH] Better error message for mismatching sorts in substitutions in z3.substitute (#6093) --- src/api/python/z3/z3.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index dbd623a2f..b2e7e250c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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)()