diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index d951f7710..f09d35158 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -100,13 +100,34 @@ public:
 
 ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception(););
 
-ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", {
-    if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
-        throw cmd_exception("model is not available");
-    model_ref m;
-    ctx.get_check_sat_result()->get_model(m);
-    ctx.display_model(m);
-});
+class get_model_cmd : public cmd {
+    unsigned m_index;
+public:
+    get_model_cmd(): cmd("get-model"), m_index(0) {}
+    virtual char const * get_usage() const { return "[<index of box objective>]"; }   
+    virtual char const * get_descr(cmd_context & ctx) const { 
+        return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; 
+    }
+    virtual unsigned get_arity() const { return VAR_ARITY; } 
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; }
+    virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }                           
+    virtual void execute(cmd_context & ctx) { 
+        if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
+            throw cmd_exception("model is not available");
+        model_ref m;
+        if (m_index > 0 && ctx.get_opt()) {
+            ctx.get_opt()->get_box_model(m, m_index);
+        }
+        else {
+            ctx.get_check_sat_result()->get_model(m);
+        }
+        ctx.display_model(m);
+    }                    
+    virtual void reset(cmd_context& ctx) {
+        m_index = 0;
+    }
+};
+
 
 ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
     if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 8eee632dc..92943c71c 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -124,6 +124,7 @@ public:
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
     virtual bool print_model() const = 0;
+    virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
     virtual void updt_params(params_ref const& p) = 0;
 };
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d1b7a489e..af3c57baa 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -342,6 +342,14 @@ namespace opt {
         fix_model(mdl);
     }
 
+    void context::get_box_model(model_ref& mdl, unsigned index) {
+        if (index >= m_box_models.size()) {
+            throw default_exception("index into models is out of bounds");
+        }
+        mdl = m_box_models[index];
+        fix_model(mdl);
+    }
+
     lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
         if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index, is_max);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index f51f75830..53bfc19c5 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -186,6 +186,7 @@ namespace opt {
         virtual bool print_model() const;
         virtual void set_model(model_ref& _m) { m_model = _m; }
         virtual void get_model(model_ref& _m);
+        virtual void get_box_model(model_ref& _m, unsigned index);
         virtual void fix_model(model_ref& _m);
         virtual void collect_statistics(statistics& stats) const;
         virtual proof* get_proof() { return 0; }