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

avoid platform non-reproducibility due to argument evaluation ordering

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-23 17:13:51 -08:00
parent 23c4728d68
commit 85d3041a80
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -619,9 +619,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
}
else if (lnz < bv_sz - 1 && m_le2extract) {
// a[sz-1:lnz+1] = 0 & a[lnz:0] <= b[lnz:0]
result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, a), mk_zero(bv_sz - lnz - 1)),
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
expr_ref e1(m_mk_extract(bv_sz - 1, lnz + 1, a), m);
expr_ref e2(mk_zero(bv_sz - lnz - 1), m);
expr_ref e3(m_mk_extract(lnz, 0, a), m);
expr_ref e4(m_mk_extract(lnz, 0, b), m);
expr_ref e5(m_util.mk_ule(e3, e4), m);
result = m.mk_and(m.mk_eq(e1, e2), e5);
return BR_REWRITE3;
}