mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
accept hereditarily finite sorts in datalog engine
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
622d8c951c
commit
2cbeedec69
|
@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) {
|
|||
}
|
||||
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
|
||||
sort* d = r->get_decl()->get_domain(i);
|
||||
if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
|
||||
sort_size sz = d->get_num_elements();
|
||||
if (!sz.is_finite()) {
|
||||
m_inf_sort.push_back(m_rule);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue