mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix check for finite sorts #1122
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ea331ebfbe
commit
5714f830b0
|
@ -51,7 +51,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);
|
||||
sort_size sz = d->get_num_elements();
|
||||
if (!sz.is_finite()) {
|
||||
if (!sz.is_finite() && !m_dl.is_rule_sort(d)) {
|
||||
TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";);
|
||||
m_inf_sort.push_back(m_rule);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue