diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index f78914b1c..ba85e569a 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -133,9 +133,11 @@ namespace datalog { if (engine.get_fact(pred).is_reachable()) should_keep = true; else if (m_context.get_model_converter()) { - for (rule* pr : source.get_predicate_rules(pred)) + for (rule* pr : source.get_predicate_rules(pred)) for (unsigned i = 0; i < pr->get_uninterpreted_tail_size(); ++i) - should_keep |= pr->get_tail(i)->get_decl() != pred; + if (pr->get_tail(i)->get_decl() != pred) + // don't try to eliminate across predicates + return nullptr; } else continue;