From 61385c8489b7fda11b518a67fe308ea3cfe28c3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Nov 2013 09:54:37 -0800 Subject: [PATCH] a.ctx -> self.ctx, thanks gario Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- src/interp/iz3translate_direct.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 22ec30ad2..959566619 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6424,7 +6424,7 @@ class Tactic: _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected") goal = _to_goal(goal) if len(arguments) > 0 or len(keywords) > 0: - p = args2params(arguments, keywords, a.ctx) + p = args2params(arguments, keywords, self.ctx) return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx) else: return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx) diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 44c907d1d..853ecbe86 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -19,6 +19,7 @@ Revision History: --*/ + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h"