From 919e0a5ea2f2bef4fe8ab9880e91dd52a7fc2bd1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Sep 2014 14:56:59 +0100 Subject: [PATCH] Z3Py: fix bug in substitute() with a list of on variable e.g. print substitute(Int('x'), [(Int('x'), Int('y'))]) Signed-off-by: Nuno Lopes --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 50d29a790..d46d40ab2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -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.")