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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-03-12 09:40:58 +01:00
parent 8bec1e25a8 7272d3f480
commit 1f4f4514bf
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/z3.py
View file

@ -7204,7 +7204,7 @@ def With(t, *args, **keys):
>>> t((x + 1)*(y + 2) == 0) >>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]] [[2*x + y + x*y == -2]]
""" """
ctx = keys.get('ctx', None) ctx = keys.pop('ctx', None)
t = _to_tactic(t, ctx) t = _to_tactic(t, ctx)
p = args2params(args, keys, t.ctx) p = args2params(args, keys, t.ctx)
return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx) return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)