mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix #3499

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-23 13:36:58 -07:00
parent b34f72dd00
commit 28bdda326b
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -461,6 +461,9 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
big_d_sig = m_bv_util.mk_concat(d_sig, m_bv_util.mk_numeral(0, sbits+3));
SASSERT(is_well_sorted(m, big_d_sig));
if (ebits > sbits)
throw default_exception("there is no floating point support for division for representations with non-standard bit representations");
expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m);
shifted_big = m_bv_util.mk_bv_lshr(big_d_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+3))-ebits), exp_delta));