From e8cdc34219befa3d583d82ec534ce16e733a865f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 22:34:26 +0100 Subject: [PATCH] Debug fix in fpa2bv converter. Relates to #872. --- 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 1217d365c..1a4698fa4 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1667,7 +1667,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg); // Result could have overflown into 4.xxx. - SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+4); + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+5); expr_ref extra(m), extra_is_zero(m); extra = m_bv_util.mk_extract(2*sbits+4, 2*sbits+3, sig_abs); extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2));