@regehr @hyperoptimizer

... hold up. This is checking |a - b| < 0.0, which is always false. Is there a typo or a bug in the checker, or did I misread something?

@steve @hyperoptimizer I don't think typo-- I'm cutting and pasting.

but we've seen Alive2 and Z3 bugs wrt FP....

@regehr @steve @hyperoptimizer but the godbolt link has

%cmp = fcmp olt double %ext, 1.000000e-15

which is reasonable, so 0.0000 shown in the screenshot is the result of printing with %f?

@amonakov @steve @hyperoptimizer ah.... the screenshot is Alive2's output, which may not be sufficiently careful about floats.

indeed the godbolt link is the correct code

@regehr with C-style formatters, IIRC, either of %.16e or %.17g will print differently two doubles that are different, whereas obviously %f does not.

(assuming a modicum of quality of the libc doing the printing)

@regehr If you are willing to accept base-2 exponents being printed instead of base-10 (the significand can be in base 10, e.g. 1.57p2 for π), you can make a function sufficient for regression tests with a call to frexp, a multiplication and a conversion to uint64_t. Always prints differently doubles that are different and the n-1 first digits are even correct!

If you want base-10 exponents, it's better to add a dependency than to try to reinvent it. Either you'll have to reinvent multiprecision integers or to reinvent extremely sophisticated shortcuts invented along the decades by extremely bright people. It is really difficult and the algorithms known today have refined the job of doing this conversion efficiently to a tour de force.