From 9f1a2e2c9432dea960fc0dfe91ee67783c996ef6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 17:12:14 -0700 Subject: [PATCH] fix #3872 Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 28c2f7dfe..f8f6a6f53 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -182,6 +182,8 @@ void rule_properties::operator()(quantifier* n) { } void rule_properties::operator()(app* n) { func_decl_ref f_out(m); + expr* n1 = nullptr, *n2 = nullptr; + rational r; if (m_is_predicate(n)) { insert(m_interp_pred, m_rule); } @@ -210,6 +212,11 @@ void rule_properties::operator()(app* n) { else if (m_a.is_considered_uninterpreted(n->get_decl(), n->get_num_args(), n->get_args(), f_out)) { m_uninterp_funs.insert(n->get_decl(), m_rule); } + else if ((m_a.is_mod(n, n1, n2) || m_a.is_div(n, n1, n2) || + m_a.is_idiv(n, n1, n2) || m_a.is_rem(n, n1, n2)) + && (!m_a.is_numeral(n2, r) || r.is_zero())) { + m_uninterp_funs.insert(n->get_decl(), m_rule); + } check_sort(m.get_sort(n)); }