From e8d85f91d7246f62825e72e42eff9b2107efaa99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jun 2016 20:08:13 -0700 Subject: [PATCH] disable filtering on negated tails. Issue #634 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_filter_rules.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);