diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index b7cb5680f..bd70c06ef 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -558,6 +558,7 @@ namespace datalog {
             m_rule_properties.check_quantifier_free();
             m_rule_properties.check_uninterpreted_free();
             m_rule_properties.check_nested_free(); 
+            m_rule_properties.check_infinite_sorts();
             break;
         case PDR_ENGINE:
             m_rule_properties.collect(r);
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 7cb1c6241..5d1aff44e 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -26,7 +26,7 @@ Notes:
 
 using namespace datalog;
 rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): 
-    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {}
+    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_bv(m), m_generate_proof(false) {}
 
 rule_properties::~rule_properties() {}
 
@@ -48,6 +48,12 @@ void rule_properties::collect(rule_set const& rules) {
         if (m_generate_proof && !r->get_proof()) {
             rm.mk_rule_asserted_proof(*r);
         }
+        for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
+            sort* d = r->get_decl()->get_domain(i);
+            if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
+                m_inf_sort.push_back(m_rule);
+            }
+        }
     }     
 }
 
@@ -85,6 +91,16 @@ void rule_properties::check_uninterpreted_free() {
     }
 }
 
+void rule_properties::check_infinite_sorts() {
+    if (!m_inf_sort.empty()) {
+        std::stringstream stm;
+        rule* r = m_inf_sort.back();
+        stm << "Rule contains infinite sorts in rule ";
+        r->display(m_ctx, stm);
+        throw default_exception(stm.str());
+    }
+}
+
 void rule_properties::check_nested_free() {
     if (!m_interp_pred.empty()) {
         std::stringstream stm;
@@ -92,7 +108,6 @@ void rule_properties::check_nested_free() {
         stm << "Rule contains nested predicates ";
         r->display(m_ctx, stm);
         throw default_exception(stm.str());
-
     }
 }
 
@@ -158,7 +173,8 @@ void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
     }
 }
 
-void rule_properties::operator()(var* n) { }
+void rule_properties::operator()(var* n) { 
+}
 
 void rule_properties::operator()(quantifier* n) {
     m_quantifiers.insert(n, m_rule);
@@ -177,6 +193,10 @@ void rule_properties::operator()(app* n) {
             m_uninterp_funs.insert(n->get_decl(), m_rule);
         }
     }
