diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 3e933b099..d9dad5c56 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -527,6 +527,9 @@ namespace datalog { bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) { + if (r->has_negation()) { + return false; + } SASSERT(rules.is_closed()); const rule_stratifier& strat = rules.get_stratifier();