mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-04 09:07:40 +00:00
Code Activity

disable bottom-up coi filtering when relations contain facts. bug reported by SeanMcL

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-15 10:53:00 -08:00
parent 3a3e1796e2
commit b8e4871d9e
2 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -41,6 +41,9 @@ namespace datalog {
bool new_tail = false;
bool contained = true;
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
if (m_context.has_facts(r->get_decl(i))) {
return 0;
}
if (r->is_neg_tail(i)) {
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
if (!new_tail) {