From 342a23cfcbff0dceedaecd6a1ca00e2ca88c8482 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 10 Oct 2014 13:00:41 +0100 Subject: [PATCH] C++ API bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/c++/z3++.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 20100d124..c35208d86 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1432,12 +1432,12 @@ namespace z3 { t1.check_error(); return tactic(t1.ctx(), r); } - friend tactic repeat(tactic const & t, unsigned max=UINT_MAX); + friend tactic repeat(tactic const & t, unsigned max); friend tactic with(tactic const & t, params const & p); friend tactic try_for(tactic const & t, unsigned ms); }; - inline tactic repeat(tactic const & t, unsigned max) { + inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) { Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); t.check_error(); return tactic(t.ctx(), r);