diff --git a/src/opt/dual_maxres.cpp b/src/opt/dual_maxres.cpp
index 5895f0573..3595149bf 100644
--- a/src/opt/dual_maxres.cpp
+++ b/src/opt/dual_maxres.cpp
@@ -64,6 +64,7 @@ class dual_maxres : public maxsmt_solver_base {
     expr_ref_vector  m_B;
     expr_ref_vector  m_asms;    
     obj_map<expr, rational> m_asm2weight;
+    obj_map<expr, expr*>    m_soft2asm;
     ptr_vector<expr> m_new_core;
     mus              m_mus;
     expr_ref_vector  m_trail;
@@ -89,6 +90,11 @@ public:
     void add_soft(expr* e, rational const& w) {
         TRACE("opt", tout << mk_pp(e, m) << "\n";);
         expr_ref asum(m), fml(m);
+        expr* f;
+        if (m_soft2asm.find(e, f)) {
+            m_asm2weight.find(f) += w;
+            return;
+        }
         if (is_literal(e)) {
             asum = e;
         }
@@ -97,6 +103,7 @@ public:
             fml = m.mk_iff(asum, e);
             m_s->assert_expr(fml);
         }
+        m_soft2asm.insert(e, asum);
         new_assumption(asum, w);
         m_upper += w;
     }
@@ -461,6 +468,7 @@ public:
         m_upper.reset();
         m_lower.reset();
         m_asm2weight.reset();
+        m_soft2asm.reset();
         m_trail.reset();
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             add_soft(m_soft[i].get(), m_weights[i]);
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 58cd241d0..ecdd788a9 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -63,6 +63,12 @@ public:
         TRACE("opt", tout << mk_pp(e, m) << "\n";);
         expr_ref asum(m), fml(m);
         app_ref cls(m);
+        info inf(0,rational(0));
+        if (m_asm2info.find(e, inf)) {
+            inf.m_weight += w;
+            m_asm2info.insert(e, inf);
+            return;
+        }
         cls = mk_cls(e);
         m_trail.push_back(cls);
         if (is_literal(e)) {
@@ -104,15 +110,21 @@ public:
                 return l_undef;
             }
             switch (is_sat) {
-            case l_true: 
+            case l_true: {
                 m_s->get_model(m_model);
+                expr_ref tmp(m);
+                DEBUG_CODE(
+                    for (unsigned i = 0; i < m_asms.size(); ++i) {
+                        VERIFY(m_model->eval(m_asms[i].get(), tmp));                        
+                        SASSERT(m.is_true(tmp));
+                    });
                 for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    expr_ref tmp(m);
                     VERIFY(m_model->eval(m_soft[i].get(), tmp));
                     m_assignment[i] = m.is_true(tmp);
                 }
                 m_upper = m_lower;
                 return l_true;
+            }
             case l_undef:
                 return l_undef;
             default: