From ba820223ced2c799a4d4c1001faf84070bad0c2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 17:43:54 -0700 Subject: [PATCH] fix #3795 Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index d43a156eb..d90d4a59b 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -46,7 +46,8 @@ void rule_properties::collect(rule_set const& rules) { if (m_generate_proof && !r->get_proof()) { rm.mk_rule_asserted_proof(*r); } - for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { + + for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { sort* d = r->get_decl()->get_domain(i); sort_size sz = d->get_num_elements(); if (m_ar.is_array(d) || (!sz.is_finite() && !m_dl.is_rule_sort(d))) { @@ -203,7 +204,11 @@ void rule_properties::operator()(app* n) { } } } - + sort* s = m.get_sort(n); + sort_size sz = s->get_num_elements(); + if (m_ar.is_array(s) || (!sz.is_finite() && !m_dl.is_rule_sort(s))) { + m_inf_sort.push_back(m_rule); + } } void rule_properties::reset() {