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 9af35d9b3..a27a1a4d2 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";);