From 4d18e24fb4ee28431cdbe7461ae611473076895c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 31 Dec 2014 14:48:45 +0000 Subject: [PATCH] FPA rewriter bugfix Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 522fad678..96561395e 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -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; }