mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Example fixed (substitute does not include a rewriter call anymore).

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-09-26 11:35:08 +01:00
parent 07a4fb4381
commit 5e6a47e2d3
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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)