mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Bugfix for FP to_fp from non-numeral reals.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-29 14:49:26 +01:00
parent 85419ca503
commit d35ebd6e57
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2312,7 +2312,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_ite(rm_nta, v1, result, result);
}
}
else {
else {
SASSERT(!m_arith_util.is_numeral(x));
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2330,12 +2331,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
expr_ref rme(rm, m);
round(s, rme, sgn, sig, exp, result);
expr_ref c0(m);
mk_is_zero(x, c0);
mk_ite(c0, x, result, result);
expr * e = m.mk_eq(m_util.mk_to_real(result), x);
m_extra_assertions.push_back(e);
m_extra_assertions.push_back(e);
}
SASSERT(is_well_sorted(m, result));