diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 05135a44f..2b3b70a41 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -574,7 +574,7 @@ namespace datalog {
 
     void context::check_uninterpreted_free(rule& r) {
         func_decl* f = 0;
-        if (r.has_uninterpreted_non_predicates(m, f)) {
+        if (get_rule_manager().has_uninterpreted_non_predicates(r, f)) {
             std::stringstream stm;
             stm << "Uninterpreted '" 
                 << f->get_name() 
@@ -585,7 +585,7 @@ namespace datalog {
     }
 
     void context::check_quantifier_free(rule& r) {
-        if (r.has_quantifiers()) {
+        if (get_rule_manager().has_quantifiers(r)) {
             std::stringstream stm;
             stm << "cannot process quantifiers in rule ";
             r.display(*this, stm);
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 6296717da..2015d4eea 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -56,7 +56,8 @@ namespace datalog {
           m_hnf(m),
           m_qe(m),
           m_cfg(m),
-          m_rwr(m, false, m_cfg) {}
+          m_rwr(m, false, m_cfg),
+          m_ufproc(m) {}
 
     void rule_manager::inc_ref(rule * r) {
         if (r) {
@@ -911,83 +912,40 @@ namespace datalog {
         return false;
     }
 
-    struct uninterpreted_function_finder_proc {
-        ast_manager& m;
-        datatype_util m_dt;
-        bool m_found;
-        func_decl* m_func;
-        uninterpreted_function_finder_proc(ast_manager& m): 
-            m(m), m_dt(m), m_found(false), m_func(0) {}
-        void operator()(var * n) { }
-        void operator()(quantifier * n) { }
-        void operator()(app * n) {
-            if (is_uninterp(n)) {
-                m_found = true;
-                m_func = n->get_decl();
-            }
-            else if (m_dt.is_accessor(n)) {
-                sort* s = m.get_sort(n->get_arg(0));
-                SASSERT(m_dt.is_datatype(s));
-                if (m_dt.get_datatype_constructors(s)->size() > 1) {
-                    m_found = true;
-                    m_func = n->get_decl();
-                }
-            }
-        }
-
-        bool found(func_decl*& f) const { f = m_func; return m_found; }
-    };
 
     //
     // non-predicates may appear only in the interpreted tail, it is therefore 
     // sufficient only to check the tail.
     //
-    bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
-        unsigned sz = get_tail_size();
-        uninterpreted_function_finder_proc proc(m);
-        expr_mark visited;
-        for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
-            for_each_expr(proc, visited, get_tail(i));
+    bool rule_manager::has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const {
+        unsigned sz = r.get_tail_size();
+        m_ufproc.reset();
+        m_visited.reset();
+        for (unsigned i = r.get_uninterpreted_tail_size(); i < sz && !m_ufproc.found(f); ++i) {
+            for_each_expr_core<uninterpreted_function_finder_proc,expr_sparse_mark, true, false>(m_ufproc, m_visited, r.get_tail(i));
         }
-        return proc.found(f);
+        return m_ufproc.found(f);
     }
 
 
-    struct quantifier_finder_proc {
-        bool m_exist;
-        bool m_univ;
-        quantifier_finder_proc() : m_exist(false), m_univ(false) {}
-        void operator()(var * n) { }
-        void operator()(quantifier * n) {
-            if (n->is_forall()) {
-                m_univ = true;
-            }
-            else {
-                SASSERT(n->is_exists());
-                m_exist = true;
-            }
-        }
-        void operator()(app * n) { }
-    };
-
     //
     // Quantifiers may appear only in the interpreted tail, it is therefore 
     // sufficient only to check the interpreted tail.
     //
-    void rule::has_quantifiers(bool& existential, bool& universal) const {
-        unsigned sz = get_tail_size();
-        quantifier_finder_proc proc;
-        expr_mark visited;
-        for (unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
-            for_each_expr(proc, visited, get_tail(i));
+    void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const {
+        unsigned sz = r.get_tail_size();
+        m_qproc.reset();
+        m_visited.reset();
+        for (unsigned i = r.get_uninterpreted_tail_size(); i < sz; ++i) {
+            for_each_expr_core<quantifier_finder_proc,expr_sparse_mark, true, false>(m_qproc, m_visited, r.get_tail(i));
         }
-        existential = proc.m_exist;
-        universal = proc.m_univ;
+        existential = m_qproc.m_exist;
+        universal = m_qproc.m_univ;
     }
 
-    bool rule::has_quantifiers() const {
+    bool rule_manager::has_quantifiers(rule const& r) const {
         bool exist, univ;
-        has_quantifiers(exist, univ);
+        has_quantifiers(r, exist, univ);
         return exist || univ;
     }
 
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index e90edefa1..50211e1d9 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -31,6 +31,7 @@ Revision History:
 #include"hnf.h"
 #include"qe_lite.h"
 #include"var_subst.h"
+#include"datatype_decl_plugin.h"
 
 namespace datalog {
 
@@ -43,6 +44,57 @@ namespace datalog {
     typedef obj_ref<rule, rule_manager> rule_ref;
     typedef ref_vector<rule, rule_manager> rule_ref_vector;
     typedef ptr_vector<rule> rule_vector;
+
+
+    struct quantifier_finder_proc {
+        bool m_exist;
+        bool m_univ;
+        quantifier_finder_proc() : m_exist(false), m_univ(false) {}
+        void operator()(var * n) { }
+        void operator()(quantifier * n) {
+            if (n->is_forall()) {
+                m_univ = true;
+            }
+            else {
+                SASSERT(n->is_exists());
+                m_exist = true;
+            }
+        }
+        void operator()(app * n) { }
+        void reset() { m_exist = m_univ = false; }
+    };
+
+    struct uninterpreted_function_finder_proc {
+        ast_manager& m;
+        datatype_util m_dt;
+        bool m_found;
+        func_decl* m_func;
+        uninterpreted_function_finder_proc(ast_manager& m): 
+            m(m), m_dt(m), m_found(false), m_func(0) {}
+
+        void reset() { m_found = false; m_func = 0; }
+
+        void operator()(var * n) { }
+        void operator()(quantifier * n) { }
+        void operator()(app * n) {
+            if (is_uninterp(n)) {
+                m_found = true;
+                m_func = n->get_decl();
+            }
+            else if (m_dt.is_accessor(n)) {
+                sort* s = m.get_sort(n->get_arg(0));
+                SASSERT(m_dt.is_datatype(s));
+                if (m_dt.get_datatype_constructors(s)->size() > 1) {
+                    m_found = true;
+                    m_func = n->get_decl();
+                }
+            }
+        }
+
+        bool found(func_decl*& f) const { f = m_func; return m_found; }
+    };
+
+
     /**
        \brief Manager for the \c rule class
 
@@ -75,6 +127,9 @@ namespace datalog {
         qe_lite              m_qe;
         remove_label_cfg               m_cfg;
         rewriter_tpl<remove_label_cfg> m_rwr;
+        mutable uninterpreted_function_finder_proc m_ufproc;
+        mutable quantifier_finder_proc m_qproc;
+        mutable expr_sparse_mark       m_visited;
 
 
         // only the context can create a rule_manager
@@ -220,6 +275,10 @@ namespace datalog {
 
         std::ostream& display_smt2(rule const& r, std::ostream & out);
 
+        bool has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const;
+        void has_quantifiers(rule const& r, bool& existential, bool& universal) const;
+        bool has_quantifiers(rule const& r) const;
+
     };
 
     class rule : public accounted_object {
@@ -295,9 +354,6 @@ namespace datalog {
         */
         bool is_in_tail(const func_decl * p, bool only_positive=false) const;
 
-        bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const;
-        void has_quantifiers(bool& existential, bool& universal) const;
-        bool has_quantifiers() const;
         bool has_negation() const;
 
         /**
diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index c30ca8b0e..a0dbe9518 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -88,6 +88,7 @@ class hnf::imp {
     proof_ref_vector      m_defs;
     contains_predicate_proc m_proc;
     expr_free_vars        m_free_vars;
+    ast_fast_mark1        m_mark1;
 
 
 public:
@@ -106,10 +107,37 @@ public:
         m_proc(*this) {
     }
 
+    bool is_horn(expr* n) {
+        expr* n1, *n2;
+        while (is_forall(n)) n = to_quantifier(n)->get_expr();
+        if (m.is_implies(n, n1, n2) && is_predicate(n2)) {
+            app* a1 = to_app(n1);
+            if (m.is_and(a1)) {
+                for (unsigned i = 0; i < a1->get_num_args(); ++i) {
+                    if (!is_predicate(a1->get_arg(i)) && 
+                        contains_predicate(a1->get_arg(i))) {                    
+                        return false;
+                    }
+                }
+            }
+            else if (!is_predicate(a1) && contains_predicate(a1)) {
+                return false;
+            }
+            return true;
+        }    
+        
+        return false;
+    }
+
     void operator()(expr * n, 
                     proof* p,
                     expr_ref_vector& result, 
                     proof_ref_vector& ps) {
+        if (is_horn(n)) {
+            result.push_back(n);
+            ps.push_back(p);
+            return;
+        }
         expr_ref fml(m);
         proof_ref pr(m);
         m_todo.reset();
@@ -184,9 +212,11 @@ private:
 
     bool contains_predicate(expr* fml)  {
         try {
-            quick_for_each_expr(m_proc, fml);
+            quick_for_each_expr(m_proc, m_mark1, fml);
+            m_mark1.reset();
         }
         catch (contains_predicate_proc::found) {
+            m_mark1.reset();
             return true;
         }
         return false;
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 1d1a59e5f..2b970e4fa 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1500,7 +1500,7 @@ namespace datalog {
             if (m_rules.get_rule(i)->get_uninterpreted_tail_size() > 1) {
                 return false;
             }
-            if (m_rules.get_rule(i)->has_quantifiers()) {
+            if (m_rules.get_rule_manager().has_quantifiers(*m_rules.get_rule(i))) {
                 return false;
             }
         }
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index beafc7c3e..98a0635fe 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -149,7 +149,7 @@ namespace datalog {
     }
 
     bool check_relation_plugin::can_handle_signature(const relation_signature & sig) {
-        return m_base->can_handle_signature(sig);
+        return m_base && m_base->can_handle_signature(sig);
     }
     relation_base * check_relation_plugin::mk_empty(const relation_signature & sig) {
         relation_base* r = m_base->mk_empty(sig);
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 86849ba72..3be31ead7 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -291,7 +291,7 @@ public:
     void merge(M& m, unsigned_vector const& roots, subset_ints const& equalities, 
                bit_vector const& discard_cols) {
         for (unsigned i = 0; i < roots.size(); ++i) {
-            merge(m, roots[i], equalities, discard_cols);
+            merge(m, roots[i], 1, equalities, discard_cols);
         }
     }
 
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 62932a901..6454da2a2 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -578,7 +578,9 @@ namespace datalog {
     }
 
     void rel_context::updt_params() {
-        if (m_context.check_relation() != symbol::null) {
+        if (m_context.check_relation() != symbol::null &&
+            m_context.check_relation() != symbol("null")) {
+            std::cout << m_context.check_relation() << "\n";
             symbol cr("check_relation");
             m_context.set_default_relation(cr);
             relation_plugin* p = get_rmanager().get_relation_plugin(cr);
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 2bdec8e01..89bf2ef54 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -63,6 +63,7 @@ namespace datalog {
         m_elems.push_back(fact2doc(f));
     }
     bool udoc_relation::empty() const {
+        if (get_signature().empty()) return false;
         // TBD: make this a complete check
         for (unsigned i = 0; i < m_elems.size(); ++i) {
             if (!dm.is_empty(m_elems[i])) return false;
@@ -719,29 +720,60 @@ namespace datalog {
         conds.push_back(g);
         qe::flatten_and(conds);
         expr* e1, *e2;
-        unsigned v1, v2, lo1, lo2, hi1, hi2;
         for (unsigned i = 0; i < conds.size(); ++i) {
             expr* g = conds[i].get();
-            if (m.is_eq(g, e1, e2) && 
-                is_var_range(e1, hi1, lo1, v1) &&
-                is_var_range(e2, hi2, lo2, v2)) {
-                unsigned col1 = column_idx(v1);
-                lo1 += col1;
-                hi1 += col1;
-                unsigned col2 = column_idx(v2);
-                lo2 += col2;
-                hi2 += col2;
-                for (unsigned j = 0; j <= hi1-lo1; ++j) {
-                    roots.push_back(lo1 + j);
-                    equalities.merge(lo1 + j, lo2 + j);
-                }
+            if (m.is_eq(g, e1, e2)) {
+                extract_equalities(e1, e2, conds, equalities, roots);
                 conds[i] = conds.back();
                 conds.pop_back();
-                --i;
             }
         }
         rest = mk_and(m, conds.size(), conds.c_ptr());
     }
+
+    void udoc_relation::extract_equalities(
+        expr* e1, expr* e2, expr_ref_vector& conds, 
+        subset_ints& equalities, unsigned_vector& roots) const {        
+        udoc_plugin& p = get_plugin();
+        ast_manager& m  = p.get_ast_manager();
+        bv_util& bv = p.bv;
+        th_rewriter rw(m);
+        unsigned hi, lo1, lo2, hi1, hi2, v1, v2;
+        if (bv.is_concat(e2)) {
+            std::swap(e1, e2);
+        }
+        if (bv.is_concat(e1)) {
+            expr_ref e3(m);
+            app* a1 = to_app(e1);
+            hi = p.num_sort_bits(e1)-1;
+            unsigned n = a1->get_num_args();
+            for (unsigned i = 0; i < n; ++i) {
+                expr* e = a1->get_arg(i);
+                unsigned sz = p.num_sort_bits(e);
+                e3 = bv.mk_extract(hi, hi-sz+1, e2);
+                rw(e3);
+                extract_equalities(e, e3, conds, equalities, roots);
+                hi -= sz;
+            }
+            return;
+        }
+        if (is_var_range(e1, hi1, lo1, v1) && 
+            is_var_range(e2, hi2, lo2, v2)) {
+            unsigned col1 = column_idx(v1);
+            lo1 += col1;
+            hi1 += col1;
+            unsigned col2 = column_idx(v2);
+            lo2 += col2;
+            hi2 += col2;
+            for (unsigned j = 0; j <= hi1-lo1; ++j) {
+                roots.push_back(lo1 + j);
+                equalities.merge(lo1 + j, lo2 + j);
+            }
+            return;
+        }   
+        conds.push_back(m.mk_eq(e1, e2));
+    }
+
     void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const {
         d.reset(dm);
         d.push_back(dm.allocateX()); 
@@ -772,6 +804,9 @@ namespace datalog {
         return false;
     }
 
+
+
+
     bool udoc_relation::apply_bv_eq(
         expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const {
         udoc_plugin& p = get_plugin();
@@ -1067,6 +1102,7 @@ namespace datalog {
         expr_ref     m_original_condition;
         expr_ref     m_reduced_condition;
         udoc         m_udoc;
+        udoc         m_udoc2;
         bit_vector   m_col_list; // map: col idx -> bool (whether the column is to be removed)
         svector<bool> m_to_delete; // same
         subset_ints  m_equalities;
@@ -1107,22 +1143,19 @@ namespace datalog {
             udoc const& u1 = t.get_udoc();
             doc_manager& dm = t.get_dm();
             ast_manager& m = m_reduced_condition.get_manager();
-            udoc  u2;
-            u2.copy(dm, u1);
-            u2.intersect(dm, m_udoc);
-            u2.merge(dm, m_roots, m_equalities, m_col_list);
-            t.apply_guard(m_reduced_condition, u2, m_equalities, m_col_list);
-            SASSERT(u2.well_formed(dm));  
+            m_udoc2.copy(dm, u1);
+            m_udoc2.intersect(dm, m_udoc);
+            t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_col_list);
+            m_udoc2.merge(dm, m_roots, m_equalities, m_col_list);
+            SASSERT(m_udoc2.well_formed(dm));  
             udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
             doc_manager& dm2 = r->get_dm();
-            // std::cout << "Size of union: " << u2.size() << "\n";
-            for (unsigned i = 0; i < u2.size(); ++i) {
-                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]);
-                dm.verify_project(m, dm2, m_to_delete.c_ptr(), u2[i], *d);
+            for (unsigned i = 0; i < m_udoc2.size(); ++i) {
+                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), m_udoc2[i]);
                 r->get_udoc().insert(dm2, d);
                 SASSERT(r->get_udoc().well_formed(dm2));
             }
-            u2.reset(dm);
+            m_udoc2.reset(dm);
             IF_VERBOSE(3, r->display(verbose_stream() << "filter project result:\n"););
             return r;
         }
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index 64ced8e83..0adc61b64 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -48,7 +48,7 @@ namespace datalog {
         virtual udoc_relation * complement(func_decl*) const;
         virtual void to_formula(expr_ref& fml) const;
         udoc_plugin& get_plugin() const; 
-        virtual bool fast_empty() const { return m_elems.is_empty(); }
+        virtual bool fast_empty() const { return !get_signature().empty() && m_elems.is_empty(); }
         virtual bool empty() const; 
         virtual void display(std::ostream& out) const;
         virtual bool is_precise() const { return true; }
@@ -68,6 +68,9 @@ namespace datalog {
         bool is_guard(unsigned n, expr* const *g) const;
         void compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
         void extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities, unsigned_vector& roots) const;
+        void extract_equalities(
+            expr* e1, expr* e2, expr_ref_vector& conds, 
+            subset_ints& equalities, unsigned_vector& roots) const;
         void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
         void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
         bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index b01b4326c..ca3042ff5 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -491,9 +491,10 @@ namespace datalog {
 
     bool mk_interp_tail_simplifier::transform_rule(rule * r0, rule_ref & res)
     {
-        rule_ref r(r0, m_context.get_rule_manager());
+        rule_manager& rm = m_context.get_rule_manager();
+        rule_ref r(r0, rm);
 
-        if (r->has_quantifiers()) {
+        if (rm.has_quantifiers(*r)) {
             res = r;
             return true;
         }
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index afb22e55f..95d3e8e73 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -252,9 +252,10 @@ namespace datalog {
         }
         bool has_quantifiers = false;
         unsigned sz = source.get_num_rules();
+        rule_manager& rm = m_ctx.get_rule_manager();
         for (unsigned i = 0; !has_quantifiers && i < sz; ++i) {
             rule& r = *source.get_rule(i);
-            has_quantifiers = has_quantifiers || r.has_quantifiers();   
+            has_quantifiers = has_quantifiers || rm.has_quantifiers(r);   
             if (r.has_negation()) {
                 return 0;
             }
diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp
index f162d550f..2a49d534e 100644
--- a/src/muz/transforms/dl_mk_slice.cpp
+++ b/src/muz/transforms/dl_mk_slice.cpp
@@ -813,9 +813,10 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_slice::operator()(rule_set const & src) {        
+    rule_set * mk_slice::operator()(rule_set const & src) { 
+        rule_manager& rm = m_ctx.get_rule_manager();       
         for (unsigned i = 0; i < src.get_num_rules(); ++i) {
-            if (src.get_rule(i)->has_quantifiers()) {
+            if (rm.has_quantifiers(*src.get_rule(i))) {
                 return 0;
             }
         }