mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Fix error messsages

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2021-09-14 11:44:39 +00:00
parent c3549ec784
commit 12c32663c6
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -465,7 +465,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
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");
throw default_exception("addition/subtract with ebits > sbits not supported");
expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m);
@ -950,7 +950,7 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
if (ebits > sbits)
throw default_exception("there is no floating point support for division for representations with non-standard bit representations");
throw default_exception("division with ebits > sbits not supported");
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);