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

fixes for #4634

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 08:45:22 -07:00
parent c41abf2241
commit 72d140334f
2 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.cpp
View file

@ -645,6 +645,7 @@ namespace datatype {
SASSERT(is_datatype(s));
bool fi = true;
return fi;
#if 0
if (m_is_fully_interp.find(s, fi)) {
return fi;
}
@ -671,6 +672,7 @@ namespace datatype {
m_is_fully_interp.insert(s, is_interp);
m_asts.push_back(s);
return true;
#endif
}
/**

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

@ -1172,9 +1172,11 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
m_mpz_manager.set(remaining, max_exp_diff_adj);
while (m_mpz_manager.gt(remaining, INT32_MAX)) {
throw default_exception("zero extension overflow floating point types are too large");
#if 0
edr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, edr_tmp);
nedr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, nedr_tmp);
m_mpz_manager.sub(remaining, INT32_MAX, remaining);
#endif
}
if (!m_mpz_manager.is_zero(remaining)) {
edr_tmp = m_bv_util.mk_zero_extend(m_mpz_manager.get_uint(remaining), edr_tmp);