diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b29a9c87d..94e20eceb 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5668,7 +5668,8 @@ END_MLAPI_EXCLUDE
        Each conjunct encodes values of the bound variables of the query that are satisfied.
        In PDR mode, the returned answer is a single conjunction.
 
-       The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+       When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+       When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
 
        def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
     */    
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 218f9906a..a6647a1d2 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -290,7 +290,7 @@ namespace datalog {
                 }
             }
             TRACE("dl_dr", 
-                  tout << r.get_decl()->get_name() << "\n";
+                  tout << mk_pp(r.get_head(), m) << " :- \n";
                   for (unsigned i = 0; i < body.size(); ++i) {
                       tout << mk_pp(body[i].get(), m) << "\n";
                   });
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index d9dad5c56..712c82feb 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -423,6 +423,11 @@ namespace datalog {
         }
 
         TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules;  );
+
+        for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
+            rule* r = m_inlined_rules.get_rule(i);
+            datalog::del_rule(m_mc, *r);
+        }
     }
 
     bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {