diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 57e4ba8cb..221832fed 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1438,8 +1438,9 @@ namespace datalog {
         m_ctx.ensure_opened();
         m_rules.reset();
         datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
-        datalog::rule_set old_rules(m_ctx.get_rules());
-        rule_manager.mk_query(query, m_ctx.get_rules());
+        rule_set& rules0 = m_ctx.get_rules();
+        datalog::rule_set old_rules(rules0);
+        rule_manager.mk_query(query, rules0);
         expr_ref bg_assertion = m_ctx.get_background_assertion();        
         apply_default_transformation(m_ctx);
         
@@ -1449,12 +1450,14 @@ namespace datalog {
             transformer.register_plugin(slice);
             m_ctx.transform_rules(transformer);
         }
-        if (m_ctx.get_rules().get_output_predicates().empty()) {
+
+        const rule_set& rules = m_ctx.get_rules();
+        if (rules.get_output_predicates().empty()) {
             return l_false;
         }
 
-        m_query_pred = m_ctx.get_rules().get_output_predicate();
-        m_rules.replace_rules(m_ctx.get_rules());
+        m_query_pred = rules.get_output_predicate();
+        m_rules.replace_rules(rules);
         m_rules.close();
         m_ctx.reopen();
         m_ctx.replace_rules(old_rules);
diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp
index d15172e22..acc38f9e6 100644
--- a/src/muz/clp/clp_context.cpp
+++ b/src/muz/clp/clp_context.cpp
@@ -70,11 +70,11 @@ namespace datalog {
             m_goals.reset();
             rm.mk_query(query, m_ctx.get_rules());
             apply_default_transformation(m_ctx);
-            if (m_ctx.get_rules().get_output_predicates().empty()) {
+            const rule_set& rules = m_ctx.get_rules();
+            if (rules.get_output_predicates().empty()) {
                 return l_false;
             }
-            func_decl* head_decl = m_ctx.get_rules().get_output_predicate();
-            rule_set& rules = m_ctx.get_rules();
+            func_decl *head_decl = rules.get_output_predicate();
             rule_vector const& rv = rules.get_predicate_rules(head_decl);
             if (rv.empty()) {
                 return l_false;
diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp
index b75be70c1..0a05d1ff3 100644
--- a/src/muz/pdr/pdr_dl_interface.cpp
+++ b/src/muz/pdr/pdr_dl_interface.cpp
@@ -84,10 +84,11 @@ lbool dl_interface::query(expr * query) {
     m_pred2slice.reset();
     ast_manager& m =                      m_ctx.get_manager();
     datalog::rule_manager& rm = m_ctx.get_rule_manager();
+    datalog::rule_set& rules0 = m_ctx.get_rules();
 
-    datalog::rule_set        old_rules(m_ctx.get_rules());
+    datalog::rule_set        old_rules(rules0);
     func_decl_ref            query_pred(m);
-    rm.mk_query(query, m_ctx.get_rules());
+    rm.mk_query(query, rules0);
     expr_ref bg_assertion = m_ctx.get_background_assertion();
 
     check_reset();
@@ -136,15 +137,16 @@ lbool dl_interface::query(expr * query) {
         }
     }
 
-    if (m_ctx.get_rules().get_output_predicates().empty()) {
+    const datalog::rule_set& rules = m_ctx.get_rules();
+    if (rules.get_output_predicates().empty()) {
         m_context->set_unsat();
         return l_false;
     }
 
-    query_pred = m_ctx.get_rules().get_output_predicate();
+    query_pred = rules.get_output_predicate();
 
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););
-    m_pdr_rules.replace_rules(m_ctx.get_rules());
+    m_pdr_rules.replace_rules(rules);
     m_pdr_rules.close();
     m_ctx.record_transformed_rules();
     m_ctx.reopen();
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index d2a2f0181..c6b47f1ed 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -241,12 +241,13 @@ namespace datalog {
 
         switch(res) {
         case l_true: {
+            const rule_set& rules = m_context.get_rules();
             expr_ref_vector ans(m);
             expr_ref e(m);
             bool some_non_empty = num_rels == 0;
             bool is_approx = false;
             for (unsigned i = 0; i < num_rels; ++i) {
-                func_decl* q = m_context.get_rules().get_pred(rels[i]);
+                func_decl* q = rules.get_pred(rels[i]);
                 relation_base& rel = get_relation(q);
                 if (!rel.empty()) {
                     some_non_empty = true;
@@ -383,7 +384,8 @@ namespace datalog {
     }
 
     void rel_context::reset_negated_tables() {
-        rule_set::pred_set_vector const & pred_sets = m_context.get_rules().get_strats();
+        const rule_set& all_rules = m_context.get_rules();
+        rule_set::pred_set_vector const & pred_sets = all_rules.get_strats();
         bool non_empty = false;
         for (unsigned i = 1; i < pred_sets.size(); ++i) {
             func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
@@ -411,7 +413,7 @@ namespace datalog {
                     if (depends_on_negation.contains(pred)) {
                         continue;
                     }
-                    rule_vector const& rules = m_context.get_rules().get_predicate_rules(pred);
+                    rule_vector const& rules = all_rules.get_predicate_rules(pred);
                     bool inserted = false;
                     for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
                         rule* r = rules[j];