mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-28 19:01:29 +00:00
Code Activity

Fix RNE/RNA overflow-to-infinity in Real-to-FP conversion (soundness bug)

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-23 04:34:58 +00:00
parent 1c6f251062
commit c0fd3513a2
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);