diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7f9183d9a..54e7f351c 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -805,8 +805,9 @@ public:
     lbool init_local() {
         m_lower.reset();
         m_trail.reset();
+        lbool is_sat = l_true;
         obj_map<expr, rational> new_soft;
-        lbool is_sat = find_mutexes(new_soft);
+        is_sat = find_mutexes(new_soft);
         if (is_sat != l_true) {
             return is_sat;
         }
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 85b19e427..21537a570 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -333,8 +333,15 @@ namespace opt {
         TRACE("opt", tout << mk_pp(f, m) << " weight: " << w << "\n";);
         SASSERT(m.is_bool(f));
         SASSERT(w.is_pos());
-        m_soft_constraints.push_back(f);
-        m_weights.push_back(w);
+        unsigned index = 0;
+        if (m_soft_constraint_index.find(f, index)) {
+            m_weights[index] += w;
+        }
+        else {
+            m_soft_constraint_index.insert(f, m_weights.size());
+            m_soft_constraints.push_back(f);
+            m_weights.push_back(w);
+        }
         m_upper += w;
     }
 
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 5ecb023f6..358ff4995 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -120,6 +120,7 @@ namespace opt {
         unsigned                  m_index;
         scoped_ptr<maxsmt_solver_base> m_msolver;
         expr_ref_vector  m_soft_constraints;
+        obj_map<expr, unsigned> m_soft_constraint_index;
         expr_ref_vector  m_answer;
         vector<rational> m_weights;
         rational         m_lower;
@@ -138,7 +139,6 @@ namespace opt {
         expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
         rational weight(unsigned idx) const { return m_weights[idx]; }
         void commit_assignment();
-        rational get_value() const;
         rational get_lower() const;
         rational get_upper() const;        
         void update_lower(rational const& r);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index b95bb62e8..e63e29dc5 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -360,6 +360,7 @@ namespace opt {
         }
         if (scoped) get_solver().pop(1);
         if (result == l_true && committed) ms.commit_assignment();
+        DEBUG_CODE(if (result == l_true) validate_maxsat(id););
         return result;
     }
 
@@ -1448,6 +1449,32 @@ namespace opt {
         return out.str();
     }
 
+    void context::validate_maxsat(symbol const& id) {
+        maxsmt& ms = *m_maxsmts.find(id);
+        for (unsigned i = 0; i < m_objectives.size(); ++i) {
+            objective const& obj = m_objectives[i];
+            if (obj.m_id == id) {
+                SASSERT(obj.m_type == O_MAXSMT);
+                rational value(0);
+                expr_ref val(m);
+                for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
+                    bool evaluated = m_model->eval(obj.m_terms[i], val);
+                    SASSERT(evaluated);
+                    CTRACE("opt", evaluated && !m.is_true(val) && !m.is_false(val), tout << mk_pp(obj.m_terms[i], m) << " " << val << "\n";);
+                    CTRACE("opt", !evaluated, tout << mk_pp(obj.m_terms[i], m) << "\n";);
+                    if (evaluated && !m.is_true(val)) {
+                        value += obj.m_weights[i];
+                    }
+                    // TBD: check that optimal was not changed.
+                }
+                value = obj.m_adjust_value(value);
+                rational value0 = ms.get_lower();
+                TRACE("opt", tout << "value " << value << " " << value0 << "\n";);
+                SASSERT(value == value0);
+            }
+        }
+    }
+
     void context::validate_lex() {
         rational r1;
         expr_ref val(m);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index ef02a4cbe..461506258 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -291,6 +291,7 @@ namespace opt {
 
 
         void validate_lex();
+        void validate_maxsat(symbol const& id);
 
         void display_benchmark();