diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f43ba83e5..9a340698a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -642,13 +642,7 @@ namespace z3 { */ friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; } - friend expr implies(expr const & a, expr const & b) { - check_context(a, b); - assert(a.is_bool() && b.is_bool()); - Z3_ast r = Z3_mk_implies(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } + friend expr implies(expr const & a, expr const & b); friend expr implies(expr const & a, bool b); friend expr implies(bool a, expr const & b); @@ -891,6 +885,13 @@ namespace z3 { }; + inline expr implies(expr const & a, expr const & b) { + check_context(a, b); + assert(a.is_bool() && b.is_bool()); + Z3_ast r = Z3_mk_implies(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }