diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp
index 75caba6ae..b65ed455c 100644
--- a/src/muz/rel/dl_mk_similarity_compressor.cpp
+++ b/src/muz/rel/dl_mk_similarity_compressor.cpp
@@ -426,7 +426,7 @@ namespace datalog {
         new_negs.push_back(false);
 
         rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), 
-            new_negs.c_ptr());
+            new_negs.c_ptr(), r->name());
         m_result_rules.push_back(new_rule);
 
         //TODO: allow for a rule to have multiple parent objects
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index e428fdd2e..a8e54085d 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -726,7 +726,7 @@ namespace datalog {
                 }
 
                 rule * new_rule = m_context.get_rule_manager().mk(orig_r->get_head(), tail.size(), tail.c_ptr(), 
-                    negs.c_ptr());
+                    negs.c_ptr(), orig_r->name());
 
                 new_rule->set_accounting_parent_object(m_context, orig_r);
                 m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule);
diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp
index aa910002d..cefda74e8 100644
--- a/src/muz/transforms/dl_mk_slice.cpp
+++ b/src/muz/transforms/dl_mk_slice.cpp
@@ -789,7 +789,7 @@ namespace datalog {
                 tail.push_back(to_app(e));                
             }
                         
-            new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);        
+            new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0, r.name());        
 
             rm.fix_unbound_vars(new_rule, false);
 
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 41b181450..78133aab7 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -173,7 +173,7 @@ namespace datalog {
             return l_false;
         }
         else {
-            rule_ref new_rule(m_context.get_rule_manager().mk(r, chead), m_context.get_rule_manager());
+            rule_ref new_rule(m_context.get_rule_manager().mk(r, chead, r->name()), m_context.get_rule_manager());
             new_rule->set_accounting_parent_object(m_context, r);
 
             m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl());