diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index f5cac29e5..7cb1c6241 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -53,7 +53,6 @@ void rule_properties::collect(rule_set const& rules) {
 
 void rule_properties::check_quantifier_free() {
     if (!m_quantifiers.empty()) {
-        quantifier* q = m_quantifiers.begin()->m_key;
         rule* r = m_quantifiers.begin()->m_value;
         std::stringstream stm;
         stm << "cannot process quantifier in rule ";
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index 14f4a2b75..6545d4282 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -54,7 +54,6 @@ namespace datalog {
 
         typedef ptr_hashtable<ddnf_node, ddnf_node::hash, ddnf_node::eq> ddnf_nodes;
     private:
-        ddnf_mgr&             m;
         tbv_manager&          tbvm;
         tbv const&            m_tbv;
         ddnf_node_vector      m_children;
@@ -68,7 +67,6 @@ namespace datalog {
 
     public:
         ddnf_node(ddnf_mgr& m, tbv_manager& tbvm, tbv const& tbv, unsigned id):
-            m(m),
             tbvm(tbvm),
             m_tbv(tbv),
             m_children(m),
@@ -130,7 +128,6 @@ namespace datalog {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
 
-        unsigned               m_num_bits;
         ddnf_node*             m_root;
         ddnf_node_vector       m_noderefs;
         bool                   m_internalized;
@@ -141,7 +138,7 @@ namespace datalog {
         svector<bool>          m_marked;
         stats                  m_stats;
     public:
-        ddnf_mgr(unsigned n): m_num_bits(n), m_noderefs(*this), m_internalized(false), m_tbv(n),
+        ddnf_mgr(unsigned n): m_noderefs(*this), m_internalized(false), m_tbv(n),
                               m_hash(m_tbv), m_eq(m_tbv),
                               m_nodes(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) {
             tbv* bX = m_tbv.allocateX();
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 3b7d5c056..30509d6bf 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -80,7 +80,7 @@ namespace pdr {
     pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): 
         pm(pm), m(pm.get_manager()),
         ctx(ctx), m_head(head, m), 
-        m_sig(m), m_solver(pm, ctx.get_params().pdr_try_minimize_core(), head->get_name()),
+        m_sig(m), m_solver(pm, head->get_name()),
         m_invariants(m), m_transition(m), m_initial_state(m), 
         m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().pdr_cache_mode()) {}
 
@@ -1137,9 +1137,9 @@ namespace pdr {
             if (n->get_model_ptr()) {
                 models.insert(n->state(), n->get_model_ptr());
                 rules.insert(n->state(), n->get_rule());
-                pred_transformer& pt = n->pt();
-                context& ctx = pt.get_context();
-                datalog::context& dctx = ctx.get_context();
+                //pred_transformer& pt = n->pt();
+                //context& ctx = pt.get_context();
+                //datalog::context& dctx = ctx.get_context();
             }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp
index a7d0a02bf..9ba976254 100644
--- a/src/muz/pdr/pdr_prop_solver.cpp
+++ b/src/muz/pdr/pdr_prop_solver.cpp
@@ -225,12 +225,11 @@ namespace pdr {
     };
 
 
-    prop_solver::prop_solver(manager& pm, bool try_minimize_core, symbol const& name) :
+    prop_solver::prop_solver(manager& pm, symbol const& name) :
         m_fparams(pm.get_fparams()),
         m(pm.get_manager()),
         m_pm(pm),
         m_name(name),
-        m_try_minimize_core(try_minimize_core),
         m_ctx(pm.mk_fresh()),
         m_pos_level_atoms(m),
         m_neg_level_atoms(m),
diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h
index d7f13a603..a44ac7e5a 100644
--- a/src/muz/pdr/pdr_prop_solver.h
+++ b/src/muz/pdr/pdr_prop_solver.h
@@ -40,7 +40,6 @@ namespace pdr {
         ast_manager&        m;
         manager&            m_pm;
         symbol              m_name;
-        bool                m_try_minimize_core;
         scoped_ptr<pdr::smt_context> m_ctx;
         decl_vector         m_level_preds;      
         app_ref_vector      m_pos_level_atoms;  // atoms used to identify level
@@ -74,7 +73,7 @@ namespace pdr {
         
         
     public:
-        prop_solver(pdr::manager& pm, bool try_minimize_core, symbol const& name);
+        prop_solver(pdr::manager& pm, symbol const& name);
         
         /** return true is s is a symbol introduced by prop_solver */
         bool is_aux_symbol(func_decl * s) const { 
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index c1b840c61..20364d5d5 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -297,7 +297,6 @@ namespace datalog {
         relation_base const& t1, relation_base const& t2, relation_base const& t,
         unsigned_vector const& cols1, unsigned_vector const& cols2, unsigned_vector const& rm_cols) {
         ast_manager& m = get_ast_manager();
-        relation_signature const& sig2 = t.get_signature();
         relation_signature const& sigA = t1.get_signature();
         relation_signature const& sigB = t2.get_signature();
         relation_signature sig1;
@@ -383,7 +382,6 @@ namespace datalog {
     void check_relation_plugin::verify_join(
         relation_base const& t1, relation_base const& t2, relation_base const& t,
         unsigned_vector const& cols1, unsigned_vector const& cols2) {
-        ast_manager& m = get_ast_manager();
         expr_ref fml1 = ground(t, mk_join(t1, t2, cols1, cols2));
         expr_ref fml2 = ground(t);
         check_equiv("join", fml1, fml2);
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index a27d20c56..e73395bc9 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -214,7 +214,7 @@ bool doc_manager::merge(
     subset_ints const& equalities, bit_vector const& discard_cols) {
     for (unsigned i = 0; i < length; ++i) {
         unsigned idx = lo + i;
-        if (!merge(d, lo + i, equalities, discard_cols)) return false;
+        if (!merge(d, idx, equalities, discard_cols)) return false;
     }
     return true;
 }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index ca5af005b..6ffefaf88 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -238,7 +238,6 @@ public:
     }
     void subtract(M& m, T& t) {
         unsigned sz = size();
-        bool found = false;
         union_bvec result;
         for (unsigned i = 0; i < sz; ++i) {
             m.subtract(*m_elems[i], t, result.m_elems);
diff --git a/src/muz/rel/product_set.cpp b/src/muz/rel/product_set.cpp
deleted file mode 100644
index 9c26ed189..000000000
--- a/src/muz/rel/product_set.cpp
+++ /dev/null
@@ -1,788 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    product_set.cpp
-
-Abstract:
-
-    Product set.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-08-23
-
-Revision History:
-
---*/
-
-#include "product_set.h"
-#include "bv_decl_plugin.h"
-#include "dl_relation_manager.h"
-#include "bool_rewriter.h"
-
-namespace datalog {
-
-    static unsigned s_ps_num_bits = 0;
-    static unsigned s_num_ps = 0;
-
-    product_set::product_set(
-        product_set_plugin& p, relation_signature const& s, 
-        initial_t init, T const& t):
-        vector_relation<bit_vector>(p, s, false, t), m_refs(0) {
-        unsigned delta = 0;
-        for (unsigned i = 0; i < s.size(); ++i) {
-            unsigned sz = p.set_size(s[i]);
-            (*this)[i].resize(sz);
-            if (init == FULL_t) {
-                (*this)[i].neg();
-            }
-            delta += sz;
-        }
-        s_ps_num_bits += delta;
-        s_num_ps ++;
-        if ((s_num_ps % 1000) == 0) {
-            std::cout << s_num_ps << " " << s_ps_num_bits << " " << delta << "\n";
-        }
-    }
-
-    product_set::~product_set() {
-        relation_signature const& s = get_signature();
-        product_set_plugin& p = dynamic_cast<product_set_plugin&>(get_plugin());
-        for (unsigned i = 0; i < s.size(); ++i) {
-            unsigned sz = p.set_size(s[i]);
-            s_ps_num_bits -= sz;
-        }        
-        --s_num_ps;
-    }
-
-    unsigned product_set::get_hash() const {
-        unsigned hash = 0;
-        for (unsigned i = 0; i < get_signature().size(); ++i) {
-            hash ^= (*this)[i].get_hash();
-        }
-        return hash;
-    }
-
-    bool product_set::operator==(product_set const& p) const {
-        for (unsigned i = 0; i < get_signature().size(); ++i) {
-            if ((*this)[i] != p[i]) return false;
-        }
-        return true;            
-    }
-    bool product_set::contains(product_set const& p) const {
-        for (unsigned i = 0; i < get_signature().size(); ++i) {
-            if ((*this)[i].contains(p[i])) return false;
-        }
-        return true;            
-    }
-    void product_set::reset() {        
-        for (unsigned i = 0; i < get_signature().size(); ++i) {
-            (*this)[i].fill0();
-        }        
-    }
-    void product_set::add_fact(const relation_fact & f) {
-        UNREACHABLE();
-    }
-    bool product_set::contains_fact(const relation_fact & f) const {
-        UNREACHABLE();
-        return false;
-    }
-    relation_base * product_set::clone() const {
-        product_set* result = alloc(product_set, dynamic_cast<product_set_plugin&>(get_plugin()), get_signature(), EMPTY_t);
-        result->copy(*this);
-        return result;
-    }
-    relation_base * product_set::complement(func_decl*) const {
-        product_set* result = alloc(product_set, dynamic_cast<product_set_plugin&>(get_plugin()), get_signature(), EMPTY_t);
-        result->copy(*this);
-        result->complement();
-        return result;
-    }
-
-    void product_set::complement() {
-        for (unsigned i = 0; i < get_signature().size(); ++i) {
-            (*this)[i].neg();
-        }        
-    }
-    void product_set::to_formula(expr_ref& fml) const {
-        ast_manager& m = fml.get_manager();
-        bv_util bv(m);
-        expr_ref_vector conjs(m), disjs(m);
-        relation_signature const& sig = get_signature();
-        if (m_empty) {
-            fml = m.mk_false();
-            return;
-        }
-        for (unsigned i = 0; i < sig.size(); ++i) {
-            sort* ty = sig[i];
-            expr_ref var(m.mk_var(i, ty), m);
-            unsigned j = find(i);
-            if (i != j) {
-                conjs.push_back(m.mk_eq(var, m.mk_var(j, sig[j])));
-                continue;
-            }            
-            T const& t = (*this)[i];
-            disjs.reset();
-            for (j = 0; j < t.size(); ++j) {
-                if (t.get(j)) {
-                    disjs.push_back(m.mk_eq(var, bv.mk_numeral(rational(j), ty)));
-                }
-            }
-            if (disjs.empty()) {
-                UNREACHABLE();
-                fml = m.mk_false();
-                return;
-            }
-            if (disjs.size() == 1) {
-                conjs.push_back(disjs[0].get());
-            }
-            else {
-                conjs.push_back(m.mk_or(disjs.size(), disjs.c_ptr()));
-            }
-        }
-        bool_rewriter br(m);
-        br.mk_and(conjs.size(), conjs.c_ptr(), fml);
-    }    
-    void product_set::display_index(unsigned i, const T& t, std::ostream& out) const {
-        out << i << ":";
-        t.display(out);
-    }
-    bool product_set::mk_intersect(unsigned idx, T const& t) {
-        if (!m_empty) {
-            (*this)[idx] &= t;
-            m_empty = is_empty(idx, (*this)[idx]);
-        }
-        return !m_empty;
-    }
-
-    // product_set_relation
-
-
-    product_set_relation::product_set_relation(product_set_plugin& p, relation_signature const& s):
-        relation_base(p, s) {
-    }
-
-    product_set_relation::~product_set_relation() {
-        reset();
-    }
-
-    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)) {
-                product_set_relation & r = get(_r);
-                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;
-        // 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].set(v.get_unsigned(), true);
-        }
-        // s->display(std::cout << "fact");
-        if (m_elems.contains(s)) {
-            dealloc(s);
-        }
-        else {
-            s->inc_ref();
-            m_elems.insert(s);
-        }
-
-    }
-    bool product_set_relation::contains_fact(const relation_fact & f) const {
-        std::cout << "contains fact\n";
-        NOT_IMPLEMENTED_YET();
-        return false;
-    }
-    product_set_relation * product_set_relation::clone() const {
-        product_set_relation* r = alloc(product_set_relation, get_plugin(), get_signature());
-        product_sets::iterator it = m_elems.begin(), end = m_elems.end();
-        for (; it != end; ++it) {
-            product_set* ps = dynamic_cast<product_set*>((*it)->clone());
-            ps->inc_ref();
-            r->m_elems.insert(ps);
-        }
-        return r;
-    }
-    void product_set_relation::reset() {
-        product_sets::iterator it = m_elems.begin(), end = m_elems.end();
-        for (; it != end; ++it) {
-            (*it)->dec_ref();
-        }
-        m_elems.reset();
-    }
-    product_set_relation * product_set_relation::complement(func_decl*) const {
-        std::cout << "complement\n";
-        NOT_IMPLEMENTED_YET();
-        return 0;
-    }
-    void product_set_relation::to_formula(expr_ref& fml) const {
-        product_sets::iterator it = m_elems.begin(), end = m_elems.end();
-        ast_manager& m = get_plugin().get_manager().get_context().get_manager();
-        expr_ref_vector disjs(m);
-        for (; it != end; ++it) {
-            (*it)->to_formula(fml);
-            disjs.push_back(fml);
-        }
-        fml = m.mk_or(disjs.size(), disjs.c_ptr());
-    }
-    product_set_plugin& product_set_relation::get_plugin() const {
-        return static_cast<product_set_plugin&>(relation_base::get_plugin());
-    }
-
-    void product_set_relation::display(std::ostream& out) const {
-        product_sets::iterator it = m_elems.begin(), end = m_elems.end();
-        for (; it != end; ++it) {
-            (*it)->display(out);
-        }
-    }
-    
-    // product_set_plugin
-    
-    product_set_plugin::product_set_plugin(relation_manager& 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) {
-        bv_util bv(get_manager().get_context().get_manager());
-        for (unsigned i = 0; i < sig.size(); ++i) {
-            if (!bv.is_bv_sort(sig[i])) return false;
-        }
-        return true;
-    }
-
-    product_set_relation& product_set_plugin::get(relation_base& r) {
-        return dynamic_cast<product_set_relation&>(r);
-    }
-    product_set_relation* product_set_plugin::get(relation_base* r) {
-        return r?dynamic_cast<product_set_relation*>(r):0;
-    }
-    product_set_relation const & product_set_plugin::get(relation_base const& r) {
-        return dynamic_cast<product_set_relation const&>(r);        
-    }
-    relation_base * product_set_plugin::mk_empty(const relation_signature & s) {
-        return alloc(product_set_relation, *this, s);
-    }
-    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, product_set::FULL_t);
-        s->inc_ref();
-        result->m_elems.insert(s);
-        return result;
-    }
-    product_set* product_set_plugin::insert(product_set* s, product_set_relation* r) {
-        if (s->empty()) {
-            s->reset();
-            s->complement();
-        }
-        else if (r->m_elems.contains(s)) {
-            s->reset();
-            s->complement();
-        }
-        else {
-            s->inc_ref();
-            r->m_elems.insert(s);
-            s = alloc(product_set, *this, r->get_signature(), product_set::FULL_t);
-        }
-        return s;
-    }
-
-    unsigned product_set_plugin::set_size(sort* ty) {
-        bv_util bv(get_ast_manager());
-        unsigned bv_size = bv.get_bv_size(ty);
-        SASSERT(bv_size <= 16);
-        if (bv_size > 16) {
-            throw default_exception("bit-vector based sets are not suitable for this domain size");
-        }
-        return 1 << bv_size;
-    }
-
-    class product_set_plugin::join_fn : public convenient_relation_join_fn {
-    public:
-        join_fn(const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt,
-                const unsigned * cols1, const unsigned * cols2) 
-            : convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2){
-        }
-
-        virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {
-            product_set_relation const& r1 = get(_r1);
-            product_set_relation const& r2 = get(_r2);
-            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, 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();
-                for (; it2 != end2; ++it2) {
-                    s->mk_join(*(*it1), *(*it2), m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr());
-                    s = p.insert(s, result);
-                }
-            }
-            dealloc(s);
-            std::cout << "join " << result->m_elems.size() << "\n";
-            return result;
-        }
-    };
-    relation_join_fn * product_set_plugin::mk_join_fn(
-        const relation_base & r1, const relation_base & r2,
-        unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
-        if (!check_kind(r1) || !check_kind(r2)) {
-            return 0;
-        }
-        return alloc(join_fn, r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2);
-    }
-
-    class product_set_plugin::project_fn : public convenient_relation_project_fn {
-    public:
-        project_fn(const relation_signature & orig_sig, unsigned removed_col_cnt, 
-                   const unsigned * removed_cols) 
-            : convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols) {
-        }
-
-        virtual relation_base * operator()(const relation_base & _r) {
-            product_set_relation const& r = get(_r);
-            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, 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());
-                s = p.insert(s, result);
-            }
-            dealloc(s);
-            return result;
-        }
-    };
-    relation_transformer_fn * product_set_plugin::mk_project_fn(
-        const relation_base & r, unsigned col_cnt, 
-        const unsigned * removed_cols) {
-        if (check_kind(r)) {
-            return alloc(project_fn, r.get_signature(), col_cnt, removed_cols);
-        }
-        else {
-            return 0;
-        }
-    }
-    class product_set_plugin::rename_fn : public convenient_relation_rename_fn {
-    public:
-        rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 
-            : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {
-        }
-
-        virtual relation_base * operator()(const relation_base & _r) {
-            product_set_relation const& r = get(_r);
-            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, 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());
-                s = p.insert(s, result);
-            }
-            dealloc(s);
-            return result;
-        }
-    };
-
-    relation_transformer_fn * product_set_plugin::mk_rename_fn(const relation_base & r, 
-            unsigned cycle_len, const unsigned * permutation_cycle) {
-        if (check_kind(r)) {
-            return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle);
-        }
-        else {
-            return 0;
-        }
-    }
-
-    class product_set_plugin::union_fn : public relation_union_fn {
-    public:
-        union_fn() {}
-
-        virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
-
-            TRACE("dl", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
-
-            product_set_relation& r = get(_r);
-            product_set_relation const& src = get(_src);
-            product_set_relation* d = get(_delta);
-            r.get_plugin().mk_union(r, src, d);
-            std::cout << "union: " << r.m_elems.size() << "\n";
-        }
-    };
-    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();
-                    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) {
-        if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
-            return 0;
-        }
-        return alloc(union_fn);
-    }
-    relation_union_fn * product_set_plugin::mk_widen_fn(
-        const relation_base & tgt, const relation_base & src, 
-        const relation_base * delta) {
-        return mk_union_fn(tgt, src, delta);
-    }
-
-
-    class product_set_plugin::filter_identical_fn : public relation_mutator_fn {
-        unsigned_vector m_identical_cols;
-    public:
-        filter_identical_fn(unsigned col_cnt, const unsigned * identical_cols) 
-            : m_identical_cols(col_cnt, identical_cols) {}
-
-        virtual void operator()(relation_base & _r) {
-            product_set_relation & r = get(_r);
-            product_set_plugin& p = r.get_plugin();
-            ptr_vector<product_set> elems;
-            product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
-            for (; it != end; ++it) {
-                elems.push_back(*it);
-            }
-            r.m_elems.reset();
-            for (unsigned i = 0; i < elems.size(); ++i) {
-                product_set* s = elems[i];
-                if (equate(*s)) {
-                    r.m_elems.insert(s);
-                }
-                else {
-                    s->dec_ref();
-                }                
-            }
-        }
-    private:
-        bool equate(product_set& dst) {
-            for (unsigned i = 1; !dst.empty() && i < m_identical_cols.size(); ++i) {
-                unsigned c1 = m_identical_cols[0];
-                unsigned c2 = m_identical_cols[i];
-                dst.equate(c1, c2);
-            }
-            return !dst.empty();
-        }
-    };
-    relation_mutator_fn * product_set_plugin::mk_filter_identical_fn(
-        const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) {
-        return check_kind(t)?alloc(filter_identical_fn, col_cnt, identical_cols):0;
-    }
-
-
-    class product_set_plugin::filter_mask_fn : public relation_mutator_fn {
-        unsigned   m_col;        
-        bit_vector m_mask;
-    public:
-        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) {
-            product_set_relation & r = get(_r);
-            product_set_plugin & p = r.get_plugin();
-
-            ptr_vector<product_set> elems;
-            product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
-            for (; it != end; ++it) {
-                elems.push_back(*it);
-            }
-            r.m_elems.reset();
-            for (unsigned i = 0; i < elems.size(); ++i) {
-                product_set* s = elems[i];
-                
-                if (s->mk_intersect(m_col, m_mask)) {
-                    r.m_elems.insert(s);
-                }
-                else {
-                    s->dec_ref();
-                }                
-            }            
-        }
-    };
-
-    relation_mutator_fn * product_set_plugin::mk_filter_equal_fn(const relation_base & r, 
-        const relation_element & value, unsigned col) {
-        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)) {
-            SASSERT(!args.empty());
-            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) {
-        if (!check_kind(t)) return 0;
-        unsigned col;
-        ptr_vector<relation_mutator_fn> mutators;
-        expr_ref_vector args(m);
-        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);
-                }
-            }
-            else {
-                return false;
-            }
-        }
-        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
deleted file mode 100644
index 238a33d8a..000000000
--- a/src/muz/rel/product_set.h
+++ /dev/null
@@ -1,284 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    product_set.h
-
-Abstract:
-
-    Product set relation.
-    A product set is a tuple of sets.
-    The meaning of a product set is the set of
-    elements in the cross-product.
-    A product set relation is a set of product sets, 
-    and the meaning of this relation is the union of
-    all elements from the products. 
-    It is to be used when computing over product sets is
-    (much) cheaper than over the space of tuples.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-08-23
-
-Revision History:
-
---*/
-#ifndef _DL_PRODUCT_SET__H_
-#define _DL_PRODUCT_SET__H_
-
-#include "util.h"
-#include "bit_vector.h"
-#include "dl_base.h"
-#include "dl_vector_relation.h"
-
-namespace datalog {
-
-    class product_set_plugin;
-
-    class product_set : public vector_relation<bit_vector> {
-        typedef bit_vector T;
-        unsigned m_refs;
-    public:
-        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;
-        bool operator==(product_set const& p) const;
-        bool contains(product_set const& p) const;
-
-        void inc_ref() { ++m_refs; }
-        void dec_ref() { --m_refs; if (0 == m_refs) dealloc(this); }
-        unsigned ref_count() const { return m_refs; }
-
-        struct eq {
-            bool operator()(product_set const* s1, product_set const* s2) const {
-                return *s1 == *s2;
-            }
-        };
-
-        struct hash {
-            unsigned operator()(product_set const* s) const {
-                return s->get_hash();
-            }
-        };
-
-        virtual void add_fact(const relation_fact & f);
-        virtual bool contains_fact(const relation_fact & f) const;
-        virtual relation_base * clone() const;
-        virtual relation_base * complement(func_decl*) const;
-        virtual void reset();
-        virtual void to_formula(expr_ref& fml) const;
-
-        bool mk_intersect(unsigned idx, T const& t);
-        void complement();
-
-    private:
-        virtual void display_index(unsigned i, const T&, std::ostream& out) const;
-        virtual T mk_intersect(T const& t1, T const& t2, bool& _is_empty) const {
-            T result(t1);
-            result &= t2;
-            _is_empty = is_empty(0, result);
-            return result;
-        }
-
-        virtual T mk_widen(T const& t1, T const& t2) const {
-            UNREACHABLE();
-            return t1;
-        }
-
-        virtual T mk_unite(T const& t1, T const& t2) const {
-            UNREACHABLE();
-            return t1;
-        }
-
-        virtual bool is_subset_of(T const& t1, T const& t2) const {
-            return t2.contains(t1);
-        }
-
-        virtual bool is_full(T const& t) const {
-            for (unsigned j = 0; j < t.size(); ++j) {
-                if (!t.get(j)) return false;
-            }
-            return true;
-        }
-
-        virtual bool is_empty(unsigned i, T const& t) const {
-            for (unsigned j = 0; j < t.size(); ++j) {
-                if (t.get(j)) return false;
-            }
-            return true;
-        }
-
-        virtual void mk_rename_elem(T& t, unsigned col_cnt, unsigned const* cycle) {
-            // no-op.
-        }
-
-        virtual T mk_eq(union_find<> const& old_eqs, union_find<> const& neq_eqs, T const& t) const { 
-            UNREACHABLE();
-            return t; 
-        }
-    };
-
-
-    typedef ptr_hashtable<product_set, product_set::hash, product_set::eq> product_sets;
-
-    class product_set_relation : public relation_base {
-        friend class product_set_plugin;
-        product_sets m_elems;
-    public:
-        product_set_relation(product_set_plugin& p, relation_signature const& s);
-        virtual ~product_set_relation();
-        virtual void reset();
-        virtual void add_fact(const relation_fact & f);
-        virtual bool contains_fact(const relation_fact & f) const;
-        virtual product_set_relation * clone() const;
-        virtual product_set_relation * complement(func_decl*) const;
-        virtual void to_formula(expr_ref& fml) const;
-        product_set_plugin& get_plugin() const; 
-        virtual bool empty() const { return m_elems.empty(); }
-        virtual void display(std::ostream& out) const;
-
-        virtual bool is_precise() const { return true; }
-    };
-
-    class product_set_plugin : public relation_plugin {
-        friend class product_set_relation;
-        class join_fn;
-        class project_fn;
-        class union_fn;
-        class rename_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);
-        virtual bool can_handle_signature(const relation_signature & s);
-        static symbol get_name() { return symbol("product_set"); }
-        virtual relation_base * mk_empty(const relation_signature & s);
-        virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
-        virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
-            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
-        virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 
-            const unsigned * removed_cols);
-        virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 
-            const unsigned * permutation_cycle);
-        virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 
-            const relation_base * delta);
-        virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src, 
-            const relation_base * delta);
-        virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
-            const unsigned * identical_cols);
-        virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 
-            unsigned col);
-        virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
-
-        unsigned set_size(sort* ty);
-
-    private:
-        static product_set_relation& get(relation_base& r);
-        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);
-    };
-
-    class product_set_factory;
-
-
-    class product_set2 {
-        friend class product_set_factory;
-        unsigned char m_data[0];
-    public:
-        enum initial_t {
-            EMPTY_t,
-            FULL_t
-        };
-        product_set2(product_set_factory& fac, initial_t init);
-        ~product_set2();
-        unsigned get_hash(product_set_factory& fac) const;
-        bool equals(product_set_factory& fac, product_set2 const& other) const;
-        void add_fact(product_set_factory& fac, const relation_fact & f);
-        bool contains_fact(product_set_factory& fac, const relation_fact & f) const;
-        relation_base * clone(product_set_factory& fac) const;
-        void reset(product_set_factory& fac);
-        void mk_join(product_set_factory& fac, product_set2 const& r1, product_set2 const& r2, 
-                     unsigned num_cols, unsigned const* cols1, unsigned const* cols2);
-        void mk_project(product_set_factory& fac, 
-                        product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols);
-        void mk_rename(product_set_factory& fac, 
-                       product_set2 const& r, unsigned col_cnt, unsigned const* cycle);
-        void mk_union(product_set_factory& fac, 
-                      product_set2 const& src, product_set2* delta, bool is_widen);
-        unsigned find(product_set_factory& fac, unsigned i);
-        void merge(product_set_factory& fac, unsigned i, unsigned j);
-        void display(product_set_factory& fac, std::ostream& out) const;        
-    };
-
-
-    class product_set_factory {
-        unsigned char m_data[0];
-    public:
-        enum initial_t {
-            EMPTY_t,
-            FULL_t
-        };
-        product_set_factory(product_set_plugin& p, relation_signature const& sig);
-        ~product_set_factory();
-        product_set2* create();
-        void          retire(product_set2*);
-
-        unsigned get_hash(product_set2& ps) const;
-        bool equals(product_set2 const& p1, product_set2 const& p2);
-        void add_fact(product_set2& p, const relation_fact & f);
-        bool contains_fact(product_set2& p, const relation_fact & f) const;
-        relation_base * clone(product_set2& p) const;
-        void reset(product_set2& p);
-        void mk_join(product_set2& p, product_set2 const& r1, product_set2 const& r2, 
-                     unsigned num_cols, unsigned const* cols1, unsigned const* cols2);
-        void mk_project(product_set2& p, 
-                        product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols);
-        void mk_rename(product_set2& p, 
-                       product_set2 const& r, unsigned col_cnt, unsigned const* cycle);
-        void mk_union(product_set2& p, 
-                      product_set2 const& src, product_set2* delta, bool is_widen);
-        unsigned find(product_set2& p, unsigned i);
-        void merge(product_set2& p, unsigned i, unsigned j);
-        void display(product_set2& p, std::ostream& out) const;        
-    };
-
-
-};
-
-#endif
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index a2519137c..f3ac4bf84 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -32,7 +32,6 @@ Revision History:
 #include"dl_interval_relation.h"
 #include"karr_relation.h"
 #include"dl_finite_product_relation.h"
