mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Bugfix for arith_rewriter single operand division

Browse source
This commit is contained in:
Zephyr Pellerin 2016-03-04 18:26:00 -08:00
parent 40c5152075
commit b13db1e82e
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -61,8 +61,10 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_ADD: st = mk_add_core(num_args, args, result); break; case OP_ADD: st = mk_add_core(num_args, args, result); break;
case OP_MUL: st = mk_mul_core(num_args, args, result); break; case OP_MUL: st = mk_mul_core(num_args, args, result); break;
case OP_SUB: st = mk_sub(num_args, args, result); break; case OP_SUB: st = mk_sub(num_args, args, result); break;
case OP_DIV: SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
case OP_IDIV: SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break; case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break;
case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break; case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break;
case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;