diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 518e848c4..247519d63 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -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);
             }
         }