diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 42c73f8d0..0e08886f5 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -247,6 +247,7 @@ public:
                 break;
             }
         }
+        m_lower = m_upper;
         trace();
         return l_true;
     }
@@ -468,6 +469,9 @@ public:
         fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);
         m_lower += w;
+        if (m_st == s_primal_dual) {
+            m_lower = std::min(m_lower, m_upper);
+        }
         trace();
     }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c0118230f..db82cbe0e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -959,11 +959,13 @@ namespace sat {
                 assign(lit, justification());
                 break;
             case l_false: {
+                m_assumptions.push_back(lit);       
                 SASSERT(!inconsistent());
                 set_conflict(justification(), ~lit);
                 flet<bool> _min1(m_config.m_minimize_core, false);
                 flet<bool> _min2(m_config.m_minimize_core_partial, false);
                 resolve_conflict_for_unsat_core();
+                m_assumptions.pop_back();
                 weight += weights[i];
                 blocker.push_back(lit);
                 TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 94917e190..1b4063b17 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -106,7 +106,11 @@ public:
         dep2asm_t dep2asm;
         VERIFY(l_true == internalize_formulas());
         VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm));
-        m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights);
+        svector<unsigned> nweights;
+        for (unsigned i = 0; i < m_asms.size(); ++i) {
+            nweights.push_back((unsigned) m_weights[i]);
+        }
+        m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
     }
  
     lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {       
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 227a34b51..fea5ac86e 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -65,9 +65,6 @@ struct simplify_tactic::imp {
                 proof * pr = g.pr(idx);
                 new_pr     = m().mk_modus_ponens(pr, new_pr);
             }
-            if (m_manager.is_false(new_curr)) {
-                std::cout << mk_pp(curr, m_manager) << " => " << new_curr << "\n";
-            }
             g.update(idx, new_curr, new_pr, g.dep(idx));
         }
         TRACE("after_simplifier_bug", g.display(tout););