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