-#include"product_set.h"
 #include"udoc_relation.h"
 #include"check_relation.h"
 #include"dl_lazy_table.h"
@@ -117,7 +116,6 @@ namespace datalog {
         rm.register_plugin(alloc(bound_relation_plugin, rm));
         rm.register_plugin(alloc(interval_relation_plugin, rm));
         if (m_context.karr()) rm.register_plugin(alloc(karr_relation_plugin, rm));
-        rm.register_plugin(alloc(product_set_plugin, rm));
         rm.register_plugin(alloc(udoc_plugin, rm));
         rm.register_plugin(alloc(check_relation_plugin, rm));
     }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 8e971ac1e..b6fa339ff 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -500,7 +500,6 @@ namespace datalog {
             udoc_relation const& src = get(_src);
             udoc_relation* d = get(_delta);
             doc_manager& dm = r.get_dm();
-            ast_manager& m = r.get_plugin().get_ast_manager();
             udoc* d1 = 0;
             if (d) d1 = &d->get_udoc();
             IF_VERBOSE(3, r.display(verbose_stream() << "orig:  "););
@@ -561,7 +560,6 @@ namespace datalog {
             : m_cols(col_cnt), m_equalities(union_ctx) {
             udoc_relation const& r = get(_r);
             doc_manager& dm = r.get_dm();
-            unsigned num_bits = dm.num_tbits();
             m_size = r.column_num_bits(identical_cols[0]);
             m_empty_bv.resize(r.get_num_bits(), false);            
             for (unsigned i = 0; i < col_cnt; ++i) {
@@ -946,7 +944,6 @@ namespace datalog {
         virtual void operator()(relation_base & tb) {            
             udoc_relation & t = get(tb);
             udoc& u = t.get_udoc();
-            ast_manager& m = m_reduced_condition.get_manager();
             SASSERT(u.well_formed(dm));
             u.intersect(dm, m_udoc);
             SASSERT(u.well_formed(dm));
@@ -981,7 +978,6 @@ namespace datalog {
               , m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2)
 #endif
         {
-            udoc_plugin& p = t1.get_plugin();
             unsigned num_bits1 = t1.get_num_bits();
             unsigned num_bits = num_bits1 + t2.get_num_bits();
             unsigned_vector removed_cols(removed_col_cnt, rm_cols);
@@ -1022,7 +1018,6 @@ namespace datalog {
             udoc const& d1 = t1.get_udoc();
             udoc const& d2 = t2.get_udoc();
             doc_manager& dm1 = t1.get_dm();
-            doc_manager& dm2 = t2.get_dm();
             udoc_plugin& p = t1.get_plugin();
             doc_manager& dm_prod = p.dm(prod_signature);
             udoc_relation* result = get(p.mk_empty(get_result_signature()));
@@ -1134,7 +1129,6 @@ namespace datalog {
         virtual void operator()(relation_base& tb, const relation_base& negb) {
             udoc_relation& t = get(tb);
             udoc_relation const& n = get(negb);
-            udoc_plugin& p = t.get_plugin();
             IF_VERBOSE(3, t.display(verbose_stream() << "dst:"););
             IF_VERBOSE(3, n.display(verbose_stream() << "neg:"););
             if (t.fast_empty() || n.fast_empty())
@@ -1241,7 +1235,6 @@ namespace datalog {
             udoc_relation const & t = get(tb);
             udoc const& u1 = t.get_udoc();
             doc_manager& dm = t.get_dm();
-            ast_manager& m = m_reduced_condition.get_manager();
             m_udoc2.copy(dm, u1);
             m_udoc2.intersect(dm, m_udoc);
             t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete);
diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp
index 8c10d3640..54ecaf35b 100644
--- a/src/opt/hitting_sets.cpp
+++ b/src/opt/hitting_sets.cpp
@@ -149,13 +149,13 @@ namespace opt {
             m_max_weight(0), 
             m_denominator(1),
             m_alloc("hitting-sets"),
-            m_weights_var(0),
             m_qhead(0),
-            m_scope_lvl(0),
             m_conflict_j(justification(justification::AXIOM)),
             m_inconsistent(false),
+            m_scope_lvl(0),
             m_compare_scores(),
-            m_heap(0, m_compare_scores) {
+            m_heap(0, m_compare_scores),
+            m_weights_var(0) {
             m_enable_simplex = true;
             m_compare_scores.m_imp = this;
         }
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index f3a4099d0..19205ddd9 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -73,7 +73,6 @@ namespace opt {
         filter_model_converter& m_fm;
         progress_callback * m_callback;
         symbol              m_logic;
-        bool                m_objective_enabled;
         svector<smt::theory_var>  m_objective_vars;
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;
diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index 7ad0ec837..e3613515f 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -176,7 +176,6 @@ namespace sat {
     bool bceq::bce(clause& cls) {
         svector<bool> live_clauses;
         use_list ul;
-        use_list* save = m_use_list;
         m_use_list = &ul;
         ul.init(m_solver.num_vars());
         for (unsigned i = 0; i < m_L.size(); ++i) {
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index 65d776d84..4a811741f 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -24,7 +24,7 @@ Notes:
 
 namespace sat {
 
-    mus::mus(solver& s):s(s), m_is_active(false) {}
+    mus::mus(solver& s):s(s), m_is_active(false), m_best_value(0), m_restart(0), m_max_restarts(0) {}
 
     mus::~mus() {}
    
diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h
index 944cceffb..12cff4cec 100644
--- a/src/sat/sat_mus.h
+++ b/src/sat/sat_mus.h
@@ -21,6 +21,7 @@ Notes:
 
 namespace sat {
     class mus {
+        solver& s;
         literal_vector m_core;
         literal_vector m_mus;
         bool           m_is_active;
@@ -30,7 +31,6 @@ namespace sat {
         unsigned       m_max_restarts;
 
 
-        solver& s;
     public:
         mus(solver& s);
         ~mus();        
diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp
index bd0f8855a..0744ef37a 100644
--- a/src/sat/sat_sls.cpp
+++ b/src/sat/sat_sls.cpp
@@ -365,7 +365,6 @@ namespace sat {
         m_clause_weights.resize(m_clauses.size(), 1);
         m_sscore.resize(s.num_vars(), 0.0);
         m_hscore.resize(s.num_vars(), 0);
-        unsigned num_violated = 0;
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             literal lit = m_soft[i];
             m_sscore[lit.var()] = m_weights[i];
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b1bcaa07f..40d02ebbb 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1637,7 +1637,6 @@ namespace sat {
 
     void solver::process_antecedent_for_unsat_core(literal antecedent) {
         bool_var var     = antecedent.var();
-        unsigned var_lvl = lvl(var);
         SASSERT(var < num_vars());
         TRACE("sat", tout << antecedent << " " << (is_marked(var)?"+":"-") << "\n";);
         if (!is_marked(var)) {
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 616fc1962..a7b4f807e 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -340,7 +340,6 @@ unsigned parse_opt(char const* file_name, bool is_wcnf) {
     g_start_time = static_cast<double>(clock());
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);
-    unsigned result = 0;
     if (file_name) {
         std::ifstream in(file_name);
         if (in.bad() || in.fail()) {
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d1f7abcbc..0e4eba822 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -961,7 +961,6 @@ namespace smt {
     bool theory_arith<Ext>::is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& shared) {
         
         context& ctx = get_context();
-        ast_manager& m = get_manager();
         shared |= ctx.is_shared(get_enode(x));
         column & c      = m_columns[x];
         typename svector<col_entry>::iterator it  = c.begin_entries();
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index b5cdbcfe2..a004da666 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -163,7 +163,6 @@ namespace smt {
         ast_manager & m  = get_manager();
         app*        own  = n->get_owner();
         expr*       arg1 = own->get_arg(0);
-        expr*       arg2 = own->get_arg(1);
         func_decl * upd  = n->get_decl();
         func_decl * acc  = to_func_decl(upd->get_parameter(0).get_ast());
         func_decl * con  = m_util.get_accessor_constructor(acc);
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index 5f0163077..971c7af57 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -631,11 +631,12 @@ public:
         m(m),
         m_util(m),
         m_params(p),
+        m_produce_proofs(false),       
+        m_fmc(0),
+        m_cancel(false),
         m_nl_tac(mk_nlsat_tactic(m, p)),
         m_nl_g(0),
         m_solver(mk_smt_solver(m, p, symbol::null)),
-        m_fmc(0),
-        m_cancel(false),
         m_eq_preds(m),
         m_new_reals(m),
         m_new_preds(m),
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 4940fa448..994083834 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1065,8 +1065,8 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
             m_mpz_manager.mul2k(rem, 1, t);
             bool tie = m_mpz_manager.eq(t, shift_p);
             if (tie &&
-                (rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
-                (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div)))
+                ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
+                 (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))))
                 m_mpz_manager.inc(div);
             else if (x.sign ^ m_mpz_manager.gt(t, shift_p))
                 m_mpz_manager.inc(div);