mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

remove unsound simplification for rem. Codeplex Issue 76

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-02 17:24:40 -08:00
parent 4f20216677
commit 23313e5bdc
1 changed files with 1 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/arith_rewriter.cpp
View file

@ -753,12 +753,7 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
if (is_add(arg1) || is_mul(arg1)) {
ptr_buffer<expr> new_args;
unsigned num_args = to_app(arg1)->get_num_args();
for (unsigned i = 0; i < num_args; i++)
new_args.push_back(m_util.mk_rem(to_app(arg1)->get_arg(i), arg2));
result = m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr());
return BR_REWRITE2;
return BR_FAILED;
}
else {
if (v2.is_neg()) {