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

fix #3795

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 17:43:54 -07:00
parent 6d12540ceb
commit ba820223ce
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/muz/base/rule_properties.cpp
View file

@ -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() {