diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index d138685ed..93769a3b4 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1430,14 +1430,22 @@ ast_manager::~ast_manager() {
         for (; it_a != end_a; ++it_a) {
             ast* n = (*it_a);
             switch (n->get_kind()) {
-            case AST_SORT:
-                mark_array_ref(mark, to_sort(n)->get_info()->get_num_parameters(), to_sort(n)->get_info()->get_parameters());
+            case AST_SORT: {
+                sort_info* info = to_sort(n)->get_info();
+                if (info != 0) {
+                    mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
+                }
                 break;
-            case AST_FUNC_DECL:
-                mark_array_ref(mark, to_func_decl(n)->get_info()->get_num_parameters(), to_func_decl(n)->get_info()->get_parameters());
+            }
+            case AST_FUNC_DECL: {
+                func_decl_info* info = to_func_decl(n)->get_info();
+                if (info != 0) {
+                    mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
+                }
                 mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
                 mark.mark(to_func_decl(n)->get_range(), true);
                 break;
+            }
             case AST_APP:
                 mark.mark(to_app(n)->get_decl(), true);
                 mark_array_ref(mark, to_app(n)->get_num_args(), to_app(n)->get_args());
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index c452e2611..e3d01a537 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -44,6 +44,9 @@ namespace datalog {
                 if (m_context.has_facts(r->get_decl(i))) {
                     return 0;
                 }
+                if (false && r->is_neg_tail(i)) {
+                    return 0;
+                }
                 if (r->is_neg_tail(i)) {
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         if (!new_tail) {
@@ -53,11 +56,13 @@ namespace datalog {
                             }
                             new_tail = true;
                         }
-                    } else if (new_tail) {
+                    } 
+                    else if (new_tail) {
                         m_new_tail.push_back(r->get_tail(i));
                         m_new_tail_neg.push_back(true);
                     }
-                } else {
+                } 
+                else {
                     SASSERT(!new_tail);
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         contained = false;