diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index b1640506e..7236a7682 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -72,32 +72,32 @@ extern "C" {
         Z3_CATCH;
     }
 
-    void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) {
+    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) {
         Z3_TRY;
         LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
         RESET_ERROR_CODE();
-        CHECK_FORMULA(a,);        
+        CHECK_FORMULA(a,0);        
         rational w("weight");
-        to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
-        Z3_CATCH;
+        return to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
+        Z3_CATCH_RETURN(0);
     }
 
-    void Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) {
+    unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_optimize_maximize(c, o, t);
         RESET_ERROR_CODE();
-        CHECK_VALID_AST(t,);        
-        to_optimize_ref(o).add_objective(to_app(t), true);
-        Z3_CATCH;
+        CHECK_VALID_AST(t,0);        
+        return to_optimize_ref(o).add_objective(to_app(t), true);
+        Z3_CATCH_RETURN(0);
     }
 
-    void Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) {
+    unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_optimize_minimize(c, o, t);
         RESET_ERROR_CODE();
-        CHECK_VALID_AST(t,);        
-        to_optimize_ref(o).add_objective(to_app(t), false);
-        Z3_CATCH;
+        CHECK_VALID_AST(t,0);        
+        return to_optimize_ref(o).add_objective(to_app(t), false);
+        Z3_CATCH_RETURN(0);
     }
 
     Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 4526ead88..925773fa5 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -18,6 +18,7 @@ Notes:
 --*/
 
 using System;
+using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Z3
@@ -28,6 +29,7 @@ namespace Microsoft.Z3
     [ContractVerification(true)]
     public class Optimize : Z3Object
     {
+        HashSet<uint> indices;
 
 #if false
         /// <summary>
@@ -64,6 +66,26 @@ namespace Microsoft.Z3
             get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
         }
 
+        /// <summary>
+        /// Get the number of objectives.
+        /// </summary>
+        public uint ObjectiveCount
+        {
+            get { return (uint)indices.Count; }
+        }
+
+        /// <summary>
+        /// Get all indices of objectives.
+        /// </summary>
+        public uint[] Objectives
+        {
+            get 
+            {
+                var objectives = new uint[indices.Count];
+                indices.CopyTo(objectives, 0);
+                return objectives;
+            }
+        }
 
         /// <summary>
         /// Assert a constraint (or multiple) into the optimize solver.
@@ -91,21 +113,28 @@ namespace Microsoft.Z3
         /// <summary>
         /// Assert soft constraint
         /// </summary>        
-        public void AssertSoft(BoolExpr constraint, uint weight, string group)
+        /// <remarks>
+        /// Return an objective which associates with the group of constraints.
+        /// </remarks>
+        public uint AssertSoft(BoolExpr constraint, uint weight, string group)
         {
             Context.CheckContextMatch(constraint);
-	    Symbol s = Context.MkSymbol(group);            
-	    Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
+	        Symbol s = Context.MkSymbol(group);            
+	        uint index = Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
+            indices.Add(index);
+            return index;
         }
-
 	
-	public Status Check() {
-	    Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
+	    public Status Check() {
+	        Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
             switch (r)
             {
-                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
-                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
-                default: return Status.UNKNOWN;
+                case Z3_lbool.Z3_L_TRUE: 
+                    return Status.SATISFIABLE;
+                case Z3_lbool.Z3_L_FALSE: 
+                    return Status.UNSATISFIABLE;
+                default: 
+                    return Status.UNKNOWN;
             }         
         }
 
@@ -127,22 +156,31 @@ namespace Microsoft.Z3
                     return new Model(Context, x);
             }
         }
+        	
+	    public uint MkMaximize(ArithExpr e) 
+        {
+	        uint index = Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
+            indices.Add(index);
+            return index;
+	    }
 
-	
-	public void Maximize(ArithExpr e) {
-	    Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
-	}
+        public uint MkMinimize(ArithExpr e)
+        {
+	        uint index = Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
+            indices.Add(index);
+            return index;
+	    }
 
-	public void Minimize(ArithExpr e) {
-	    Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
-	}
-
-	public ArithExpr GetLower(uint index) {
-	    return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
+	    public ArithExpr GetLower(uint index) 
+        {
+            Contract.Requires(indices.Contains(index));
+	        return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
         }
 
-	public ArithExpr GetUpper(uint index) {
-	    return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
+        public ArithExpr GetUpper(uint index)
+        {
+            Contract.Requires(indices.Contains(index));
+	        return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
         #region Internal
@@ -150,11 +188,13 @@ namespace Microsoft.Z3
             : base(ctx, obj)
         {
             Contract.Requires(ctx != null);
+            indices = new HashSet<uint>();
         }
         internal Optimize(Context ctx)
             : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
         {
             Contract.Requires(ctx != null);
+            indices = new HashSet<uint>();
         }
 
         internal class DecRefQueue : IDecRefQueue
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index a52ad6106..9350eb529 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5987,9 +5987,9 @@ END_MLAPI_EXCLUDE
        \param weight - a positive weight, penalty for violating soft constraint
        \param id - optional identifier to group soft constraints
 
-       def_API('Z3_optimize_assert_soft', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
+       def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
     */
-    void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
+    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
 
 
     /**
@@ -5997,9 +5997,9 @@ END_MLAPI_EXCLUDE
        \param c - context
        \param o - optimization context
        \param a - arithmetical term       
-       def_API('Z3_optimize_maximize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+       def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
-    void Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t);
+    unsigned Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t);
 
     /**
        \brief Add a minimiztion constraint.
@@ -6007,9 +6007,9 @@ END_MLAPI_EXCLUDE
        \param o - optimization context
        \param a - arithmetical term   
     
-       def_API('Z3_optimize_minimize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+       def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
-    void Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t);
+    unsigned Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t);
 
     /**
        \brief Check consistency and produce optimal values.
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 49f15f420..78495c928 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -42,21 +42,25 @@ namespace opt {
         }
     }
 
-    void context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { 
+    unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { 
         maxsmt* ms;
         if (!m_maxsmts.find(id, ms)) {
             ms = alloc(maxsmt, m);
             m_maxsmts.insert(id, ms);
             m_objectives.push_back(objective(m, id));
+            m_indices.insert(id, m_objectives.size() - 1);
         }
-        ms->add(f, w);
+        ms->add(f, w);        
+        SASSERT(m_indices.contains(id));        
+        return m_indices[id];
     }
 
-    void context::add_objective(app* t, bool is_max) {
+    unsigned context::add_objective(app* t, bool is_max) {
         app_ref tr(t, m);
         unsigned index = m_optsmt.get_num_objectives();
         m_optsmt.add(t, is_max);
         m_objectives.push_back(objective(is_max, tr, index));
+        return index;
     }
 
     lbool context::optimize() {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index bce4ad3db..cb46494cd 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -36,6 +36,7 @@ namespace opt {
 
     class context {
         typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
+        typedef map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> map_id;
         enum objective_t {
             O_MAXIMIZE,
             O_MINIMIZE,
@@ -65,13 +66,14 @@ namespace opt {
         params_ref          m_params;
         optsmt              m_optsmt;        
         map_t               m_maxsmts;
+        map_id              m_indices;
         vector<objective>   m_objectives;
         model_ref           m_model;
     public:
         context(ast_manager& m);
         ~context();
-        void add_soft_constraint(expr* f, rational const& w, symbol const& id);
-        void add_objective(app* t, bool is_max);
+        unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
+        unsigned add_objective(app* t, bool is_max);
         void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
 
         lbool optimize();