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"