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

Merge pull request #8737 from Z3Prover/copilot/fix-refutational-soundness-bug

Browse source 
Fix soundness bug: RNE/RNA overflow to ±infinity in symbolic Real-to-FP conversion
This commit is contained in:
Nikolaj Bjorner 2026-02-25 13:34:59 -08:00 • committed by GitHub
commit fba1e4b648
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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);