diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index e708788f6..3707e5aeb 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -229,6 +229,7 @@ public:
     }
 
     lbool primal_dual_solver() {
+        std::cout << "pd\n";
         if (!init()) return l_undef;
         lbool is_sat = init_local();
         trace();
@@ -315,14 +316,13 @@ public:
 
     void found_optimum() {
         IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
-        rational upper(0);
+        m_lower.reset();
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
             if (!m_assignment[i]) {
-                upper += m_weights[i];
+                m_lower += m_weights[i];
             }
         }
-        SASSERT(upper == m_lower);
         m_upper = m_lower;
         m_found_feasible_optimum = true;
     }
@@ -397,10 +397,11 @@ public:
     void get_current_correction_set(model* mdl, exprs& cs) {
         cs.reset();
         if (!mdl) return;
-        for (unsigned i = 0; i < m_asms.size(); ++i) {
-            if (is_false(mdl, m_asms[i].get())) {
-                cs.push_back(m_asms[i].get());
+        for (expr* a : m_asms) {
+            if (is_false(mdl, a)) {
+                cs.push_back(a);
             }
+            TRACE("opt", expr_ref tmp(m); mdl->eval(a, tmp, true); tout << mk_pp(a, m) << ": " << tmp << "\n";);
         }
         TRACE("opt", display_vec(tout << "new correction set: ", cs););
     }
@@ -509,6 +510,7 @@ public:
         trace();
         if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
             exprs cs;
+            TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
             get_current_correction_set(m_csmodel.get(), cs);
             m_correction_set_size = cs.size();
             if (m_correction_set_size < core.size()) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2b31e243c..8d73ea7c8 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -819,7 +819,7 @@ namespace opt {
         bool is_max = is_maximize(fml, term, orig_term, index);
         bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
         if (is_min && get_pb_sum(term, terms, weights, offset)) {
-            TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";);
+            TRACE("opt", tout << "try to convert minimization\n" << mk_pp(term, m) << "\n";);
             // minimize 2*x + 3*y 
             // <=>
             // (assert-soft (not x) 2)