fix #2523

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/opt/optsmt.cpp

@@ -199,7 +199,6 @@ namespace opt {
                 m_s->maximize_objective(obj_index, bound);
                 m_s->get_model(m_model);
                 SASSERT(m_model);
-                m_s->get_labels(m_labels);
                 inf_eps obj = m_s->saved_objective_value(obj_index);
                 update_lower_lex(obj_index, obj, is_maximize);
                 if (!is_int || !m_lower[obj_index].is_finite()) {
@@ -374,7 +373,8 @@ namespace opt {
                 m_s->maximize_objective(i, tmp);
                 m_lower[i] = m_s->saved_objective_value(i);
             }
-
+            m_best_model = m_model;
+            m_s->get_labels(m_labels);
             m_context.set_model(m_model);
         }
     }
@@ -525,7 +525,6 @@ namespace opt {
 
             m_s->maximize_objective(obj_index, bound);
             m_s->get_model(m_model);
-            m_s->get_labels(m_labels);
             inf_eps obj = m_s->saved_objective_value(obj_index);
             update_lower_lex(obj_index, obj, is_maximize);
             TRACE("opt", tout << "strengthen bound: " << bound << "\n";);
@@ -590,7 +589,7 @@ namespace opt {
     }
 
     void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {        
-        mdl = m_model.get();
+        mdl = m_best_model.get();
         labels = m_labels;
     }
 

src/opt/optsmt.h

@@ -39,7 +39,7 @@ namespace opt {
         expr_ref_vector  m_lower_fmls;
         svector<smt::theory_var> m_vars;
         symbol           m_optsmt_engine;
-        model_ref        m_model;
+        model_ref        m_model, m_best_model;
         svector<symbol>  m_labels;
         sref_vector<model> m_models;
     public:

src/smt/theory_seq.cpp

@@ -1472,7 +1472,6 @@ bool theory_seq::branch_variable_mb() {
             break;
         }
     }
-    CTRACE("seq", change, get_context().display(tout << "branch_variable_mb\n"););
     return change;
 }
 
@@ -2290,6 +2289,7 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
         return;
     TRACE("seq",
           tout << "scope: " << ctx.get_scope_level() << "\n";
+          tout << lits << "\n";
           ctx.display_detailed_literal(tout << "assert:", lit);
           ctx.display_literals_verbose(tout << " <- ", lits);
           if (!lits.empty()) tout << "\n"; display_deps(tout, dep););
@@ -2601,7 +2601,6 @@ bool theory_seq::is_var(expr* a) const {
         !m_util.str.is_unit(a) &&
         !m_util.str.is_itos(a) &&
         !m_util.str.is_nth_i(a) && 
-        // !m_util.str.is_extract(a) && 
         !m.is_ite(a);
 }