From 1c6f2510627bfb2e2f6bc3210e12e8d87d85625e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Feb 2026 04:11:40 +0000 Subject: [PATCH 1/2] Initial plan From c0fd3513a29301cadc3761218ba2db9d12b210ef Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Feb 2026 04:34:58 +0000 Subject: [PATCH 2/2] Fix RNE/RNA overflow-to-infinity in Real-to-FP conversion (soundness bug) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/fpa/fpa2bv_converter.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 288bcab4e..39ef06538 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2823,9 +2823,14 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn); mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz); + // IEEE 754: RNE/RNA carry all overflows to infinity with the sign of the result. + // RTP carries positive overflow to +inf, RTN carries negative overflow to -inf. + expr_ref rm_rounds_to_pinf(m), rm_rounds_to_ninf(m); + rm_rounds_to_pinf = m.mk_or(rm_tp, m.mk_or(rm_nte, rm_nta)); + rm_rounds_to_ninf = m.mk_or(rm_tn, m.mk_or(rm_nte, rm_nta)); expr_ref implies_gt_max_real(m), implies_lt_min_real(m); - implies_gt_max_real = m.mk_implies(r_is_pinf, m.mk_and(rm_tp, m_arith_util.mk_gt(x, e_max_real))); - implies_lt_min_real = m.mk_implies(r_is_ninf, m.mk_and(rm_tn, m_arith_util.mk_lt(x, e_max_real_neg))); + implies_gt_max_real = m.mk_implies(r_is_pinf, m.mk_and(rm_rounds_to_pinf, m_arith_util.mk_gt(x, e_max_real))); + implies_lt_min_real = m.mk_implies(r_is_ninf, m.mk_and(rm_rounds_to_ninf, m_arith_util.mk_lt(x, e_max_real_neg))); m_extra_assertions.push_back(implies_gt_max_real); m_extra_assertions.push_back(implies_lt_min_real);