From 2673807a7f1eac9fc4d890a426360d111806f48a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 18:34:15 -0700 Subject: [PATCH] fix #3863 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_rule_set.cpp | 9 ++++----- src/muz/fp/horn_tactic.cpp | 2 ++ 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index 04f50a53e..0e5145f66 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -394,19 +394,18 @@ namespace datalog { */ bool rule_set::stratified_negation() { ptr_vector::const_iterator it = m_rules.c_ptr(); - ptr_vector::const_iterator end = m_rules.c_ptr()+m_rules.size(); + ptr_vector::const_iterator end = m_rules.c_ptr() + m_rules.size(); for (; it != end; it++) { rule * r = *it; - app * head = r->get_head(); - func_decl * head_decl = head->get_decl(); + func_decl * head_decl = r->get_decl(); unsigned n = r->get_uninterpreted_tail_size(); for (unsigned i = r->get_positive_tail_size(); i < n; i++) { SASSERT(r->is_neg_tail(i)); - func_decl * tail_decl = r->get_tail(i)->get_decl(); + func_decl * tail_decl = r->get_decl(i); unsigned neg_strat = get_predicate_strat(tail_decl); unsigned head_strat = get_predicate_strat(head_decl); - SASSERT(head_strat>=neg_strat); //head strat can never be lower than that of a tail + SASSERT(head_strat >= neg_strat); // head strat can never be lower than that of a tail if (head_strat == neg_strat) { return false; } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index b8485a1f7..b15171e88 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -358,6 +358,8 @@ class horn_tactic : public tactic { not_supported("xform.instantiate_arrays"); if (p.xform_magic()) not_supported("xform.magic"); + if (p.xform_quantify_arrays()) + not_supported("xform.quantify_arrays"); } void not_supported(char const* s) {