diff --git a/scripts/update_api.py b/scripts/update_api.py
index ab1b4d6fd..d4d1ab0e0 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1820,8 +1820,8 @@ _error_handler_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
 _lib.Z3_set_error_handler.restype  = None
 _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
-push_eh_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
-pop_eh_type   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
+push_eh_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
+pop_eh_type   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
 fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 
 fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 6f4dcf430..d3d6067c3 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -11237,12 +11237,16 @@ def ensure_prop_closures():
         _prop_closures = PropClosures()
 
 
-def user_prop_push(ctx):
-    _prop_closures.get(ctx).push()
+def user_prop_push(ctx, cb):
+    prop = _prop_closures.get(ctx)
+    prop.cb = cb
+    prop.push()
 
 
-def user_prop_pop(ctx, num_scopes):
-    _prop_closures.get(ctx).pop(num_scopes)
+def user_prop_pop(ctx, cb, num_scopes):
+    prop = _prop_closures.get(ctx)
+    prop.cb = cb
+    pop(num_scopes)
 
 
 def user_prop_fresh(id, ctx):
diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt
index d88d11c0f..c652bcaea 100644
--- a/src/opt/CMakeLists.txt
+++ b/src/opt/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(opt
     opt_lns.cpp
     opt_pareto.cpp
     opt_parse.cpp
+    opt_preprocess.cpp
     optsmt.cpp
     opt_solver.cpp
     pb_sls.cpp
diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 46c7104d5..82eee6f5e 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -26,15 +26,15 @@ Author:
 
 namespace opt {
 
-    bool is_maxlex(weights_t & _ws) {
-        vector<rational> ws(_ws);
-        std::sort(ws.begin(), ws.end());
+    bool is_maxlex(vector<soft> const & _ws) {
+        vector<soft> ws(_ws);
+        std::sort(ws.begin(), ws.end(), [&](soft const& s1, soft const& s2) { return s1.weight < s2.weight; });
         ws.reverse();
         rational sum(0);
-        for (rational const& w : ws) {
+        for (auto const& [e, w, t] : ws) {
             sum += w;
         }
-        for (rational const& w : ws) {
+        for (auto const& [e, w, t] : ws) {
             if (sum > w + w) return false;
             sum -= w;
         }
@@ -185,8 +185,8 @@ namespace opt {
 
     public:
 
-        maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
-            maxsmt_solver_base(c, ws, s),
+        maxlex(maxsat_context& c, unsigned id, vector<soft>& s):
+            maxsmt_solver_base(c, s),
             m(c.get_manager()),
             m_c(c) {
             // ensure that soft constraints are sorted with largest soft constraints first.
@@ -210,8 +210,8 @@ namespace opt {
         }
     };
 
-    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) {
-        return alloc(maxlex, c, id, ws, soft);
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector<soft>& soft) {
+        return alloc(maxlex, c, id, soft);
     }
 
 }
diff --git a/src/opt/maxlex.h b/src/opt/maxlex.h
index b5c1a6e20..fc30b1fd8 100644
--- a/src/opt/maxlex.h
+++ b/src/opt/maxlex.h
@@ -21,9 +21,9 @@ Notes:
 
 namespace opt {
 
-    bool is_maxlex(weights_t & ws);
+    bool is_maxlex(vector<soft> const & ws);
 
-    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector<soft>& soft);
 
 
 };
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 1b4348105..0d1bf2394 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -129,10 +129,10 @@ private:
     typedef ptr_vector<expr> exprs;
 
 public:
-    maxres(maxsat_context& c, unsigned index, 
-           weights_t& ws, expr_ref_vector const& soft, 
+    maxres(maxsat_context& c, unsigned index,
+           vector<soft>& soft,
            strategy_t st):
-        maxsmt_solver_base(c, ws, soft),
+        maxsmt_solver_base(c, soft),
         m_index(index), 
         m_B(m), m_asms(m), m_defs(m),
         m_new_core(m),
@@ -875,17 +875,10 @@ public:
     }
 
     lbool init_local() {
-        m_lower.reset();
         m_trail.reset();
         lbool is_sat = l_true;
-        obj_map<expr, rational> new_soft;
-        is_sat = find_mutexes(new_soft);
-        if (is_sat != l_true) {
-            return is_sat;
-        }
-        for (auto const& kv : new_soft) {
-            add_soft(kv.m_key, kv.m_value);
-        }
+        for (auto const& [e, w, t] : m_soft)
+            add_soft(e, w);
         m_max_upper = m_upper;
         m_found_feasible_optimum = false;
         m_last_index = 0;
@@ -953,12 +946,12 @@ public:
 };
 
 opt::maxsmt_solver_base* opt::mk_maxres(
-    maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
-    return alloc(maxres, c, id, ws, soft, maxres::s_primal);
+    maxsat_context& c, unsigned id, vector<soft>& soft) {
+    return alloc(maxres, c, id, soft, maxres::s_primal);
 }
 
 opt::maxsmt_solver_base* opt::mk_primal_dual_maxres(
-    maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
-    return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual);
+    maxsat_context& c, unsigned id, vector<soft>& soft) {
+    return alloc(maxres, c, id, soft, maxres::s_primal_dual);
 }
 
diff --git a/src/opt/maxres.h b/src/opt/maxres.h
index 85c83efba..25ef9bf05 100644
--- a/src/opt/maxres.h
+++ b/src/opt/maxres.h
@@ -21,9 +21,9 @@ Notes:
 
 namespace opt {
 
-    maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
-    maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
 };
 
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index bf25f3f95..538ecf59b 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -28,6 +28,7 @@ Notes:
 #include "opt/wmax.h"
 #include "opt/opt_params.hpp"
 #include "opt/opt_context.h"
+#include "opt/opt_preprocess.h"
 #include "smt/theory_wmaxsat.h"
 #include "smt/theory_pb.h"
 
@@ -35,17 +36,15 @@ Notes:
 namespace opt {
 
     maxsmt_solver_base::maxsmt_solver_base(
-        maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& softs):
+        maxsat_context& c, vector<soft>& s):
         m(c.get_manager()), 
         m_c(c),
+        m_soft(s),
         m_assertions(m),
         m_trail(m) {
         c.get_base_model(m_model);
         SASSERT(m_model);
         updt_params(c.params());
-        for (unsigned i = 0; i < ws.size(); ++i) {
-            m_soft.push_back(soft(expr_ref(softs.get(i), m), ws[i], false));
-        }
     }
     
     void maxsmt_solver_base::updt_params(params_ref& p) {
@@ -88,14 +87,22 @@ namespace opt {
         m_upper.reset();
         for (soft& s : m_soft) {
             s.set_value(m.is_true(s.s));
-            if (!s.is_true()) m_upper += s.weight;
+            if (!s.is_true())
+                m_upper += s.weight;
         }
+
+        preprocess pp(s());
+        rational lower(0);
+        bool r = pp(m_soft, lower);
+
+        if (lower != 0)
+            m_adjust_value.set_offset(lower + m_adjust_value.get_offset());
         
         TRACE("opt", 
               tout << "upper: " << m_upper << " assignments: ";
               for (soft& s : m_soft) tout << (s.is_true()?"T":"F");              
               tout << "\n";);
-        return true;
+        return r;
     }
 
     void maxsmt_solver_base::set_mus(bool f) {
@@ -165,74 +172,9 @@ namespace opt {
                    verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);                
     }
 
-    lbool maxsmt_solver_base::find_mutexes(obj_map<expr, rational>& new_soft) {
-        m_lower.reset();
-        expr_ref_vector fmls(m);
-        for (soft& s : m_soft) {
-            new_soft.insert(s.s, s.weight);
-            fmls.push_back(s.s);
-        }
-        vector<expr_ref_vector> mutexes;
-        lbool is_sat = s().find_mutexes(fmls, mutexes);
-        if (is_sat != l_true) {
-            return is_sat;
-        }
-        for (auto& mux : mutexes) {
-            process_mutex(mux, new_soft);
-        }
-        return l_true;
-    }
-
-    struct maxsmt_compare_soft {
-        obj_map<expr, rational> const& m_soft;
-        maxsmt_compare_soft(obj_map<expr, rational> const& soft): m_soft(soft) {}
-        bool operator()(expr* a, expr* b) const {
-            return m_soft.find(a) > m_soft.find(b);
-        }
-    };
-
-    void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft) {
-        TRACE("opt", 
-              for (expr* e : mutex) {
-                  tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
-              });
-        if (mutex.size() <= 1) {
-            return;
-        }
-        maxsmt_compare_soft cmp(new_soft);
-        ptr_vector<expr> _mutex(mutex.size(), mutex.data());
-        std::sort(_mutex.begin(), _mutex.end(), cmp);
-        mutex.reset();
-        mutex.append(_mutex.size(), _mutex.data());
-
-        rational weight(0), sum1(0), sum2(0);
-        vector<rational> weights;
-        for (expr* e : mutex) {
-            rational w = new_soft.find(e);
-            weights.push_back(w);
-            sum1 += w;
-            new_soft.remove(e);
-        }
-        for (unsigned i = mutex.size(); i-- > 0; ) {
-            expr_ref soft(m.mk_or(i+1, mutex.data()), m);
-            m_trail.push_back(soft);
-            rational w = weights[i];
-            weight = w - weight;
-            m_lower += weight*rational(i);
-            IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
-            sum2 += weight*rational(i+1);
-            new_soft.insert(soft, weight);
-            for (; i > 0 && weights[i-1] == w; --i) {} 
-            weight = w;
-        }        
-        SASSERT(sum1 == sum2);        
-    }
-
-
 
     maxsmt::maxsmt(maxsat_context& c, unsigned index):
-        m(c.get_manager()), m_c(c), m_index(index), 
-        m_soft_constraints(m), m_answer(m) {}
+        m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {}
 
     lbool maxsmt::operator()() {
         lbool is_sat = l_undef;
@@ -241,25 +183,25 @@ namespace opt {
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
-        if (optp.maxlex_enable() && is_maxlex(m_weights)) {
-            m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
+        if (optp.maxlex_enable() && is_maxlex(m_soft)) {
+            m_msolver = mk_maxlex(m_c, m_index, m_soft);            
         }
-        else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
-            m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+        else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
+            m_msolver = mk_maxres(m_c, m_index, m_soft);            
         }
         else if (maxsat_engine == symbol("pd-maxres")) {            
-            m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft);
         }
         else if (maxsat_engine == symbol("wmax")) {
-            m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
+            m_msolver = mk_wmax(m_c, m_soft);
         }
         else if (maxsat_engine == symbol("sortmax")) {
-            m_msolver = mk_sortmax(m_c, m_weights, m_soft_constraints);
+            m_msolver = mk_sortmax(m_c, m_soft);
         }
         else {
             auto str = maxsat_engine.str();
             warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str());
-            m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_maxres(m_c, m_index, m_soft);
         }
 
         if (m_msolver) {
@@ -360,39 +302,32 @@ namespace opt {
         SASSERT(w.is_pos());
         unsigned index = 0;
         if (m_soft_constraint_index.find(f, index)) {
-            m_weights[index] += w;
+            m_soft[index].weight += w;
         }
         else {
-            m_soft_constraint_index.insert(f, m_weights.size());
-            m_soft_constraints.push_back(f);
-            m_weights.push_back(w);
+            m_soft_constraint_index.insert(f, m_soft.size());
+            m_soft.push_back(soft(expr_ref(f, m), w, false));
         }
         m_upper += w;
     }
 
     struct cmp_first {
         bool operator()(std::pair<unsigned, rational> const& x, std::pair<unsigned, rational> const& y) const {
-            return x.first < y.first;
+            return x.second < y.second;
         }
     };
 
     void maxsmt::display_answer(std::ostream& out) const {
-        vector<std::pair<unsigned, rational>> sorted_weights;
-        unsigned n = m_weights.size();
-        for (unsigned i = 0; i < n; ++i) {
-            sorted_weights.push_back(std::make_pair(i, m_weights[i]));
-        }
-        std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first());
-        sorted_weights.reverse();
-        for (unsigned i = 0; i < n; ++i) {
-            unsigned idx = sorted_weights[i].first;
-            expr* e = m_soft_constraints[idx];
+
+        unsigned idx = 0;
+        for (auto const & [_e, w, t] : m_soft) {
+            expr* e = _e.get();
             bool is_not = m.is_not(e, e);
-            out << m_weights[idx] << ": " << mk_pp(e, m)
+            out << w << ": " << mk_pp(e, m)
                 << ((is_not != get_assignment(idx))?" |-> true ":" |-> false ")
                 << "\n";
-            
-        }
+            ++idx;
+        }       
     }
     
     
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 5bf637dde..4029bb911 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -52,21 +52,23 @@ namespace opt {
     // ---------------------------------------------
     // base class with common utilities used
     // by maxsmt solvers
-    // 
+    //
+
+    struct soft { 
+        expr_ref  s; 
+        rational  weight; 
+        lbool     value;
+        void set_value(bool t) { value = t?l_true:l_undef; }
+        void set_value(lbool t) { value = t; }
+        bool is_true() const { return value == l_true; }
+        soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
+    };
+
     class maxsmt_solver_base : public maxsmt_solver {
     protected:
-        struct soft { 
-            expr_ref  s; 
-            rational  weight; 
-            lbool     value;
-            void set_value(bool t) { value = t?l_true:l_undef; }
-            void set_value(lbool t) { value = t; }
-            bool is_true() const { return value == l_true; }
-            soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
-        };
         ast_manager&     m;
         maxsat_context&  m_c;        
-        vector<soft>     m_soft;
+        vector<soft>&    m_soft;
         expr_ref_vector  m_assertions;
         expr_ref_vector  m_trail;
         rational         m_lower;
@@ -76,8 +78,8 @@ namespace opt {
         params_ref       m_params;           // config
 
     public:
-        maxsmt_solver_base(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft); 
-
+        maxsmt_solver_base(maxsat_context& c, vector<soft>& soft);
+        
         ~maxsmt_solver_base() override {}
         rational get_lower() const override { return m_lower; }
         rational get_upper() const override { return m_upper; }
@@ -102,8 +104,6 @@ namespace opt {
             smt::theory_wmaxsat& operator()();
         };
 
-        lbool find_mutexes(obj_map<expr, rational>& new_soft);
-
         void reset_upper();
         
 
@@ -111,9 +111,6 @@ namespace opt {
         void enable_sls(bool force);
         void trace_bounds(char const* solver);
 
-        void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft);
-
-
     };
 
     /**
@@ -126,10 +123,9 @@ namespace opt {
         maxsat_context&           m_c;
         unsigned                  m_index;
         scoped_ptr<maxsmt_solver_base> m_msolver;
-        expr_ref_vector  m_soft_constraints;
+        vector<soft>     m_soft;
         obj_map<expr, unsigned> m_soft_constraint_index;
         expr_ref_vector  m_answer;
-        vector<rational> m_weights;
         rational         m_lower;
         rational         m_upper;
         adjust_value     m_adjust_value;
@@ -142,9 +138,9 @@ namespace opt {
         void updt_params(params_ref& p);
         void add(expr* f, rational const& w); 
         void set_adjust_value(adjust_value& adj);
-        unsigned size() const { return m_soft_constraints.size(); }
-        expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
-        rational weight(unsigned idx) const { return m_weights[idx]; }
+        unsigned size() const { return m_soft.size(); }
+        expr* operator[](unsigned idx) const { return m_soft[idx].s; }
+        rational weight(unsigned idx) const { return m_soft[idx].weight; }
         void commit_assignment();
         rational get_lower() const;
         rational get_upper() const;        
diff --git a/src/opt/opt_mux.h b/src/opt/opt_mux.h
new file mode 100644
index 000000000..b093026f0
--- /dev/null
+++ b/src/opt/opt_mux.h
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_mux.h
+
+Abstract:
+   
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+    class mux {
+        ast_manager&     m;
+        solver&          s;
+
+    public:
+        mux(solver& s);
+        lbool operator()(vector<soft>& soft, rational& bound);
+    };
+};
diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp
new file mode 100644
index 000000000..f65d5d09b
--- /dev/null
+++ b/src/opt/opt_preprocess.cpp
@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_preprocess.cpp
+
+Abstract:
+   
+    Pre-processing for MaxSMT
+
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/opt_preprocess.h"
+
+namespace opt {
+
+    bool preprocess::find_mutexes(vector<soft>& softs, rational& lower) {
+        expr_ref_vector fmls(m);
+        obj_map<expr, rational> new_soft;
+        for (soft& sf : softs) {
+            m_trail.push_back(sf.s);
+            if (new_soft.contains(sf.s))
+                new_soft[sf.s] += sf.weight;
+            else
+                new_soft.insert(sf.s, sf.weight);
+            fmls.push_back(sf.s);
+        }
+        vector<expr_ref_vector> mutexes;
+        lbool is_sat = s.find_mutexes(fmls, mutexes);
+        if (is_sat == l_false)
+            return true;
+        if (is_sat == l_undef)
+            return false;
+        for (auto& mux : mutexes) 
+            process_mutex(mux, new_soft, lower);
+        softs.reset();
+        for (auto const& [k, v] : new_soft)
+            softs.push_back(soft(expr_ref(k, m), v, false));
+        m_trail.reset();
+        return true;
+    }
+
+    struct maxsmt_compare_soft {
+        obj_map<expr, rational> const& m_soft;
+        maxsmt_compare_soft(obj_map<expr, rational> const& soft): m_soft(soft) {}
+        bool operator()(expr* a, expr* b) const {
+            return m_soft.find(a) > m_soft.find(b);
+        }
+    };
+
+    void preprocess::process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower) {
+        TRACE("opt", 
+              for (expr* e : mutex) {
+                  tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
+              });
+        if (mutex.size() <= 1) 
+            return;
+
+        maxsmt_compare_soft cmp(new_soft);
+        ptr_vector<expr> _mutex(mutex.size(), mutex.data());
+        std::sort(_mutex.begin(), _mutex.end(), cmp);
+        mutex.reset();
+        mutex.append(_mutex.size(), _mutex.data());
+
+        rational weight(0), sum1(0), sum2(0);
+        vector<rational> weights;
+        for (expr* e : mutex) {
+            rational w = new_soft.find(e);
+            weights.push_back(w);
+            sum1 += w;
+            new_soft.remove(e);
+        }
+        for (unsigned i = mutex.size(); i-- > 0; ) {
+            expr_ref soft(m.mk_or(i+1, mutex.data()), m);
+            m_trail.push_back(soft);
+            rational w = weights[i];
+            weight = w - weight;
+            lower += weight*rational(i);
+            IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
+            sum2 += weight*rational(i+1);
+            new_soft.insert(soft, weight);
+            for (; i > 0 && weights[i-1] == w; --i) {} 
+            weight = w;
+        }        
+        SASSERT(sum1 == sum2);        
+    }
+
+    preprocess::preprocess(solver& s):  m(s.get_manager()), s(s), m_trail(m) {}
+    
+    bool preprocess::operator()(vector<soft>& soft, rational& lower) {
+        return find_mutexes(soft, lower);
+    }
+};
diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h
new file mode 100644
index 000000000..8918e5e89
--- /dev/null
+++ b/src/opt/opt_preprocess.h
@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_preprocess.h
+
+Abstract:
+   
+    Pre-processing for MaxSMT
+
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+    class preprocess {
+        ast_manager&     m;
+        solver&          s;
+        expr_ref_vector  m_trail;
+
+        bool find_mutexes(vector<soft>& softs, rational& lower);
+        void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
+
+    public:
+        preprocess(solver& s);
+        bool operator()(vector<soft>& soft, rational& lower);
+    };
+};
diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp
index c6a2f04a9..a6539e129 100644
--- a/src/opt/sortmax.cpp
+++ b/src/opt/sortmax.cpp
@@ -36,34 +36,27 @@ namespace opt {
         expr_ref_vector   m_trail;
         func_decl_ref_vector m_fresh;
         ref<generic_model_converter> m_filter;
-        sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
-            maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {}
+        sortmax(maxsat_context& c, vector<soft>& s): 
+            maxsmt_solver_base(c, s), m_sort(*this), m_trail(m), m_fresh(m) {}
 
         ~sortmax() override {}
 
         lbool operator()() override {
-            obj_map<expr, rational> soft;            
-            if (!init()) {
-                return l_false;
-            }
-            lbool is_sat = find_mutexes(soft);
-            if (is_sat != l_true) {
-                return is_sat;
-            }
+            if (!init()) 
+                return l_undef;
+
+            lbool is_sat = l_true;
             m_filter = alloc(generic_model_converter, m, "sortmax");
-            rational offset = m_lower;
-            m_upper = offset;
             expr_ref_vector in(m);
             expr_ref tmp(m);
             ptr_vector<expr> out;
-            obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
-            for (; it != end; ++it) {
-                if (!it->m_value.is_unsigned()) {
+            for (auto const & [e, w, t] : m_soft) {
+                if (!w.is_unsigned()) {
                     throw default_exception("sortmax can only handle unsigned weights. Use a different heuristic.");
                 }
-                unsigned n = it->m_value.get_unsigned();
+                unsigned n = w.get_unsigned();
                 while (n > 0) {
-                    in.push_back(it->m_key);
+                    in.push_back(e);
                     --n;
                 }
             }
@@ -71,19 +64,15 @@ namespace opt {
 
             // initialize sorting network outputs using the initial assignment.
             unsigned first = 0;
-            it = soft.begin();
-            for (; it != end; ++it) {
-                if (m_model->is_true(it->m_key)) {
-                    unsigned n = it->m_value.get_unsigned();
+            for (auto const & [e, w, t] : m_soft) {
+                if (t == l_true) {
+                    unsigned n = w.get_unsigned();
                     while (n > 0) {
                         s().assert_expr(out[first]);
                         ++first;
                         --n;
                     }
                 }
-                else {
-                    m_upper += it->m_value;
-                }
             }
             while (l_true == is_sat && first < out.size() && m_lower < m_upper) {
                 trace_bounds("sortmax");
@@ -149,8 +138,8 @@ namespace opt {
     };
     
     
-    maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
-        return alloc(sortmax, c, ws, soft);
+    maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector<soft>& s) {
+        return alloc(sortmax, c, s);
     }
 
 }
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 22a660799..812c8f954 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -44,8 +44,8 @@ namespace opt {
         }
 
     public:
-        wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
-            maxsmt_solver_base(c, ws, soft),
+        wmax(maxsat_context& c, vector<soft>& s): 
+            maxsmt_solver_base(c, s),
             m_trail(m),
             m_defs(m) {}
 
@@ -54,22 +54,18 @@ namespace opt {
         lbool operator()() override {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
-            obj_map<expr, rational> soft;
             reset();
-            lbool is_sat = find_mutexes(soft);
-            if (is_sat != l_true) {
-                return is_sat;
-            }
-            m_upper = m_lower;
+            if (init())
+                return l_undef;
+            
+            lbool is_sat = l_true;
+            
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
 
-            for (auto const& kv : soft) {
-                assert_weighted(wth(), kv.m_key, kv.m_value);
-                if (!is_true(kv.m_key)) {
-                    m_upper += kv.m_value;
-                }
-            }
+            for (auto const& [k, w, t] : m_soft) 
+                assert_weighted(wth(), k, w);
+            
             wth().init_min_cost(m_upper - m_lower);
             trace_bounds("wmax");
 
@@ -308,8 +304,8 @@ namespace opt {
                 
     };
 
-    maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
-        return alloc(wmax, c, ws, soft);
+    maxsmt_solver_base* mk_wmax(maxsat_context& c, vector<soft> & s) {
+        return alloc(wmax, c, s);
     }
 
 }
diff --git a/src/opt/wmax.h b/src/opt/wmax.h
index 6cc3ed46b..0a5167269 100644
--- a/src/opt/wmax.h
+++ b/src/opt/wmax.h
@@ -22,8 +22,8 @@ Notes:
 #include "opt/maxsmt.h"
 
 namespace opt {
-    maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_wmax(maxsat_context& c, vector<soft>& s);
 
-    maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector<soft>& s);
 
 }
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 116621dcc..045b92c99 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -312,6 +312,7 @@ namespace euf {
             }
         }
         else if (m.is_distinct(e)) {
+            // TODO - add lazy case for large values of sz.
             expr_ref_vector eqs(m);
             unsigned sz = n->num_args();
             for (unsigned i = 0; i < sz; ++i) {