From db6b9faabca20648ce57447bc7811d9873d5961d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:35:45 +0000 Subject: [PATCH] Bugfix for FPA rewriter. --- src/ast/rewriter/fpa_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 83372bcf4..5a25e11ec 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -130,7 +130,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, ebits+sbits); + result = bu.mk_numeral(0, width); else result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); @@ -149,7 +149,7 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, ebits+sbits); + result = bu.mk_numeral(0, width); else result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);