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

FPA rewriter bugfix

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-31 14:48:45 +00:00
parent 2258988b37
commit 4d18e24fb4
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/float_rewriter.cpp
View file

@ -587,9 +587,14 @@ br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) {
scoped_mpf fv(m_util.fm());
if (m_util.is_value(arg1, fv)) {
scoped_mpq r(m_fm.mpq_manager());
m_fm.to_rational(fv, r);
result = m_util.au().mk_numeral(r.get(), false);
if (m_fm.is_nan(fv) || m_fm.is_inf(fv)) {
result = m_util.mk_internal_to_real_unspecified();
}
else {
scoped_mpq r(m_fm.mpq_manager());
m_fm.to_rational(fv, r);
result = m_util.au().mk_numeral(r.get(), false);
}
return BR_DONE;
}