From 8871cb120a6bb74f40c3b1911d614cddf7e6e0ce Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 17 Sep 2017 12:57:29 +0100
Subject: [PATCH] Fixed bug in fp.to_{s,u}bv
---
src/ast/fpa/fpa2bv_converter.cpp | 15 ++++++---------
1 file changed, 6 insertions(+), 9 deletions(-)
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index cd3b0ccca..cae357a32 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3240,10 +3240,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m), unspec_v(m);
- if (!is_signed)
- c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
- else
- c1 = m.mk_or(x_is_nan, x_is_inf);
+ c1 = m.mk_or(x_is_nan, x_is_inf);
mk_to_bv_unspecified(f, num, args, unspec_v);
v1 = unspec_v;
dbg_decouple("fpa2bv_to_bv_c1", c1);
@@ -3335,18 +3332,18 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
dbg_decouple("fpa2bv_to_bv_inc", inc);
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
- expr_ref in_range(m);
+ pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
+
+ expr_ref ll(m), ul(m), in_range(m);
if (!is_signed) {
- expr_ref ul(m);
+ ll = m_bv_util.mk_numeral(0, bv_sz+3);
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
- in_range = m_bv_util.mk_ule(pre_rounded, ul);
}
else {
- expr_ref ll(m), ul(m);
ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
- in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
}
+ in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
dbg_decouple("fpa2bv_to_bv_in_range", in_range);
expr_ref rounded(m);