From 01f64898922564a550574d936c517675da150fba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 May 2019 16:22:49 -0700 Subject: [PATCH] fix #2310 Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 315765acc..b53996aed 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -190,11 +190,21 @@ void rule_properties::operator()(app* n) { sort* s = m.get_sort(n->get_arg(0)); SASSERT(m_dt.is_datatype(s)); if (m_dt.get_datatype_constructors(s)->size() > 1) { - m_uninterp_funs.insert(n->get_decl(), m_rule); + bool found = false; + func_decl * c = m_dt.get_accessor_constructor(n->get_decl()); + unsigned ut_size = m_rule->get_uninterpreted_tail_size(); + unsigned t_size = m_rule->get_tail_size(); + for (unsigned i = ut_size; !found && i < t_size; ++i) { + app* t = m_rule->get_tail(i); + if (m_dt.is_recognizer(t) && t->get_arg(0) == n->get_arg(0) && m_dt.get_recognizer_constructor(t->get_decl()) == c) { + found = true; + } + } + if (!found) { + m_uninterp_funs.insert(n->get_decl(), m_rule); + } } } - else { - } }