Repository navigation

[WIP] Floating-point fixes - #8912

Draft

tautschnig wants to merge 62 commits into

diffblue:developfrom

tautschnig:fp-issues

Draft

[WIP] Floating-point fixes#8912
tautschnig wants to merge 62 commits into
diffblue:developfrom
tautschnig:fp-issues

Commits on Mar 24, 2026
- Add KNOWNBUG test for fmaf double rounding (Float-fma-precision1)
  
  tautschnig
  and
  kiro-agent
  committed
  254757d
- Add KNOWNBUG SMT-LIB test for fp.fma on non-standard sort (Z3#6674)
  
  tautschnig
  and
  kiro-agent
  committed
  317715e
- Add KNOWNBUG SMT-LIB tests for fp.fma (Z3#6117, Z3#7162, CVC5#11139)
  
  tautschnig
  and
  kiro-agent
  committed
  8238cb0
- Add KNOWNBUG test for fp.fma
  
  tautschnig
  and
  kiro-agent
  committed
  a0244e5
- Implement fused multiply-add (FMA) in float_utilst
  
  tautschnig
  and
  kiro-agent
  committed
  307e18c
- Add __CPROVER_fma built-in and floatbv_fma_exprt expression
  
  tautschnig
  and
  kiro-agent
  committed
  bcb7930
- Add FMA special-case tests: NaN, infinity, 0*inf
  
  tautschnig
  and
  kiro-agent
  committed
  1a998bc
- Add SMT2 FPA backend tests for fp.fma emission
  
  tautschnig
  and
  kiro-agent
  committed
  084336d
- Add end-to-end SMT FPA test for FMA special cases
  
  tautschnig
  and
  kiro-agent
  committed
  ec84464
- cbmc-incr-smt2: Add test suffix to avoid intermittent failures
  tautschnig
  committed
  0c1f138
- Remove dead #if 0 block in boolbv_mod.cpp
  
  tautschnig
  and
  kiro-agent
  committed
  4334489
- Introduce ID_floatbv_mod to distinguish fmod from IEEE remainder
  
  tautschnig
  and
  kiro-agent
  committed
  b2fec73
- Use __CPROVER_fmod and __CPROVER_remainder built-ins in C library
  
  tautschnig
  and
  kiro-agent
  committed
  ae924fe
- Fix float_utilst::rem crash and distinguish fmod from remainder
  
  tautschnig
  and
  kiro-agent
  committed
  3ecb3ce
- Add fmod and remainder support to SMT2 and float_bvt back-ends
  
  tautschnig
  and
  kiro-agent
  committed
  929f628
- Update fmod/fmodf/fmodl regression tests
  
  tautschnig
  and
  kiro-agent
  committed
  54b7086
- Update remainder/remainderf/remainderl regression tests
  
  tautschnig
  and
  kiro-agent
  committed
  4f28dde
- Add remainderf edge case test
  
  tautschnig
  and
  kiro-agent
  committed
  ed3ec15
- Add remainderf tie-break test
  
  tautschnig
  and
  kiro-agent
  committed
  41d426b
- Add Java fmod regression test (farith2)
  
  tautschnig
  and
  kiro-agent
  committed
  2b6a4d1
- Add fp.rem regression tests (Z3#2381, Z3#8414)
  
  tautschnig
  and
  kiro-agent
  committed
  593e462
- Implement fused multiply-add (FMA) in float_utilst
  
  tautschnig
  and
  kiro-agent
  committed
  f8543bb
- Use FMA for IEEE remainder correction in float_utilst
  
  tautschnig
  and
  kiro-agent
  committed
  585d120
- Add _Float16 variants of fmod/remainder/fma built-ins
  
  tautschnig
  and
  kiro-agent
  committed
  108f2bc
- Add Coq proof and documentation for FMA-based remainder
  
  tautschnig
  and
  kiro-agent
  committed
  d72e961
- Add HOL Light proofs for FMA-based remainder algorithm
  
  tautschnig
  and
  kiro-agent
  committed
  bc72c54
- Add proof verification CI and _Float16 property tests
  
  tautschnig
  and
  kiro-agent
  committed
  4487fbb
- Add FP solver issues tracking document
  
  tautschnig
  and
  kiro-agent
  committed
  4ce9dbb
- Add FP regression tests based on external solver issues
  
  tautschnig
  and
  kiro-agent
  committed
  8d7a8c6
- Update FP tracking document with test results and bugs found
  
  tautschnig
  and
  kiro-agent
  committed
  d075b52
- Add more FP regression tests: roundToIntegral, BF16, trunc
  
  tautschnig
  and
  kiro-agent
  committed
  adb002a
- Add FP conversion and signed zero tests
  
  tautschnig
  and
  kiro-agent
  committed
  0ad2fe9
- Comprehensive update of FP tracking document
  
  tautschnig
  and
  kiro-agent
  committed
  5f52535
- Add deep implementation analysis of FP gaps and effort estimates
  
  tautschnig
  and
  kiro-agent
  committed
  5d9f46b
- Add fp.isSubnormal, fp.isNegative, fp.isPositive to SMT2 parser
  
  tautschnig
  and
  kiro-agent
  committed
  3088813
- Add to_fp from BitVec (reinterpret cast) to SMT2 parser
  
  tautschnig
  and
  kiro-agent
  committed
  ba33ec2
- Fix fp.to_sbv/fp.to_ubv crash with non-RTZ rounding modes
  
  tautschnig
  and
  kiro-agent
  committed
  18ded4d
- Fix fp.roundToIntegral on non-standard FP sorts
  
  tautschnig
  and
  kiro-agent
  committed
  0ec0b23
- Update FP tracking document with implementation progress
  
  tautschnig
  and
  kiro-agent
  committed
  f4f4fc4
- Add comprehensive SMT-LIB tests for external FP solver issues
  
  tautschnig
  and
  kiro-agent
  committed
  89a898b
- Add KNOWNBUG test for fp.isZero(-0) (z3-isZero-neg-zero)
  
  tautschnig
  and
  kiro-agent
  committed
  0f5285d
- Update tracking document with comprehensive test coverage
  
  tautschnig
  and
  kiro-agent
  committed
  8392bf1
- Add remaining SMT-LIB tests for all external FP solver issues
  
  tautschnig
  and
  kiro-agent
  committed
  74c9b0f
- Update tracking document with final test coverage numbers
  
  tautschnig
  and
  kiro-agent
  committed
  8b89b16
- Fix fp.isZero to handle -0 correctly
  
  tautschnig
  and
  kiro-agent
  committed
  19d7848
- Add fp.min, fp.max and fix fp.isZero(-0)
  
  tautschnig
  and
  kiro-agent
  committed
  937ac77
- Implement fp.sqrt in SMT2 solver
  
  tautschnig
  and
  kiro-agent
  committed
  27356d6
- Add KNOWNBUG tests for fp.sqrt gaps
  
  tautschnig
  and
  kiro-agent
  committed
  f9a2ee0
- Add KNOWNBUG test for fminf zero sign (Float-fmin-zero-sign1)
  
  tautschnig
  and
  kiro-agent
  committed
  a7e157f
- Add KNOWNBUG test for sqrtf rounding (Float-sqrt-rounding1)
  
  tautschnig
  and
  kiro-agent
  committed
  52cdfdf
- Add plan for remaining FP issues
  
  tautschnig
  and
  kiro-agent
  committed
  7816853
- Fix to_fp from large Real constant tests: KNOWNBUG→CORE
  
  tautschnig
  and
  kiro-agent
  committed
  f10cc88
- Improve fp.sqrt: correct for RNE and exact cases, RTZ/RTP still TODO
  
  tautschnig
  and
  kiro-agent
  committed
  79fc62f
- Status update: 3.3 done, sqrt partially done, C built-ins deferred
  
  tautschnig
  and
  kiro-agent
  committed
  961c4c2
- Fix fp.sqrt: correct for all rounding modes and subnormals
  
  tautschnig
  and
  kiro-agent
  committed
  d226524
- Add __CPROVER_fmin/fmax built-ins for correct IEEE 754 min/max
  
  tautschnig
  and
  kiro-agent
  committed
  82da606
- Add __CPROVER_sqrt built-in for correct IEEE 754 sqrt
  
  tautschnig
  and
  kiro-agent
  committed
  c18fc47
- Fix z3-2631-quant-fpa test: use declare-const for indexed sort
  
  tautschnig
  and
  kiro-agent
  committed
  b4d89ab
- Support to_fp from rational constants (/ p q)
  
  tautschnig
  and
  kiro-agent
  committed
  7005b30
- Implement fp.to_real and to_fp from rational constants
  
  tautschnig
  and
  kiro-agent
  committed
  3c8f7a1
- Add relevant-value-set quantifier instantiation for FP/BV types
  
  tautschnig
  and
  kiro-agent
  committed
  eb92591
- Add arithmetic refinement for fp.rem and fix float_bvt tie-breaking
  
  tautschnig
  and
  kiro-agent
  committed
  43c7e0b

Commits

Commits on Mar 24, 2026