#4637

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 13, 2020 · 7d391d4 · 7d391d4
1 parent a892e47
commit 7d391d4
Showing 1 changed file with 9 additions and 6 deletions.
diff --git 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));
         }