diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index c6ffa1378..8428d9049 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -667,7 +667,7 @@ namespace datalog {
         return et->get_data().m_value;
     }
 
-    void mk_rule_inliner::add_rule(rule* r, unsigned i) {
+    void mk_rule_inliner::add_rule(rule_set const& source, rule* r, unsigned i) {
         svector<bool>& can_remove = m_head_visitor.can_remove();
         svector<bool>& can_expand = m_head_visitor.can_expand();
         app* head = r->get_head();
@@ -676,7 +676,7 @@ namespace datalog {
         m_head_index.insert(head);
         m_pinned.push_back(r);
             
-        if (m_context.get_rules().is_output_predicate(headd) ||
+        if (source.is_output_predicate(headd) ||
             m_preds_with_facts.contains(headd)) {
             can_remove.set(i, false);
             TRACE("dl", output_predicate(m_context, head, tout << "cannot remove: " << i << " "); tout << "\n";);
@@ -692,7 +692,7 @@ namespace datalog {
             tl_sz == 1
             && r->get_positive_tail_size() == 1 
             && !m_preds_with_facts.contains(r->get_decl(0)) 
-            && !m_context.get_rules().is_output_predicate(r->get_decl(0));
+            && !source.is_output_predicate(r->get_decl(0));
         can_expand.set(i, can_exp);
     }
 
@@ -709,7 +709,7 @@ namespace datalog {
 
 #define PRT(_x_) ((_x_)?"T":"F")
 
-    bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
+    bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
         scoped_ptr<rule_set> res = alloc(rule_set, m_context);
         bool done_something = false;        
         unsigned sz = rules->get_num_rules();
@@ -731,7 +731,7 @@ namespace datalog {
         svector<bool>& can_expand = m_head_visitor.can_expand();
 
         for (unsigned i = 0; i < sz; ++i) {
-            add_rule(acc[i].get(), i);
+            add_rule(source, acc[i].get(), i);
         }
 
         // initialize substitution.
@@ -808,7 +808,7 @@ namespace datalog {
                 TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
 
                 del_rule(r, i);
-                add_rule(rl_res.get(), i);
+                add_rule(source, rl_res.get(), i);
                 
 
                 r = rl_res;
@@ -875,7 +875,7 @@ namespace datalog {
             TRACE("dl", res->display(tout << "after eager inlining\n"););
         }
 
-        if (m_context.get_params().inline_linear() && inline_linear(res)) {
+        if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
             something_done = true;
         }
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index bec788ffe..476c6b4b0 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -172,9 +172,9 @@ namespace datalog {
         /**
            Inline predicates that are known to not be join-points.
          */
-        bool inline_linear(scoped_ptr<rule_set>& rules);
+        bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
 
-        void add_rule(rule* r, unsigned i);
+        void add_rule(rule_set const& rule_set, rule* r, unsigned i);
         void del_rule(rule* r, unsigned i);
 
     public:
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp
index 969f1444a..040cbfa78 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.cpp
+++ b/src/muz_qe/dl_mk_similarity_compressor.cpp
@@ -429,7 +429,7 @@ namespace datalog {
         m_modified = true;
     }
 
-    void mk_similarity_compressor::process_class(rule_vector::iterator first, 
+    void mk_similarity_compressor::process_class(rule_set const& source, rule_vector::iterator first, 
             rule_vector::iterator after_last) {
         SASSERT(first!=after_last);
         //remove duplicates
@@ -487,7 +487,7 @@ namespace datalog {
         //TODO: compress also rules with pairs (or tuples) of equal constants
 
 #if 1
-        if (const_cnt>0) {
+        if (const_cnt>0 && !source.is_output_predicate((*first)->get_decl())) {
             unsigned rule_cnt = static_cast<unsigned>(after_last-first);
             if (rule_cnt>m_threshold_count) {
                 merge_class(first, after_last);
@@ -521,7 +521,7 @@ namespace datalog {
             rule_vector::iterator prev = it;
             ++it;
             if (it==end || rough_compare(*prev, *it)!=0) {
-                process_class(cl_begin, it);
+                process_class(source, cl_begin, it);
                 cl_begin = it;
             }
         }
diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz_qe/dl_mk_similarity_compressor.h
index 6e0ca9db5..49704b8cd 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.h
+++ b/src/muz_qe/dl_mk_similarity_compressor.h
@@ -63,7 +63,7 @@ namespace datalog {
         ast_ref_vector      m_pinned;
         
         void merge_class(rule_vector::iterator first, rule_vector::iterator after_last);
-        void process_class(rule_vector::iterator first, rule_vector::iterator after_last);
+        void process_class(rule_set const& source, rule_vector::iterator first, rule_vector::iterator after_last);
 
         void reset();
     public:
diff --git a/src/muz_qe/dl_rule_set.cpp b/src/muz_qe/dl_rule_set.cpp
index b0bcdec89..cb129ab37 100644
--- a/src/muz_qe/dl_rule_set.cpp
+++ b/src/muz_qe/dl_rule_set.cpp
@@ -332,15 +332,12 @@ namespace datalog {
 
     void rule_set::inherit_predicates(rule_set const& other) {
         m_refs.append(other.m_refs);
-        SASSERT(m_refs.size() < 1000);
         set_union(m_output_preds, other.m_output_preds);
         {
             obj_map<func_decl, func_decl*>::iterator it = other.m_orig2pred.begin();
             obj_map<func_decl, func_decl*>::iterator end = other.m_orig2pred.end();
             for (; it != end; ++it) {
                 m_orig2pred.insert(it->m_key, it->m_value);
-                m_refs.push_back(it->m_key);
-                m_refs.push_back(it->m_value);
             }
         }
         {
@@ -348,8 +345,6 @@ namespace datalog {
             obj_map<func_decl, func_decl*>::iterator end = other.m_pred2orig.end();
             for (; it != end; ++it) {
                 m_pred2orig.insert(it->m_key, it->m_value);
-                m_refs.push_back(it->m_key);
-                m_refs.push_back(it->m_value);
             }
         }
     }
@@ -515,6 +510,11 @@ namespace datalog {
     void rule_set::display(std::ostream & out) const {
         out << "; rule count: " << get_num_rules() << "\n";
         out << "; predicate count: " << m_head2rules.size() << "\n";
+        func_decl_set::iterator pit = m_output_preds.begin();
+        func_decl_set::iterator pend = m_output_preds.end();
+        for (; pit != pend; ++pit) {
+            out << "; output: " << (*pit)->get_name() << '\n';
+        }
         decl2rules::iterator it  = m_head2rules.begin();
         decl2rules::iterator end = m_head2rules.end();
         for (; it != end; ++it) {
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index 327e63c0f..00181b18c 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -253,6 +253,8 @@ namespace datalog {
             m_context.transform_rules(alloc(mk_magic_sets, m_context, query_pred));
         }
 
+        query_pred = m_context.get_rules().get_pred(query_pred);
+
         lbool res = saturate();
         
         if (res != l_undef) {