diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index d8b166924..e6b452603 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -155,7 +155,7 @@ public:
     
 
     void add_soft(expr* e, rational const& w) {
-        TRACE("opt", tout << mk_pp(e, m) << "\n";);
+        TRACE("opt", tout << mk_pp(e, m) << " |-> " << w << "\n";);
         expr_ref asum(m), fml(m);
         app_ref cls(m);
         rational weight(0);
@@ -290,7 +290,10 @@ public:
     }
 
     void process_mutex(expr_ref_vector& mutex) {
-        TRACE("opt", tout << mutex << "\n";);
+        TRACE("opt", 
+              for (unsigned i = 0; i < mutex.size(); ++i) {
+                  tout << mk_pp(mutex[i].get(), m) << " |-> " << get_weight(mutex[i].get()) << "\n";
+              });
         if (mutex.size() <= 1) {
             return;
         }
@@ -298,20 +301,22 @@ public:
         ptr_vector<expr> core(mutex.size(), mutex.c_ptr());
         remove_soft(core, m_asms);
         rational weight(0), sum1(0), sum2(0);
+        vector<rational> weights;
         for (unsigned i = 0; i < mutex.size(); ++i) {
-            sum1 += get_weight(mutex[i].get());
+            rational w = get_weight(mutex[i].get());
+            weights.push_back(w);
+            sum1 += w;
+            m_asm2weight.remove(mutex[i].get());
         }
-        while (!mutex.empty()) {
-            expr_ref soft = mk_or(mutex);
-            rational w = get_weight(mutex.back());
+        for (unsigned i = mutex.size(); i > 0; ) {
+            --i;
+            expr_ref soft(m.mk_or(i+1, mutex.c_ptr()), m);
+            rational w = weights[i];
             weight = w - weight;
-            m_lower += weight*rational(mutex.size()-1);
-            sum2 += weight*rational(mutex.size());
+            m_lower += weight*rational(i);
+            sum2 += weight*rational(i+1);
             add_soft(soft, weight);
-            mutex.pop_back();
-            while (!mutex.empty() && get_weight(mutex.back()) == w) {
-                mutex.pop_back();
-            }
+            for (; i > 0 && weights[i-1] == w; --i) {} 
             weight = w;
         }        
         SASSERT(sum1 == sum2);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index d1fae0156..682978287 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -379,7 +379,6 @@ private:
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         TRACE("sat", g->display_with_dependencies(tout););
-        std::cout << "exprs: " << g->num_exprs() << "\n";
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {