From bd00d98398b8dbeb45a78fb128e7e5dddb324fc3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 5 Apr 2018 17:21:17 +0100 Subject: [PATCH] Fixed overflow bug in fp.to_ubv. Thanks to Florian Schanda for reporting this bug. --- src/ast/fpa/fpa2bv_converter.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7344f6f2f..2b09dfe8c 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3243,8 +3243,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr_ref ul(m), ovfl(m), in_range(m); if (!is_signed) { + expr_ref incd(m), pr_is_zero(m); + incd = m.mk_eq(rounding_decision, bv1); + pr_is_zero = m.mk_eq(pre_rounded, 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.mk_and(m.mk_not(x_is_neg), m_bv_util.mk_ule(pre_rounded, ul)); + in_range = m.mk_and(m.mk_not(x_is_neg), + m.mk_not(m.mk_and(incd, pr_is_zero)), + m_bv_util.mk_ule(pre_rounded, ul)); } else { expr_ref ll(m);