more updates for #1439

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/opt_context.cpp

@@ -122,6 +122,7 @@ namespace opt {
         m_bv(m),
         m_hard_constraints(m),
         m_solver(0),
+        m_pareto1(false),
         m_box_index(UINT_MAX),
         m_optsmt(m),
         m_scoped_state(m),
@@ -294,12 +295,19 @@ namespace opt {
         if (0 == m_objectives.size()) {
             // no op
         }
+        else if (1 == m_objectives.size()) {
+            if (m_pareto1) {
+                is_sat = l_false;
+                m_pareto1 = false;
+            }
+            else {
+                m_pareto1 = (pri == symbol("pareto"));
+                is_sat = execute(m_objectives[0], true, false);
+            }
+        }
         else if (pri == symbol("pareto")) {
             is_sat = execute_pareto();
         }
-        else if (1 == m_objectives.size()) {
-            is_sat = execute(m_objectives[0], true, false);
-        }
         else if (pri == symbol("box")) {
             is_sat = execute_box();
         }
@@ -1358,13 +1366,14 @@ namespace opt {
     }
 
     void context::clear_state() {
-        set_pareto(0);
+        set_pareto(0);        
         m_box_index = UINT_MAX;
         m_model.reset();
     }
 
     void context::set_pareto(pareto_base* p) {
         m_pareto = p;        
+        m_pareto1 = p != nullptr;
     }
 
     void context::collect_statistics(statistics& stats) const {

src/opt/opt_context.h

@@ -144,7 +144,8 @@ namespace opt {
         ref<opt_solver>     m_opt_solver;
         ref<solver>         m_solver;
         ref<solver>         m_sat_solver;
-        scoped_ptr<pareto_base>          m_pareto;
+        scoped_ptr<pareto_base> m_pareto;
+        bool                 m_pareto1;
         scoped_ptr<qe::qmax> m_qmax;
         sref_vector<model>  m_box_models;
         unsigned            m_box_index;

src/sat/sat_model_converter.cpp

@@ -74,9 +74,7 @@ namespace sat {
             DEBUG_CODE({
                 // all clauses must be satisfied
                 bool sat = false;
-                it2 = it->m_clauses.begin();
+                for (literal l : m_clauses) {
-                for (; it2 != end2; ++it2) {
-                    literal l = *it2;
                     if (l == null_literal) {
                         SASSERT(sat);
                         sat = false;