From 64d085c18886221038b136e6a1bbfbff4e4726a6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 Feb 2019 14:02:30 +0000 Subject: [PATCH] Fix bug in fpa2bv_converter, fixes #2136. --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1dc13ff9e..eef2452db 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3300,11 +3300,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args 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_bv_neg(m_bv_util.mk_numeral(1, bv_sz-1))); ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz + 3)))); + pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); in_range = m.mk_and(m.mk_not(ovfl), m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)); dbg_decouple("fpa2bv_to_bv_in_range_ll", ll); - pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); } dbg_decouple("fpa2bv_to_bv_in_range_ovfl", ovfl); dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);