diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index fc4c411ff..8583fbe45 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -52,10 +52,14 @@ namespace datalog {
         ptr_vector<func_decl> todo;
         rule_set::decl2rules body2rules;
         // initialization for reachability
+            rel_context_base* rc = m_context.get_rel_context();
         for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
             rule * r = *it;
             all.insert(r->get_decl());
-            if (r->get_uninterpreted_tail_size() == 0) {
+            bool non_empty = 
+                (rc && !rc->is_empty_relation(r->get_decl())) ||
+                r->get_uninterpreted_tail_size() == 0;
+            if (non_empty) {
                 if (!reached.contains(r->get_decl())) {
                     reached.insert(r->get_decl());
                     todo.insert(r->get_decl());
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index d0aafb896..d63f0ae00 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -482,7 +482,7 @@ namespace qe {
         }
 
         void nnf_iff(app* a, bool p) {
-            SASSERT(m.is_iff(a) || m.is_xor(a));
+            SASSERT(m.is_iff(a) || m.is_xor(a) || m.is_eq(a));
             expr* a0 = a->get_arg(0);
             expr* a1 = a->get_arg(1);
 
@@ -616,7 +616,7 @@ namespace qe {
                 else if (m.is_ite(a)) {
                     nnf_ite(a, p);
                 }
-                else if (m.is_iff(a)) {
+                else if (m.is_iff(a) || (m.is_eq(a) && m.is_bool(a->get_arg(0)))) {
                     nnf_iff(a, p);
                 }
                 else if (m.is_xor(a)) {
@@ -1926,6 +1926,7 @@ namespace qe {
                     plugin(x).get_num_branches(contains(x), fml, num_branches)) {
                     return true;
                 }
+                TRACE("qe", tout << "setting variable " << mk_pp(x, m) << " free\n";);
                 m_free_vars.push_back(x);
                 m_current->del_var(x);
             }
@@ -2493,6 +2494,7 @@ namespace qe {
 
         // callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml'
         virtual void elim_var(unsigned idx, expr* fml, expr* def) {
+            TRACE("qe", tout << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << "\n";);
             *m_fml = fml;
             m_vars->set(idx, m_vars->get(m_vars->size()-1));
             m_vars->pop_back();