+    else {
+        std::cout << mk_pp(n, m) << "\n";
+    }
+
 }
 
 void rule_properties::reset() {
@@ -184,5 +204,6 @@ void rule_properties::reset() {
     m_uninterp_funs.reset();
     m_interp_pred.reset();
     m_negative_rules.reset();
+    m_inf_sort.reset();
 }
 
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index a16f63507..18ecd2ee8 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -23,6 +23,7 @@ Notes:
 
 #include"ast.h"
 #include"datatype_decl_plugin.h"
+#include"bv_decl_plugin.h"
 #include"dl_rule.h"
 
 namespace datalog {
@@ -33,12 +34,14 @@ namespace datalog {
         i_expr_pred&  m_is_predicate;
         datatype_util m_dt;
         dl_decl_util  m_dl;
+        bv_util       m_bv;
         bool          m_generate_proof;
         rule*         m_rule;
         obj_map<quantifier, rule*> m_quantifiers;
         obj_map<func_decl, rule*>  m_uninterp_funs;
         ptr_vector<rule>           m_interp_pred;
         ptr_vector<rule>           m_negative_rules;
+        ptr_vector<rule>           m_inf_sort;
 
         void insert(ptr_vector<rule>& rules, rule* r);
     public:
@@ -51,6 +54,7 @@ namespace datalog {
         void check_existential_tail();
         void check_for_negated_predicates();
         void check_nested_free();
+        void check_infinite_sorts();
         void operator()(var* n);
         void operator()(quantifier* n);
         void operator()(app* n);
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 1338a6de6..7fcbdaaff 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -654,7 +654,7 @@ namespace datalog {
         family_id expl_kind = m_er_plugin->get_kind();
         family_id expl_sieve_kind = sieve_plugin.get_relation_kind(sig, expl_sieve, expl_kind);
 
-        product_relation_plugin::rel_spec product_spec;
+        rel_spec product_spec;
         product_spec.push_back(inner_sieve_kind);
         product_spec.push_back(expl_sieve_kind);
 
diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp
index f1dbc589c..1bc5e3545 100644
--- a/src/muz/rel/dl_product_relation.cpp
+++ b/src/muz/rel/dl_product_relation.cpp
@@ -77,6 +77,7 @@ namespace datalog {
     }
 
     family_id product_relation_plugin::get_relation_kind(const relation_signature & sig, const rel_spec & spec) {
+        SASSERT(spec.well_formed());
         return m_spec_store.get_relation_kind(sig, spec);
     }
 
@@ -132,14 +133,11 @@ namespace datalog {
         ptr_vector<const product_relation>::const_iterator rend = rels.end();
         for(; rit!=rend; ++rit) {
             specs.push_back((*rit)->m_spec);
+            SASSERT(specs.back().well_formed());
+            std::sort(specs.back().begin(), specs.back().end());
         }
 
-        vector<rel_spec>::iterator sit = specs.begin();
-        vector<rel_spec>::iterator send = specs.end();
-        for(; sit!=send; ++sit) {
-            rel_spec & s = *sit;
-            std::sort(s.begin(), s.end());
-        }
+        vector<rel_spec>::iterator sit = specs.begin(), send = specs.end();
 
         res.reset();
         for(;;) {
@@ -160,7 +158,7 @@ namespace datalog {
             sit = specs.begin();
             for(; sit!=send; ++sit) {
                 rel_spec & s = *sit;
-                if(!s.empty() && s.back()==next) {
+                while (!s.empty() && s.back()==next) {
                     s.pop_back();
                 }
             }
@@ -191,6 +189,7 @@ namespace datalog {
         }
         rel_spec spec;
         m_spec_store.get_relation_spec(s, kind, spec);
+        SASSERT(spec.well_formed());
         relation_vector inner_rels;
         unsigned rel_cnt = spec.size();
         for(unsigned i=0; i<rel_cnt; i++) {
@@ -540,6 +539,7 @@ namespace datalog {
      
     class product_relation_plugin::aligned_union_fn : public relation_union_fn {
         relation_manager & m_rmgr;
+        product_relation_plugin& m_plugin;
         bool m_is_widen;
 
         //m_union[i][j] is union between i-th and j-th relation.
@@ -556,6 +556,7 @@ namespace datalog {
             else {
                 u = rmgr.mk_union_fn(r1, r2, delta);
             }
+            TRACE("dl_verbose", tout << r1.get_plugin().get_name() << " " << r2.get_plugin().get_name() << " " << (u?"found":"not found") << "\n";); 
             m_unions.back().push_back(u);
         }
 
@@ -574,7 +575,7 @@ namespace datalog {
         }
 
         bool can_do_inner_union(unsigned tgt_idx, unsigned src_idx) {
-            return m_unions[tgt_idx][src_idx]!=0;
+            return m_unions[tgt_idx][src_idx] != 0;
         }
 
         void do_inner_union(unsigned tgt_idx, unsigned src_idx, relation_base& tgt, 
@@ -601,7 +602,8 @@ namespace datalog {
         void do_intersection(relation_base& tgt, relation_base& src) {
             scoped_ptr<relation_intersection_filter_fn> intersect_fun = 
                 m_rmgr.mk_filter_by_intersection_fn(tgt, src);
-            if(!intersect_fun) {
+            if (!intersect_fun) {
+                TRACE("dl", tgt.display(tout << "tgt\n"); src.display(tout << "src\n");); 
                 warning_msg("intersection does not exist");
                 return;
             }
@@ -613,9 +615,13 @@ namespace datalog {
             (*union_fun)(tgt, src);
         }
     public:
-        aligned_union_fn(product_relation const& tgt, product_relation const& src, product_relation const* delta, 
-                    bool is_widen) :
+        aligned_union_fn(
+            product_relation const& tgt, 
+            product_relation const& src, 
+            product_relation const* delta, 
+            bool is_widen) :
                 m_rmgr(tgt.get_manager()),
+                m_plugin(tgt.get_plugin()),
                 m_is_widen(is_widen) {
             SASSERT(vectors_equal(tgt.m_spec, src.m_spec));
             SASSERT(!delta || vectors_equal(tgt.m_spec, delta->m_spec));
@@ -631,6 +637,9 @@ namespace datalog {
 
         virtual void operator()(relation_base& _tgt, const relation_base& _src, relation_base* _delta) {
             TRACE("dl", _tgt.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+            SASSERT(m_plugin.check_kind(_tgt));
+            SASSERT(m_plugin.check_kind(_src));
+            SASSERT(!_delta || m_plugin.check_kind(*_delta));
             product_relation& tgt = get(_tgt);
             product_relation const& src = get(_src);
             product_relation* delta = get(_delta);
@@ -652,7 +661,7 @@ namespace datalog {
                     if (i == j) {
                         continue; //this is the basic union which we will perform later
                     }
-                    if (can_do_inner_union(i, j)) {
+                    if (can_do_inner_union(i, j) && can_do_inner_union(j, i)) {
                         TRACE("dl", itgt.display(tout << "tgt:\n"); src[j].display(tout << "src:\n"););
                         // union[i][j]
                         scoped_rel<relation_base> one_side_union = itgt.clone();
@@ -740,7 +749,7 @@ namespace datalog {
 
 
         virtual void operator()(relation_base& _tgt, const relation_base& _src, relation_base* _delta) {
-            TRACE("dl", _tgt.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+            TRACE("dl_verbose", _tgt.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
             product_relation& tgt = get(_tgt);
             product_relation const& src0 = get(_src);
             product_relation* delta = _delta ? get(_delta) : 0;
@@ -775,6 +784,7 @@ namespace datalog {
                 m_inner_union_fun(inner_union_fun) {}
 
         virtual void operator()(relation_base& tgt, const relation_base& _src, relation_base* delta) {
+            TRACE("dl", tgt.display(tout); _src.display(tout); );
             product_relation const& src = get(_src);
             (*m_inner_union_fun)(tgt, src[m_single_rel_idx], delta);
         }
@@ -788,7 +798,8 @@ namespace datalog {
             }
             return alloc(unaligned_union_fn, get(tgt), get(src), get(delta), is_widen);
         }
-        if(check_kind(src)) {
+        if (check_kind(src)) {
+            TRACE("dl", tgt.display(tout << "different kinds"); src.display(tout););
             const product_relation & p_src = get(src);
             unsigned single_idx;
             if(p_src.try_get_single_non_transparent(single_idx)) {
@@ -799,7 +810,7 @@ namespace datalog {
                 else {
                     inner = get_manager().mk_union_fn(tgt, p_src[single_idx], delta);
                 }
-                if(inner) {
+                if (inner) {
                     return alloc(single_non_transparent_src_union_fn, single_idx, inner);
                 }
             }
@@ -975,10 +986,20 @@ namespace datalog {
         func_decl* p = 0;
         const relation_signature & sig = get_signature();
         family_id new_kind = get_plugin().get_relation_kind(sig, spec);
-        if(new_kind == get_kind()) {
+        if (new_kind == get_kind()) {
             return;
         }
 
+        TRACE("dl", {
+                ast_manager& m = get_ast_manager_from_rel_manager(get_manager());
+                sig.output(m, tout); tout << "\n";
+                for (unsigned i = 0; i < spec.size(); ++i) {
+                    tout << spec[i] << " ";
+                }
+                tout << "\n";
+            }
+            );
+
         unsigned old_sz = size();
         unsigned new_sz = spec.size();
         unsigned old_remain = old_sz;
@@ -1001,10 +1022,10 @@ namespace datalog {
                 if(old_sz == 0 && m_default_empty) {
                     //The relation didn't contain any inner relations but it was empty,
                     //so we make the newly added relations empty as well.
-                    irel = get_manager().mk_empty_relation(sig, new_kind);
+                    irel = get_manager().mk_empty_relation(sig, ikind);
                 }
                 else {
-                    irel = get_manager().mk_full_relation(sig, p, new_kind);
+                    irel = get_manager().mk_full_relation(sig, p, ikind);
                 }
             }
             new_rels.push_back(irel);
@@ -1013,10 +1034,8 @@ namespace datalog {
         m_relations = new_rels;
 
         set_kind(new_kind);
-        DEBUG_CODE(
-            ensure_correct_kind();
-            SASSERT(get_kind() == new_kind);
-            );
+        m_spec = spec;
+        SASSERT(get_kind() == new_kind);        
     }
 
     bool product_relation::try_get_single_non_transparent(unsigned & idx) const {
@@ -1104,7 +1123,11 @@ namespace datalog {
     }
 
     void product_relation::display(std::ostream & out) const {
-        out<<"Product of the following relations:\n";
+        if (m_relations.empty()) {
+            out << "{}\n";
+            return;
+        }
+        out << "Product of the following relations:\n";
         for (unsigned i = 0; i < m_relations.size(); ++i) {
             m_relations[i]->display(out);
         }
diff --git a/src/muz/rel/dl_product_relation.h b/src/muz/rel/dl_product_relation.h
index 0633ddbf1..f2efd9678 100644
--- a/src/muz/rel/dl_product_relation.h
+++ b/src/muz/rel/dl_product_relation.h
@@ -27,10 +27,12 @@ namespace datalog {
 
     class product_relation;
 
+    struct rel_spec : public svector<family_id> {        
+        bool well_formed() const { return true; }
+    };
+
     class product_relation_plugin : public relation_plugin {
         friend class product_relation;
-    public:
-        typedef svector<family_id> rel_spec;
     private:
         class join_fn;
         class transform_fn;
@@ -120,8 +122,6 @@ namespace datalog {
 
 
 
-        typedef product_relation_plugin::rel_spec rel_spec;
-
         /**
            If m_relations is empty, value of this determines whether the relation is empty or full.
         */
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 9a2d0575d..b92c9f796 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -350,6 +350,7 @@ namespace datalog {
 
         //If there is no plugin to handle the signature, we just create an empty product relation and
         //stuff will be added to it by later operations.
+        TRACE("dl", s.output(get_context().get_manager(), tout << "empty product relation"); tout << "\n";);
         return product_relation_plugin::get_plugin(*this).mk_empty(s);
     }
 
@@ -756,7 +757,6 @@ namespace datalog {
 
     relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, 
             const relation_base * delta) {         
-        TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << "\n";); 
         relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta);
         if(!res && &tgt.get_plugin()!=&src.get_plugin()) {
             res = src.get_plugin().mk_union_fn(tgt, src, delta);
@@ -764,6 +764,7 @@ namespace datalog {
         if(!res && delta && &tgt.get_plugin()!=&delta->get_plugin() && &src.get_plugin()!=&delta->get_plugin()) {
             res = delta->get_plugin().mk_union_fn(tgt, src, delta);
         }
+        // TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << " " << (res?"created":"not created") << "\n";); 
         return res;
     }
 
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index f3ac4bf84..c3ffdceae 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -486,7 +486,7 @@ namespace datalog {
             target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
             break;
         default: {
-            svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
+            rel_spec rel_kinds; // kinds of plugins that are not table plugins
             family_id rel_kind;           // the aggregate kind of non-table plugins
             for (unsigned i = 0; i < relation_name_cnt; i++) {
                 relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 2be32c02d..d2360762a 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -399,7 +399,7 @@ namespace qe {
         expr_ref qt(unsigned i, expr* ctx, model_ref& model) {
             model_ref model1;
             while (true) {
-                IF_VERBOSE(1, verbose_stream() << "qt " << i << "\n";);
+                IF_VERBOSE(1, verbose_stream() << "(qt " << i << ")\n";);
                 TRACE("qe",
                       tout << i << " " << mk_pp(ctx, m) << "\n";
                       display(tout););