From a1073206f999b683f0770fb9a2882f7a682f5492 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Sep 2015 16:23:24 +0100 Subject: [PATCH] Bugfix for FP rewriter. --- src/ast/rewriter/fpa_rewriter.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 1d12621cd..d004273d1 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -739,7 +739,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ m_util.is_numeral(arg2, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { - result = m_util.mk_internal_to_ubv_unspecified(bv_sz); + mk_to_ubv_unspecified(f, result); return BR_REWRITE_FULL; } @@ -754,7 +754,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ if (r >= ll && r <= ul) result = bu.mk_numeral(r, bv_sz); else - result = m_util.mk_internal_to_ubv_unspecified(bv_sz); + mk_to_ubv_unspecified(f, result); return BR_DONE; } @@ -772,7 +772,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ m_util.is_numeral(arg2, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - result = m_util.mk_internal_to_sbv_unspecified(bv_sz); + mk_to_sbv_unspecified(f, result); return BR_REWRITE_FULL; } @@ -787,7 +787,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ if (r >= ll && r <= ul) result = bu.mk_numeral(r, bv_sz); else - result = m_util.mk_internal_to_sbv_unspecified(bv_sz); + mk_to_sbv_unspecified(f, result); return BR_DONE; }