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

Fix z3.py doctests to reflect recent changes in the substitute API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-25 18:58:13 -07:00
parent 4363c9f44f
commit 8ef2fe7ddb
1 changed files with 2 additions and 2 deletions
Show stats 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)