From 0fdf01e410295cd36a508f3ad9e71d26962d6579 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Jun 2016 04:53:28 -0700
Subject: [PATCH] avoid crash on box models under cancellation. Issue #        
    SASSERT(!m_box_models.empty());

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp      | 15 ++++++++-------
 src/opt/opt_context.cpp | 18 +++++++++++-------
 2 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index b6950f674..7e4acd979 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -189,9 +189,10 @@ public:
         trace_bounds(m_trace_id.c_str());
     }
 
+#define RUNDEF() { std::cout << __LINE__ << "\n"; return l_undef; }
     lbool mus_solver() {
         lbool is_sat = l_true;
-        if (!init()) return l_undef;
+        if (!init()) RUNDEF();
         init_local();
         trace();
         while (m_lower < m_upper) {
@@ -203,7 +204,7 @@ public:
                   );
             is_sat = check_sat_hill_climb(m_asms);
             if (m.canceled()) {
-                return l_undef;
+                RUNDEF();
             }
             switch (is_sat) {
             case l_true: 
@@ -219,7 +220,7 @@ public:
                 }
                 break;
             case l_undef:
-                return l_undef;
+                RUNDEF();
             default:
                 break;
             }
@@ -229,14 +230,14 @@ public:
     }
 
     lbool primal_dual_solver() {
-        if (!init()) return l_undef;
+        if (!init()) RUNDEF();
         init_local();
         trace();
         exprs cs;
         while (m_lower < m_upper) {
             lbool is_sat = check_sat_hill_climb(m_asms);
             if (m.canceled()) {
-                return l_undef;
+                RUNDEF();
             }
             switch (is_sat) {
             case l_true: 
@@ -259,7 +260,7 @@ public:
                 }
                 break;
             case l_undef:
-                return l_undef;
+                RUNDEF();
             default:
                 break;
             }
@@ -339,7 +340,7 @@ public:
         case s_primal_dual:
             return primal_dual_solver();
         }
-        return l_undef;
+        RUNDEF();
     }
 
     virtual void collect_statistics(statistics& st) const { 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 788921205..7a59c1ddb 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -366,12 +366,16 @@ namespace opt {
     }    
 
     lbool context::execute_box() {
-        if (m_box_index < m_objectives.size()) {
-            SASSERT(m_box_index < m_box_models.size());            
+        if (m_box_index < m_box_models.size()) {
             m_model = m_box_models[m_box_index];
             ++m_box_index;           
             return l_true;
         }
+        if (m_box_index < m_objectives.size()) {
+            m_model = 0;
+            ++m_box_index;
+            return l_undef;
+        }
         if (m_box_index != UINT_MAX && m_box_index >= m_objectives.size()) {
             m_box_index = UINT_MAX;
             return l_false;
@@ -384,17 +388,14 @@ namespace opt {
             if (obj.m_type == O_MAXSMT) {
                 solver::scoped_push _sp(get_solver());
                 r = execute(obj, false, false);
-                if (r == l_true) {
-                    m_box_models.push_back(m_model.get());
-                }
+                m_box_models.push_back(m_model.get());
             }
             else {
                 m_box_models.push_back(m_optsmt.get_model(j));
                 ++j;
             }
         }
-        if (r == l_true && m_objectives.size() > 0) {
-            SASSERT(!m_box_models.empty());
+        if (r == l_true && m_box_models.size() > 0) {
             m_model = m_box_models[0];
         }
         return r;
@@ -498,6 +499,9 @@ namespace opt {
     }
 
     std::string context::reason_unknown() const { 
+        if (m.canceled()) {
+            return Z3_CANCELED_MSG;
+        }
         if (m_solver.get()) {
             return m_solver->reason_unknown();
         }