diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 9421b26df..3c034ff0f 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -668,6 +668,27 @@ namespace datalog {
         return res;
     }
 
+    class relation_manager::default_relation_apply_sequential_fn : public relation_mutator_fn {
+        ptr_vector<relation_mutator_fn> m_mutators;
+    public:
+        default_relation_apply_sequential_fn(unsigned n, relation_mutator_fn ** mutators):
+            m_mutators(n, mutators) {            
+        }
+        virtual ~default_relation_apply_sequential_fn() {
+            std::for_each(m_mutators.begin(), m_mutators.end(), delete_proc<relation_mutator_fn>());
+        }
+        
+        virtual void operator()(relation_base& t) {
+            for (unsigned i = 0; i < m_mutators.size(); ++i) {
+                if (t.empty()) return;
+                (*(m_mutators[i]))(t);
+            }
+        }
+    };
+
+    relation_mutator_fn * relation_manager::mk_apply_sequential_fn(unsigned n, relation_mutator_fn ** mutators) {
+        return alloc(default_relation_apply_sequential_fn, n, mutators);
+    }
 
     class relation_manager::default_relation_join_project_fn : public relation_join_fn {
         scoped_ptr<relation_join_fn> m_join;
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index 2c148c5e6..be81a7afa 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -43,6 +43,7 @@ namespace datalog {
         class default_relation_select_equal_and_project_fn;
         class default_relation_intersection_filter_fn;
         class default_relation_filter_interpreted_and_project_fn;
+        class default_relation_apply_sequential_fn;
 
         class auxiliary_table_transformer_fn;
         class auxiliary_table_filter_fn;
@@ -352,9 +353,13 @@ namespace datalog {
 
         relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
 
+
         relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition,
             unsigned removed_col_cnt, const unsigned * removed_cols);
 
+        relation_mutator_fn * mk_apply_sequential_fn(unsigned n, relation_mutator_fn* * mutators);
+
+
         /**
             \brief Operations that returns all rows of \c t for which is column \c col equal to \c value
             with the column \c col removed.
diff --git a/src/muz/rel/product_set.cpp b/src/muz/rel/product_set.cpp
index 2812c56e2..a0c534934 100644
--- a/src/muz/rel/product_set.cpp
+++ b/src/muz/rel/product_set.cpp
@@ -26,10 +26,14 @@ namespace datalog {
 
     product_set::product_set(
         product_set_plugin& p, relation_signature const& s, 
-        bool is_empty, T const& t):
-        vector_relation(p, s, is_empty, t), m_refs(0) {
+        initial_t init, T const& t):
+        vector_relation(p, s, false, t), m_refs(0) {
         for (unsigned i = 0; i < s.size(); ++i) {
-            (*this)[i] = bit_vector(p.set_size(s[i]));
+            unsigned sz = p.set_size(s[i]);
+            (*this)[i].resize(sz);
+            if (init == FULL_t) {
+                (*this)[i].neg();
+            }
         }
     }
 
@@ -135,19 +139,43 @@ namespace datalog {
         }
     }
 
+    class product_set_plugin::filter_interpreted_fn : public relation_mutator_fn {
+        app_ref m_condition;
+    public:
+        filter_interpreted_fn(ast_manager& m, app* condition): m_condition(condition, m) {
+            
+        };
+        virtual ~filter_interpreted_fn() {}
+        
+        virtual void operator()(relation_base & _r) {
+            ast_manager& m = m_condition.get_manager();
+            if (m.is_false(m_condition)) {
+                _r.reset();
+                return;
+            }
+            if (m.is_true(m_condition)) {
+                return;
+            }
+            product_set_relation & r = get(_r);
+            product_set_plugin & p = r.get_plugin();
+            NOT_IMPLEMENTED_YET();
+        }
+    };
+
     void product_set_relation::add_fact(const relation_fact & f) {
         ast_manager& m = get_plugin().get_ast_manager(); 
         bv_util bv(m);
+        product_set* s = alloc(product_set, get_plugin(), get_signature(), product_set::EMPTY_t);
         rational v;
         unsigned bv_size;
-        product_set* s = alloc(product_set, get_plugin(), get_signature(), false);
+        // the bit-vector sets are empty at this point so they need to be primed.
         for (unsigned i = 0; i < f.size(); ++i) {
             VERIFY(bv.is_numeral(f[i], v, bv_size));
             SASSERT(v.is_unsigned());
             (*s)[i] = bit_vector(get_plugin().set_size(m.get_sort(f[i])));
             (*s)[i].set(v.get_unsigned(), true);
         }
-        s->display(std::cout << "fact");
+        // s->display(std::cout << "fact");
         if (m_elems.contains(s)) {
             dealloc(s);
         }
@@ -201,7 +229,9 @@ namespace datalog {
     // product_set_plugin
     
     product_set_plugin::product_set_plugin(relation_manager& rm):
-        relation_plugin(product_set_plugin::get_name(), rm) {
+        relation_plugin(product_set_plugin::get_name(), rm),
+        m(rm.get_context().get_manager()),
+        bv(m) {
     }
 
     bool product_set_plugin::can_handle_signature(const relation_signature & sig) {
@@ -226,15 +256,8 @@ namespace datalog {
     }
     relation_base * product_set_plugin::mk_full(func_decl* p, const relation_signature & sig) {
         product_set_relation* result = alloc(product_set_relation, *this, sig);
-        product_set* s = alloc(product_set, *this, sig, false);
+        product_set* s = alloc(product_set, *this, sig, product_set::FULL_t);
         s->inc_ref();
-        for (unsigned i = 0; i < sig.size(); ++i) {
-            bit_vector& t = (*s)[i];
-            t = bit_vector(set_size(sig[i]));
-            for (unsigned j = 0; j < t.size(); ++j) {
-                t.set(j, true);
-            }
-        }
         result->m_elems.insert(s);
         return result;
     }
@@ -248,7 +271,7 @@ namespace datalog {
         else {
             s->inc_ref();
             r->m_elems.insert(s);
-            s = alloc(product_set, *this, r->get_signature(), false);
+            s = alloc(product_set, *this, r->get_signature(), product_set::FULL_t);
         }
         return s;
     }
@@ -276,7 +299,7 @@ namespace datalog {
             product_set_plugin& p = r1.get_plugin();
             relation_signature const& sig = get_result_signature();
             product_set_relation * result = alloc(product_set_relation, p, sig);
-            product_set* s = alloc(product_set, p, sig, false);
+            product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
             product_sets::iterator it1 = r1.m_elems.begin(), end1 = r1.m_elems.end();
             for (; it1 != end1; ++it1) {
                 product_sets::iterator it2 = r2.m_elems.begin(), end2 = r2.m_elems.end();
@@ -310,7 +333,7 @@ namespace datalog {
             product_set_plugin& p = r.get_plugin();
             relation_signature const& sig = get_result_signature();
             product_set_relation* result = alloc(product_set_relation, p, sig);
-            product_set* s = alloc(product_set, p, sig, false);
+            product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
             product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
             for (; it != end; ++it) {
                 s->mk_project(*(*it), m_removed_cols.size(), m_removed_cols.c_ptr());
@@ -341,7 +364,7 @@ namespace datalog {
             product_set_plugin& p = r.get_plugin();
             relation_signature const& sig = get_result_signature();
             product_set_relation* result = alloc(product_set_relation, p, sig);
-            product_set* s = alloc(product_set, p, sig, false);
+            product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
             product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
             for (; it != end; ++it) {
                 s->mk_rename(*(*it), m_cycle.size(), m_cycle.c_ptr());
@@ -373,20 +396,24 @@ namespace datalog {
             product_set_relation& r = get(_r);
             product_set_relation const& src = get(_src);
             product_set_relation* d = get(_delta);
-            product_sets::iterator it = src.m_elems.begin(), end = src.m_elems.end();
-            for (; it != end; ++it) {
-                product_set* ps = *it;
-                if (!r.m_elems.contains(ps)) {
+            r.get_plugin().mk_union(r, src, d);
+        }
+    };
+    void product_set_plugin::mk_union(
+        product_set_relation& dst, product_set_relation const& src, product_set_relation* delta) {
+        product_sets::iterator it = src.m_elems.begin(), end = src.m_elems.end();
+        for (; it != end; ++it) {
+            product_set* ps = *it;
+            if (!dst.m_elems.contains(ps)) {
+                ps->inc_ref();
+                dst.m_elems.insert(ps);
+                if (delta) {
                     ps->inc_ref();
-                    r.m_elems.insert(ps);
-                    if (d) {
-                        ps->inc_ref();
-                        d->m_elems.insert(ps);
-                    }
+                    delta->m_elems.insert(ps);
                 }
             }
         }
-    };
+    }
     relation_union_fn * product_set_plugin::mk_union_fn(
         const relation_base & tgt, const relation_base & src, 
         const relation_base * delta) {
@@ -442,31 +469,13 @@ namespace datalog {
         return check_kind(t)?alloc(filter_identical_fn, col_cnt, identical_cols):0;
     }
 
-    class product_set_plugin::filter_equal_fn : public relation_mutator_fn {
-        unsigned   m_col;
-        bit_vector m_value;
+
+    class product_set_plugin::filter_mask_fn : public relation_mutator_fn {
+        unsigned   m_col;        
+        bit_vector m_mask;
     public:
-        filter_equal_fn(product_set_plugin& p, const relation_element & value, unsigned col, bool is_eq) 
-            : m_col(col) {
-            ast_manager& m = p.get_ast_manager();
-            // m.get_context().get_manager()
-            bv_util bv(m);
-            rational v;
-            unsigned bv_size;
-            unsigned sz = p.set_size(m.get_sort(value));
-            VERIFY(bv.is_numeral(value, v, bv_size));
-            SASSERT(v.is_unsigned());
-            unsigned w = v.get_unsigned();
-            SASSERT(w < sz);
-            m_value = bit_vector(sz);
-            if (is_eq) {
-                m_value.set(w, true);
-            }
-            else {
-                for (unsigned i = 0; i < sz; ++i) {
-                    m_value.set(i, i != w);
-                }
-            }
+        filter_mask_fn(product_set_plugin& p, bit_vector const& mask, unsigned col) 
+            : m_col(col), m_mask(mask) {
         }
 
         virtual void operator()(relation_base & _r) {
@@ -482,7 +491,7 @@ namespace datalog {
             for (unsigned i = 0; i < elems.size(); ++i) {
                 product_set* s = elems[i];
                 
-                if (s->mk_intersect(m_col, m_value)) {
+                if (s->mk_intersect(m_col, m_mask)) {
                     r.m_elems.insert(s);
                 }
                 else {
@@ -494,17 +503,246 @@ namespace datalog {
 
     relation_mutator_fn * product_set_plugin::mk_filter_equal_fn(const relation_base & r, 
         const relation_element & value, unsigned col) {
-        return check_kind(r)?alloc(filter_equal_fn, *this, value, col, true):0;
+        bit_vector mask;
+        expr* v = value;
+        extract_mask(1, &v, mask);
+        return check_kind(r)?alloc(filter_mask_fn, *this, mask, col):0;
     }
 
+    class product_set_plugin::filter_by_union_fn : public relation_mutator_fn {
+        ptr_vector<relation_mutator_fn> m_mutators;
+    public:
+        filter_by_union_fn(unsigned n, relation_mutator_fn ** mutators):
+            m_mutators(n, mutators) {            
+        }
+        virtual ~filter_by_union_fn() {
+            std::for_each(m_mutators.begin(), m_mutators.end(), delete_proc<relation_mutator_fn>());
+        }
+        
+        virtual void operator()(relation_base& _r) {
+            product_set_relation & r = get(_r);
+            product_set_plugin & p = r.get_plugin();
+
+            SASSERT(!m_mutators.empty());
+            if (m_mutators.size() == 1) {
+                (*(m_mutators[0]))(r);
+                return;
+            }
+            product_set_relation src(p, r.get_signature());
+            for (unsigned i = 1; i < m_mutators.size(); ++i) {
+                product_set_relation* r1 = r.clone();
+                (*(m_mutators[i]))(*r1);
+                p.mk_union(src, *r1, 0);
+                r1->deallocate();
+            }
+            (*(m_mutators[0]))(r);
+            p.mk_union(r, src, 0);
+        }
+    };
+
+    product_set_plugin::decomp_t product_set_plugin::decompose(
+        expr* condition, expr_ref_vector& args, unsigned& col) {
+        args.reset();
+        expr* e1, *e2;
+        app* value;
+        if (m.is_not(condition, e1) && m.is_not(e1, e2)) {
+            return decompose(e2, args, col);
+        }
+        if (m.is_not(condition, e1) && m.is_and(e1)) {
+            expr_ref tmp(m);
+            app* a = to_app(e1);
+            unsigned sz = a->get_num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                args.push_back(mk_not(a->get_arg(i)));
+            }
+            tmp = m.mk_or(args.size(), args.c_ptr());
+            return decompose(tmp, args, col);
+        }
+        if (m.is_not(condition, e1) && m.is_or(e1)) {
+            expr_ref tmp(m);
+            app* a = to_app(e1);
+            unsigned sz = a->get_num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                args.push_back(mk_not(a->get_arg(i)));
+            }
+            tmp = m.mk_and(args.size(), args.c_ptr());
+            return decompose(tmp, args, col);
+        }
+        if (m.is_and(condition)) {
+            app* a = to_app(condition);
+            unsigned sz = a->get_num_args();
+            args.append(sz, a->get_args());
+            return AND_d;
+        }
+        if (is_setof(condition, args, col)) {
+            return SET_d;
+        }
+        if (m.is_or(condition)) {
+            app* a = to_app(condition);
+            unsigned sz = a->get_num_args();
+            args.append(sz, a->get_args());
+            return OR_d;
+        }
+        if (is_value_ne(condition, value, col)) {
+            args.push_back(value);
+            return NE_d;
+        }
+        if (is_value_eq(condition, value, col)) {
+            args.push_back(value);
+            return EQ_d;
+        }
+        if (m.is_not(condition, e1) && m.is_true(e1)) {
+            return F_d;
+        }
+        if (m.is_false(condition)) {
+            return F_d;
+        }
+        if (m.is_not(condition, e1) && m.is_false(e1)) {
+            return T_d;
+        }
+        if (m.is_true(condition)) {
+            return T_d;
+        }
+        return UNHANDLED_d;
+    }
+
+    bool product_set_plugin::mk_filter_interpreted(
+        const relation_base & t, expr_ref_vector const& args,
+        ptr_vector<relation_mutator_fn>& mutators) {
+        unsigned sz = args.size();
+        
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* arg = args[i];
+            if (!is_app(arg)) {
+                break;
+            }
+            relation_mutator_fn* mut = mk_filter_interpreted_fn(t, to_app(arg));
+            if (!mut) {
+                break;
+            }
+            mutators.push_back(mut);
+        }
+        if (mutators.size() < sz) {
+            std::for_each(mutators.begin(), mutators.end(), delete_proc<relation_mutator_fn>());
+            return false;
+        }
+        else {
+            return true;
+        }        
+    }
     relation_mutator_fn * product_set_plugin::mk_filter_interpreted_fn(
         const relation_base & t, app * condition) {
-        ast_manager& m =get_manager().get_context().get_manager();
-        std::cout << "filter interpreted '" << mk_pp(condition, m) << "'\n";            
-        NOT_IMPLEMENTED_YET();
+        if (!check_kind(t)) return 0;
+        unsigned col;
+        ptr_vector<relation_mutator_fn> mutators;
+        expr_ref_vector args(m);
+        std::cout << mk_pp(condition, m) << "\n";
+        bit_vector mask;
+        switch (decompose(condition, args, col)) {
+        case NE_d:
+            SASSERT(args.size() == 1);
+            extract_mask(1, args.c_ptr(), mask);            
+            mask.neg();
+            return alloc(filter_mask_fn, *this, mask, col);
+        case EQ_d:
+            SASSERT(args.size() == 1);
+            extract_mask(1, args.c_ptr(), mask);            
+            return alloc(filter_mask_fn, *this, mask, col);
+        case AND_d: 
+            if (!mk_filter_interpreted(t, args, mutators)) {
+                return 0;
+            } 
+            return get_manager().mk_apply_sequential_fn(mutators.size(), mutators.c_ptr());
+        case OR_d: 
+            if (!mk_filter_interpreted(t, args, mutators)) {
+                return 0;
+            } 
+            return alloc(filter_by_union_fn, mutators.size(), mutators.c_ptr());
+        case F_d:
+            return alloc(filter_interpreted_fn, m, m.mk_false());
+        case T_d:
+            return alloc(filter_interpreted_fn, m, m.mk_true());
+        case SET_d:
+            extract_mask(args.size(), args.c_ptr(), mask);
+            return alloc(filter_mask_fn, *this, mask, col);
+        case UNHANDLED_d:
+            std::cout << "filter interpreted unhandled '" << mk_pp(condition, m) << "'\n";            
+            NOT_IMPLEMENTED_YET();
+            return 0;
+        default:
+            UNREACHABLE();
+        }
         return 0;
     }
 
+    void product_set_plugin::extract_mask(unsigned n, expr* const* values, bit_vector& mask) {
+        SASSERT(n > 0);
+        unsigned sz = set_size(m.get_sort(values[0]));
+        mask.resize(sz, false);
+        rational v;
+        unsigned bv_size;
+        for (unsigned i = 0; i < n; ++i) {
+            expr* value = values[i];
+            VERIFY(bv.is_numeral(value, v, bv_size));
+            SASSERT(v.is_unsigned());
+            unsigned w = v.get_unsigned();
+            SASSERT(w < sz);
+            mask.set(w, true);
+        }
+    }
+
+    bool product_set_plugin::is_setof(expr* condition, expr_ref_vector& values, unsigned & col) {
+        if (!m.is_or(condition)) return false;
+        unsigned sz = to_app(condition)->get_num_args();
+        col = UINT_MAX;
+        unsigned col1;
+        if (sz == 0) return false;
+        values.reset();
+        app* value;
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* arg = to_app(condition)->get_arg(i);
+            if (is_value_eq(arg, value, col1)) {
+                if (col == UINT_MAX) {
+                    col = col1;
+                    values.push_back(value);
+                }
+                else if (col != col1) {
+                    return false;
+                }
+                else {
+                    values.push_back(value);
+                }
+            }
+        }
+        return true;
+    }
+
+    bool product_set_plugin::is_value_eq(expr* e, app*& value, unsigned& col) {
+        expr* e1, *e2;
+        rational val;
+        unsigned bv_size;
+        if (!m.is_eq(e, e1, e2)) return false;
+        if (!is_var(e1)) {
+            std::swap(e1, e2);
+        }
+        if (!is_var(e1)) return false;
+        if (!bv.is_numeral(e2, val, bv_size)) return false;
+        if (!val.is_unsigned()) return false;
+        value = to_app(e2);
+        col = to_var(e1)->get_idx();
+        return true;
+    }
+
+    bool product_set_plugin::is_value_ne(expr* condition, relation_element& value, unsigned& col) {
+        expr* e;
+        if (m.is_not(condition, e)) {
+            return is_value_eq(e, value, col);
+        }
+        else {
+            return false;
+        }
+    }
+
 
 };
 
diff --git a/src/muz/rel/product_set.h b/src/muz/rel/product_set.h
index 670ec1cbf..c099e579a 100644
--- a/src/muz/rel/product_set.h
+++ b/src/muz/rel/product_set.h
@@ -40,7 +40,11 @@ namespace datalog {
         typedef bit_vector T;
         unsigned m_refs;
     public:
-        product_set(product_set_plugin& p, relation_signature const& s, bool is_empty, T const& t = T());
+        enum initial_t {
+            EMPTY_t,
+            FULL_t
+        };
+        product_set(product_set_plugin& p, relation_signature const& s, initial_t init, T const& t = T());
        
         virtual ~product_set() {}
         unsigned get_hash() const;
@@ -146,10 +150,13 @@ namespace datalog {
         class project_fn;
         class union_fn;
         class rename_fn;
-        class filter_equal_fn;
+        class filter_mask_fn;
         class filter_identical_fn;
         class filter_interpreted_fn;
         class filter_by_negation_fn;        
+        class filter_by_union_fn;
+        ast_manager& m;
+        bv_util bv;
 
     public:        
         product_set_plugin(relation_manager& rm);
@@ -180,6 +187,29 @@ namespace datalog {
         static product_set_relation* get(relation_base* r);
         static product_set_relation const & get(relation_base const& r);   
         product_set* insert(product_set* s, product_set_relation* r);
+
+        enum decomp_t {
+            AND_d,    // conjunction
+            OR_d,     // disjunction 
+            EQ_d,     // value = col
+            NE_d,     // value != col
+            F_d,      // false
+            T_d,      // true
+            SET_d,    // disjunction value_i = col
+            UNHANDLED_d            
+        };
+
+        decomp_t decompose(expr* condition, expr_ref_vector& args, unsigned& col);
+
+        bool is_value_ne(expr* condition, relation_element& value, unsigned& col);
+        bool is_value_eq(expr* condition, relation_element& value, unsigned& col);
+        bool is_setof(expr* condition, expr_ref_vector& values, unsigned& col);
+        expr* mk_not(expr* e) { return m.is_not(e,e)?e:m.mk_not(e); }
+        void mk_union(product_set_relation& dst, product_set_relation const& src, product_set_relation* delta);
+        void extract_mask(unsigned sz, expr* const* values, bit_vector& mask);
+        bool mk_filter_interpreted(
+            const relation_base & t, expr_ref_vector const& args,
+            ptr_vector<relation_mutator_fn>& mutators);
     };
 
 };
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index fbc2a8796..86c3fba11 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -3,15 +3,12 @@ def_module_params('opt',
                   export=True,
                   params=(('timeout', UINT, UINT_MAX, 'set timeout'),
                           ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
-	                  ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'hsmax'"),
+	                  ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('print_model', BOOL, False, 'display model for satisfiable constraints'),
-                          ('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'),
-                          ('debug_conflict', BOOL, False, 'debug conflict resolution'),
                           ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
                           ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
-                          ('sls_engine', SYMBOL, 'pb', "SLS engine. Either 'bv' or 'pb'"),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')
 
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index b33c9420c..b6c7390e5 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -71,18 +71,19 @@ namespace sat {
             literal lit = core.back();
             core.pop_back();
             unsigned sz = mus.size();
-            // mus.push_back(~lit); // TBD: measure
             mus.append(core);
+            mus.push_back(~lit); // TBD: measure
             lbool is_sat = s.check(mus.size(), mus.c_ptr());
             TRACE("sat", tout << "mus: " << mus << "\n";);
-            mus.resize(sz);
             switch (is_sat) {
             case l_undef:
+                mus.resize(sz);
                 core.push_back(lit);
                 set_core();
                 return l_undef;
             case l_true: {
                 SASSERT(value_at(lit, s.get_model()) == l_false);
+                mus.resize(sz);
                 mus.push_back(lit);
                 if (!core.empty()) {
                     // mr(); // TBD: measure
@@ -92,8 +93,18 @@ namespace sat {
             case l_false:
                 literal_vector const& new_core = s.get_core();
                 if (new_core.contains(~lit)) {
+                    mus.resize(sz);
                     break;
+#if 0
+                    mus.pop_back();
+                    is_sat = s.check(mus.size(), mus.c_ptr());
+                    SASSERT(is_sat != l_true);
+                    if (is_sat != l_false) {
+                        return l_undef;
+                    }
+#endif 
                 }
+                mus.resize(sz);
                 TRACE("sat", tout << "new core: " << new_core << "\n";);
                 core.reset();
                 for (unsigned i = 0; i < new_core.size(); ++i) {
@@ -102,7 +113,6 @@ namespace sat {
                         core.push_back(lit);
                     }
                 }
-                IF_VERBOSE(2, verbose_stream() << "reduced core: " << core.size() << "\n";);
                 break;
             }
         }
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index c0c385210..b8cbdade2 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -228,6 +228,14 @@ unsigned bit_vector::get_hash() const {
     return string_hash(reinterpret_cast<char const* const>(m_data), size()/8,  0);
 }
 
+bit_vector& bit_vector::neg() {
+    unsigned n = num_words();
+    for (unsigned i = 0; i < n; ++i) {
+        m_data[i] = ~m_data[i];
+    }
+    return *this;
+}
+
 void fr_bit_vector::reset() {
     unsigned sz = size();
     unsigned_vector::const_iterator it  = m_one_idxs.begin();
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 6ec2c18ee..6bfccd914 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -200,6 +200,8 @@ public:
     bit_vector & operator|=(bit_vector const & source);
 
     bit_vector & operator&=(bit_vector const & source);
+
+    bit_vector & neg();
     
     void display(std::ostream & out) const;