diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 46122d619..56b152caa 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -570,11 +570,11 @@ namespace opt {
         m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
         m_opt_solver->set_logic(m_logic);
         m_solver = m_opt_solver.get();
+        m_opt_solver->ensure_pb();
     
-        if (opt_params(m_params).priority() == symbol("pareto") ||
-            (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
-            m_opt_solver->ensure_pb();
-        }        
+        //if (opt_params(m_params).priority() == symbol("pareto") ||
+        //    (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
+        //}        
     }
 
     void context::setup_arith_solver() {
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 62fb99a11..bd975115b 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -154,7 +154,6 @@ namespace sat {
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
-
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());