From 5e6a47e2d37b1e348925d8455b06808631c942e3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 26 Sep 2013 11:35:08 +0100 Subject: [PATCH] Example fixed (substitute does not include a rewriter call anymore). Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index aaad24256..22ec30ad2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6932,10 +6932,10 @@ def substitute(t, *m): >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) - 2 + y + y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) - 2 + 1 + 1 """ if isinstance(m, tuple): m1 = _get_args(m)