mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Z3Py: fix bug in substitute() with a list of on variable

Browse source 
e.g. print substitute(Int('x'), [(Int('x'), Int('y'))])

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-09-16 14:56:59 +01:00
parent dd62ca5eb3
commit 919e0a5ea2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6960,7 +6960,7 @@ def substitute(t, *m):
if isinstance(m, tuple):
m1 = _get_args(m)
if isinstance(m1, list):
m = _get_args(m1)
m = m1
if __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.")