mpfr_sub1 is called, where b is 2 limbs long (128-bit), while a and c is just one limb long (64-bit).
As c is small, but not small enough (difference in exponents exactly 128), we reach the:

for (k = 0; (bn > 0) || (cn > 0); k = 1)

loop in sub1.c, with sh == 0.  In the first iteration bb is equal to MPFR_LIMB_HIGHBIT and cc is 0 (it is before the highest limb in c), and we reach the special case:

      /* the case rounding to nearest with sh=0 is special since one couldn't
         subtract above 1/2 ulp in the trailing limb of the result */
      if ((rnd_mode == GMP_RNDN) && sh == 0 && k == 0)
        {
          mp_limb_t half = MPFR_LIMB_HIGHBIT;

          is_exact = (bb == cc);

          /* add one ulp if bb > cc + half
             truncate if cc - half < bb < cc + half
             sub one ulp if bb < cc - half
          */
...
        }

The comments seems to cover most of the cases, just not two important ones, where either bb is equal to cc + half (this case) or bb is equal to cc - half.
In that case after this bb is equal to cc, eventhough they weren't equal before.  In this case with round to nearest we really can't decide right away, need to look at next (or following limbs) to decide if exactly 0.5ulp was added resp. subtracted, or if tiny bit above it or below it, but that decision should take into account that the special case above with bb == cc + half or bb == cc - half happened.  In the code it doesn't, so we fall through to the next limb - 0 in bb (as it is after lowest limb) and 0xfff80f8000000000 in cc.  k is non-zero, so the special case isn't done now, bb is smaller than cc, so it sets down and reaches the
420                   else if (down && sh == 0)
421                     goto sub_one_ulp;
case, so it incorrectly subtracts 1ulp instead of just raising inexact and truncating.

fixed upstream in revision 7212. Jakub, please could you check it fixes the
problem, so that we can close the bug on our side? Thank you for reporting it
and analyzing the reason.

Paul Zimmermann

PS: I guess Vincent Lefevre will post a patch for MPFR 3.0.0

Created attachment 454393 [details]
mpfr-rh643657.patch

Backported patch from upstream (the differences are just changing MPFR_RND* back to GMP_RND* and undoing the move of sub1.c to src/sub1.c).
So far my fma tester runs with this patch for 5 hours on each of -DDO_FLT, -DDO_DBL and -DDO_LDBL on x86_64-linux and no problems were reported.

This request was evaluated by Red Hat Product Management for
inclusion in the current release of Red Hat Enterprise Linux.
Because the affected component is not scheduled to be updated
in the current release, Red Hat is unfortunately unable to
address this request at this time. Red Hat invites you to
ask your support representative to propose this request, if
appropriate and relevant, in the next release of Red Hat
Enterprise Linux. If you would like it considered as an
exception in the current release, please ask your support
representative.

Red Hat Enterprise Linux 6 is in the Production 3 Phase. During the Production 3 Phase, Critical impact Security Advisories (RHSAs) and selected Urgent Priority Bug Fix Advisories (RHBAs) may be released as they become available.

The official life cycle policy can be reviewed here:

http://redhat.com/rhel/lifecycle

This issue does not meet the inclusion criteria for the Production 3 Phase and will be marked as CLOSED/WONTFIX. If this remains a critical requirement, please contact Red Hat Customer Support to request a re-evaluation of the issue, citing a clear business justification. Note that a strong business justification will be required for re-evaluation. Red Hat Customer Support can be contacted via the Red Hat Customer Portal at the following URL:

https://access.redhat.com/