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

fix #7661

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-29 17:46:51 +01:00
parent 819c2079cb
commit 2714dc2623
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2811,7 +2811,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
rational min_real, max_real; rational min_real, max_real;
const mpz& max_exp_z = m_mpf_manager.m_powers2.m1(ebits-1); const mpz& max_exp_z = m_mpf_manager.m_powers2.m1(ebits-1);
SASSERT(m_mpz_manager.is_uint(max_exp_z)); if (!m_mpz_manager.is_uint(max_exp_z))
throw default_exception("exponents requiring more than 32 bits are not supported");
unsigned max_exp = m_mpz_manager.get_uint(max_exp_z); unsigned max_exp = m_mpz_manager.get_uint(max_exp_z);
rational max_sig = m_mpf_manager.m_powers2.m1(sbits) / m_mpf_manager.m_powers2(sbits-1); rational max_sig = m_mpf_manager.m_powers2.m1(sbits) / m_mpf_manager.m_powers2(sbits-1);
max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp)); max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp));