diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp
index 8cc2c0304..d85e6b3f4 100644
--- a/src/opt/hitting_sets.cpp
+++ b/src/opt/hitting_sets.cpp
@@ -204,7 +204,7 @@ namespace opt {
                 set_conflict(0, justification(justification::AXIOM));
             }
             else if (sz == 1) {                
-                IF_VERBOSE(1, verbose_stream() << "unit literal : " << S[0] << " " << val << "\n";);
+                IF_VERBOSE(2, verbose_stream() << "unit literal : " << S[0] << " " << val << "\n";);
                 assign(S[0], val, justification(justification::AXIOM));
             }
             else {
@@ -221,6 +221,7 @@ namespace opt {
                     inc_score(clause_id);
                 }
                 TRACE("opt", display(tout, j););
+                IF_VERBOSE(1, if (!sign) display(verbose_stream(), j););
                 if (!sign && m_enable_simplex) {
                     add_simplex_row(!sign, sz, S);
                 }
@@ -246,6 +247,7 @@ namespace opt {
             pop(scope_lvl());
 
 
+            IF_VERBOSE(1, verbose_stream() << "(hsmax.negated-size: " << fsz << ")\n";);
 #if 0
             // garbage collect agressively on exit.
             // all learned clases for negative branches are
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index b8eeb0d09..58c5c2017 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -269,6 +269,9 @@ namespace opt {
             if (r == l_true && !get_lower_as_num(i).is_finite()) {
                 return r;
             }
+            if (r == l_true && i + 1 < m_objectives.size()) {
+                update_lower(true);
+            }
         }
         DEBUG_CODE(if (r == l_true) validate_lex(););
         return r;
@@ -841,6 +844,7 @@ namespace opt {
         switch(obj.m_type) {
         case O_MAXSMT: {
             rational r = m_maxsmts.find(obj.m_id)->get_upper();
+            TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
             if (obj.m_neg) r.neg();
             r += obj.m_offset;
             return inf_eps(r);
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 00c445402..8d405196c 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -701,9 +701,9 @@ namespace opt {
                     TRACE("opt", tout << "no more cores\n";);
                     m_lower = m_upper;
                     return l_true;
-                 }
-             }
-             return l_true;
+                }
+            }
+            return l_true;
         }
 
     private:
@@ -785,7 +785,7 @@ namespace opt {
                 switch (is_sat) {
                 case l_true:
                     if (lower > m_lower) {
-                        m_lower = lower;
+                        m_lower = lower;                        
                     }
                     return true;
                 case l_false: