mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Bugfix for bvurem0 model evaluation (+1 rewriting step)

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-17 13:09:52 +00:00
parent 22cae143b1
commit c8af48d7ef
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bv_rewriter.cpp
View file

@ -892,7 +892,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) { if (r2.is_zero()) {
if (!hi_div0) { if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BUREM0, arg1); result = m().mk_app(get_fid(), OP_BUREM0, arg1);
return BR_DONE; return BR_REWRITE1;
} }
else { else {
// The "hardware interpretation" for (bvurem x 0) is x // The "hardware interpretation" for (bvurem x 0) is x