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

fix #3869

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 17:18:55 -07:00
parent 9f1a2e2c94
commit 4bfcc75ed4
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/arith_decl_plugin.cpp
View file

@ -799,26 +799,26 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
rational r;
if (is_decl_of(f, m_afid, OP_DIV) && is_numeral(args[1], r) && r.is_zero()) {
if (is_decl_of(f, m_afid, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
f_out = mk_div0();
return true;
}
if (is_decl_of(f, m_afid, OP_IDIV) && is_numeral(args[1], r) && r.is_zero()) {
if (is_decl_of(f, m_afid, OP_IDIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
return true;
}
if (is_decl_of(f, m_afid, OP_MOD) && is_numeral(args[1], r) && r.is_zero()) {
if (is_decl_of(f, m_afid, OP_MOD) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int());
return true;
}
if (is_decl_of(f, m_afid, OP_REM) && is_numeral(args[1], r) && r.is_zero()) {
if (is_decl_of(f, m_afid, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int());
return true;
}
if (is_decl_of(f, m_afid, OP_POWER) && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) {
if (is_decl_of(f, m_afid, OP_POWER) && n == 2 && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) {
f_out = is_int(args[0]) ? mk_ipower0() : mk_rpower0();
return true;
}