3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

z3py: With tactical should not try to use context as a parameter

This commit is contained in:
James Bornholt 2017-03-11 16:03:09 -08:00
parent 228111511c
commit 559c5e5ae6

View file

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