diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp
index 6cad9a8c2..2e3d59a36 100644
--- a/src/opt/hitting_sets.cpp
+++ b/src/opt/hitting_sets.cpp
@@ -58,7 +58,10 @@ namespace opt {
             m_cancel(false), 
             m_max_weight(0), 
             m_weights_var(0),
-            m_solver(m_params,0) {}
+            m_solver(m_params,0) {
+            m_params.set_bool("elim_vars", false);
+            m_solver.updt_params(m_params);
+        }
         ~imp() {}
 
         void add_weight(rational const& w) {
@@ -245,6 +248,9 @@ namespace opt {
                 unsigned i = 0, j = 0;
                 set_undef_to_false();
                 if (values_satisfy_Ts(i)) {
+                    if (m_upper > m_max_weight) {
+                        IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";);
+                    }
                     return l_true;
                 }
                 
@@ -282,21 +288,44 @@ namespace opt {
         }
 
         lbool compute_U2() {
-            lbool is_sat = m_solver.check();
-            if (is_sat == l_true) {                
-                sat::model const& model = m_solver.get_model();
-                m_value_saved.reset();
-                m_upper.reset();
-                for (unsigned i = 0; i < m_vars.size(); ++i) {
-                    m_value_saved.push_back(model[m_vars[i]]);
-                    if (model[m_vars[i]] == l_true) {
-                        m_upper += m_weights[i];
+            lbool is_sat = l_true;
+            while (true) {
+                is_sat = m_solver.check();
+                if (is_sat == l_true) {                
+                    sat::model const& model = m_solver.get_model();
+                    m_value_saved.reset();
+                    m_upper.reset();
+                    for (unsigned i = 0; i < m_vars.size(); ++i) {
+                        m_value_saved.push_back(model[m_vars[i]]);
+                        if (model[m_vars[i]] == l_true) {
+                            m_upper += m_weights[i];
+                        }
                     }
+                    IF_VERBOSE(1, verbose_stream() << "(hs.upper " << m_upper << ")\n";);
+                    m_solver.pop(m_solver.scope_lvl());
+
                 }
+                break;
             }
             return is_sat;
         }
 
+        bool block_model(sat::model const& model) {
+            rational value(0);
+            svector<sat::literal> lits;
+            for (unsigned i = 0; i < m_vars.size(); ++i) {
+                if (value >= m_max_weight) {
+                    m_solver.mk_clause(lits.size(), lits.c_ptr());
+                    return true;
+                }
+                if (model[m_vars[i]] == l_true) {
+                    value += m_weights[i];
+                    lits.push_back(sat::literal(m_vars[i], true));
+                }
+            }
+            return false;
+        }
+
         // compute upper bound for hitting set.
         bool compute_U1() {        
             rational w(0);
@@ -329,9 +358,6 @@ namespace opt {
             m_upper = w;
             m_value_saved.reset();
             m_value_saved.append(m_value);
-            if (m_upper > m_max_weight) {
-                IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";);
-            }
             return !m_cancel;
         }
 
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 23c1a59b2..21667e5f8 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -125,7 +125,7 @@ namespace opt {
     }
 
     lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        TRACE("opt", {
+        TRACE("opt_verbose", {
             tout << "context size: " << m_context.size() << "\n";            
             for (unsigned i = 0; i < m_context.size(); ++i) {
                 tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 1c07b05c8..00c445402 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -928,30 +928,36 @@ namespace opt {
             model_ref mdl;
             s().get_model(mdl);
             for (unsigned i = 0; i < num_soft(); ++i) {
-                if (!m_seed[i]) {
-                    if (is_true(mdl, m_soft[i].get())) {
-                        m_seed[i] = true;                        
-                    }
-                    else {
-                        ensure_active(i);
-                        m_asms.push_back(m_aux[i].get());
-                        lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
-                        TRACE("opt", tout 
-                              << "check: " << mk_pp(m_asms.back(), m) 
-                              << ":" << is_sat << "\n";);
-                        switch(is_sat) {
-                        case l_undef: 
-                            return false;
-                        case l_false: 
-                            ++m_stats.m_num_model_expansions_failure;
-                            m_asms.pop_back(); 
-                            break;
-                        case l_true: 
-                            ++m_stats.m_num_model_expansions_success;
-                            s().get_model(mdl);
-                            m_seed[i] = true; 
-                            break;                     
-                        }
+                ensure_active(i);    
+                m_seed[i] = false;
+            }
+            for (unsigned i = 0; i < m_asms.size(); ++i) {
+                m_seed[m_aux2index.find(m_asms[i])] = true; 
+            }
+
+            for (unsigned i = 0; i < num_soft(); ++i) {
+                if (m_seed[i]) {
+                    // already an assumption
+                }
+                else if (is_true(mdl, m_soft[i].get())) {
+                    m_seed[i] = true;                    
+                    m_asms.push_back(m_aux[i].get());
+                }
+                else {
+                    m_asms.push_back(m_aux[i].get());
+                    lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
+                    switch(is_sat) {
+                    case l_undef: 
+                        return false;
+                    case l_false: 
+                        ++m_stats.m_num_model_expansions_failure;
+                        m_asms.pop_back(); 
+                        break;
+                    case l_true: 
+                        ++m_stats.m_num_model_expansions_success;
+                        s().get_model(mdl);
+                        m_seed[i] = true; 
+                        break;                     
                     }
                 }
             }
@@ -971,6 +977,11 @@ namespace opt {
                       tout << "new upper: " << m_upper << "\n";
                       model_smt2_pp(tout, m, *(mdl.get()), 0););
             }
+            DEBUG_CODE(                
+                for (unsigned i = 0; i < num_soft(); ++i) {
+                    SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]);
+                });
+            
             return true;
         }