mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

fix #3872

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 17:12:14 -07:00
parent db3d6d7c95
commit 9f1a2e2c94
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/base/rule_properties.cpp
View file

@ -182,6 +182,8 @@ void rule_properties::operator()(quantifier* n) {
} }
void rule_properties::operator()(app* n) { void rule_properties::operator()(app* n) {
func_decl_ref f_out(m); func_decl_ref f_out(m);
expr* n1 = nullptr, *n2 = nullptr;
rational r;
if (m_is_predicate(n)) { if (m_is_predicate(n)) {
insert(m_interp_pred, m_rule); 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)) { 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); 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)); check_sort(m.get_sort(n));
} }