From 76c59cb85c0637c32989f40a85c8c5364afb3e8f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jun 2013 17:22:25 +0100 Subject: [PATCH] MPF conversion bugfix. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 12 ++++++++---- src/util/mpf.cpp | 2 +- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 015bce0ed..367fa3a4c 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -83,17 +83,21 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c rational q; mpf q_mpf; if (m_util.au().is_numeral(args[1], q)) { + TRACE("fp_rewriter", tout << "q: " << q << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (m_util.is_value(args[1], q_mpf)) { + else if (m_util.is_value(args[1], q_mpf)) { + TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q_mpf); result = m_util.mk_value(v); m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else @@ -117,11 +121,11 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c return BR_FAILED; TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";); - mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index def9f4fd5..735d21c99 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode o.ebits = ebits; o.sbits = sbits; - signed ds = sbits - x.sbits + 4; // plus rounding bits + signed ds = sbits - x.sbits + 3; // plus rounding bits if (ds > 0) { m_mpz_manager.mul2k(o.significand, ds);