diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index d23da72fb..b112f4c99 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -111,7 +111,7 @@ namespace datalog { bool rule_modified = false; for (unsigned i = 0; i < sz; i++) { app * tail = r->get_tail(i); - if (is_candidate(tail)) { + if (is_candidate(tail) && !r->is_neg_tail(i)) { TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";); var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail); func_decl * filter_decl = mk_filter_decl(tail, non_local_vars);