From 2cbeedec690fbd89da1a4154ae96708af77cfe65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 May 2017 19:32:43 -0700 Subject: [PATCH] accept hereditarily finite sorts in datalog engine Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 619f88e3b..518e848c4 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -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); } }