From 7c4b2b04a7f8a24c0338153781e2029eb575be69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Sep 2013 08:54:02 -0700 Subject: [PATCH] fix coi-filter to not ignore relational tables Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index fc4c411ff..8583fbe45 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -52,10 +52,14 @@ namespace datalog { ptr_vector todo; rule_set::decl2rules body2rules; // initialization for reachability + rel_context_base* rc = m_context.get_rel_context(); for (rule_set::iterator it = source.begin(); it != source.end(); ++it) { rule * r = *it; all.insert(r->get_decl()); - if (r->get_uninterpreted_tail_size() == 0) { + bool non_empty = + (rc && !rc->is_empty_relation(r->get_decl())) || + r->get_uninterpreted_tail_size() == 0; + if (non_empty) { if (!reached.contains(r->get_decl())) { reached.insert(r->get_decl()); todo.insert(r->get_decl());