diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 10aab65e792..d5312b47199 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2848,20 +2848,23 @@ namespace z3 { void add(expr_vector const& es) { for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it); } - handle add(expr const& e, unsigned weight) { - assert(e.is_bool()); - auto str = std::to_string(weight); - return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0)); - } void add(expr const& e, expr const& t) { assert(e.is_bool()); Z3_optimize_assert_and_track(ctx(), m_opt, e, t); } - handle add(expr const& e, char const* weight) { + handle add_soft(expr const& e, unsigned weight) { + assert(e.is_bool()); + auto str = std::to_string(weight); + return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0)); + } + handle add_soft(expr const& e, char const* weight) { assert(e.is_bool()); return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); } + handle add(expr const& e, unsigned weight) { + return add_soft(e, weight); + } handle maximize(expr const& e) { return handle(Z3_optimize_maximize(ctx(), m_opt, e)); }