diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index d4dac1db3..d38b5e38c 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -129,12 +129,13 @@ extern "C" {
         RESET_ERROR_CODE();
         model_ref _m;
         to_optimize_ref(o).get_model(_m);
-        if (!_m) {
-            SET_ERROR_CODE(Z3_INVALID_USAGE);
-            RETURN_Z3(0);
-        }
         Z3_model_ref * m_ref = alloc(Z3_model_ref); 
-        m_ref->m_model = _m;
+        if (_m) {
+            m_ref->m_model = _m;
+        }
+        else {
+            m_ref->m_model = alloc(model, mk_c(c)->m());
+        }
         mk_c(c)->save_object(m_ref);
         RETURN_Z3(of_model(m_ref));
         Z3_CATCH_RETURN(0);
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index e892ee70f..8284125d5 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -142,12 +142,12 @@ namespace Microsoft.Z3
 
         public ArithExpr GetLower(uint index) 
         {
-            return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
+            return (ArithExpr)Expr.Create(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));
+            return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
 	    public override string ToString() 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 0695abc6d..c3dd32ab8 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -114,10 +114,12 @@ namespace opt {
 
     void context::get_model(model_ref& mdl) {
         mdl = m_model;
-        if (m_model_converter) {
-            (*m_model_converter)(mdl, 0);
+        if (mdl) {
+            if (m_model_converter) {
+                (*m_model_converter)(mdl, 0);
+            }
+            get_solver().mc()(mdl, 0);
         }
-        get_solver().mc()(mdl, 0);
     }
 
     lbool context::execute_min_max(unsigned index, bool committed) {
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index b0d983bca..485b68e2a 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1315,6 +1315,7 @@ namespace smt {
                     }
                     theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row);
                     if (curr_x_i == null_theory_var) {
+                        TRACE("opt", tout << "unbounded\n";);
                         // we can increase/decrease curr_x_j as much as we want.
                         x_i   = null_theory_var; // unbounded
                         x_j   = curr_x_j;
@@ -1340,7 +1341,8 @@ namespace smt {
                     }
                 }
             }
-            TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";);
+            TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";
+                  tout << "skipped row: " << (skipped_row?"yes":"no") << "\n";);
 
             if (x_j == null_theory_var) {
                 TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);