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

fpa warning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 00:55:13 -07:00
parent 9e374d6514
commit 399cf75ad4
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1162,7 +1162,6 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
m_mpz_manager.add(max_exp_diff_adj, 1, max_exp_diff_adj);
expr_ref edr_tmp = exp_diff, nedr_tmp = neg_exp_diff;
m_mpz_manager.set(remaining, max_exp_diff_adj);
unsigned num_rounds = 0;
while (m_mpz_manager.gt(remaining, INT32_MAX)) {
throw default_exception("zero extension overflow floating point types are too large");
edr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, edr_tmp);