From 5159291d573e18d582c813bc10a59f6c6327c1e3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jan 2018 19:29:42 -0800 Subject: [PATCH] add missing interpreted tail during bottom-up simplification #1452 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 3ea0e305a..2ca64aa68 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -79,6 +79,10 @@ namespace datalog { } if (contained) { if (new_tail) { + for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) { + m_new_tail.push_back(r->get_tail(i)); + m_new_tail_neg.push_back(false); + } rule* new_r = m_context.get_rule_manager().mk(r->get_head(), m_new_tail.size(), m_new_tail.c_ptr(), m_new_tail_neg.c_ptr(), symbol::null, false); res->add_rule(new_r);