From 559c5e5ae63e13a0fbb18b7b6589d8a0b111debe Mon Sep 17 00:00:00 2001 From: James Bornholt Date: Sat, 11 Mar 2017 16:03:09 -0800 Subject: [PATCH] z3py: With tactical should not try to use context as a parameter --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a0aba95d6..16d7fbb5f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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)