From 322e4441b3a170c9c30c747f10b1d3b0c04e2a0b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 25 Apr 2025 12:38:00 +0100 Subject: [PATCH] Fix conversion of signed 1-bit BV to FP Fixes https://github.com/AliveToolkit/alive2/issues/1193 --- 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 d138cc082..cad3a7c01 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3051,7 +3051,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const expr_ref sign_bit(m), exp_too_large(m), sig_4(m), exp_2(m), rest(m); expr_ref is_neg(m), x_abs(m), neg_x(m); sign_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x); - rest = m_bv_util.mk_extract(bv_sz - 2, 0, x); + rest = m_bv_util.mk_extract(bv_sz == 1 ? 0 : (bv_sz - 2), 0, x); dbg_decouple("fpa2bv_to_fp_signed_rest", rest); is_neg = m.mk_eq(sign_bit, bv1_1); neg_x = m_bv_util.mk_bv_neg(x); // overflow ok, x_abs is now unsigned.