3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00

Add fpa regression test for fp.to_real denormal encoding fix

Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the
bug reported in the issue: denormal floating-point values in
(_ FloatingPoint 2 24) were getting wrong fp.to_real values because
mk_to_real was not subtracting the normalization shift lz from the
exponent.

Tests verify:
- The specific denormal from the bug report is NOT > 1.0
- Two other denormals have correct real values (0.5 and 0.125)
- A normal value is correctly identified as > 1.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-25 22:04:03 +00:00
parent de3cf18899
commit add65451fd
3 changed files with 75 additions and 0 deletions

View file

@ -287,4 +287,5 @@ int main(int argc, char ** argv) {
TST(ho_matcher);
TST(finite_set);
TST(finite_set_rewriter);
TST(fpa);
}