mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-10 07:51:20 +00:00
Code Activity

fpa: remove redundant underflow width alias

Browse source
This commit is contained in:
1sgtpepper 2026-08-09 10:42:59 +08:00
parent f53309c7bc
commit 024747d80e
No known key found for this signature in database
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1145,9 +1145,8 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
m_simp.mk_ite(shift_is_deep, all_discarded, discarded_shifted, discarded);
expr_ref sticky_ext(m), underflow_sig(m);
unsigned underflow_sig_low_bit = sig_extract_low_bit;
underflow_sig = m_bv_util.mk_extract(
2 * sig_size - 1, underflow_sig_low_bit, shifted_sig);
2 * sig_size - 1, sig_extract_low_bit, shifted_sig);
sticky_ext = m_bv_util.mk_zero_extend(sbits + 1, discarded);
underflow_sig = m_bv_util.mk_bv_or({underflow_sig, sticky_ext});