IEEE округление с плавающей запятой в C

У меня возникли проблемы с пониманием конкретного двойного вычисления IEEE. Возьмем следующую программу C99, которая работает на хосте с двойным IEEE (8 байт, 11-битная смещенная экспонента, 52-битная закодированная мантисса):

#include <stdio.h>
#include <fenv.h>

// Expect IEEE double
int _a[sizeof (double) == 8 ? 1 : -1];

#define PP(X) printf (#X " = %d\n", X)

int main (void)
{
  // Print rounding modes.
  PP (FE_TONEAREST);
  PP (FE_UPWARD);
  PP (FE_DOWNWARD);
  PP (FE_TOWARDZERO);

  // What mode do we have?
  printf ("rounding mode = %d\n", fegetround());

  // Add a and b.
  double a = -0x1.638e38e38e38ep5;
  double b = -0x1.638e38e38e38ep6;
  __asm ("" : "+r" (a));
  __asm ("" : "+r" (b));
  printf ("a   = %a\n", a);
  printf ("b   = %a\n", b);
  printf ("a+b = %a\n", a + b);

  return 0;
}

Скомпилируйте и запустите:

$ gcc rounding.c -lm && ./a.out
FE_TONEAREST = 0
FE_UPWARD = 2048
FE_DOWNWARD = 1024
FE_TOWARDZERO = 3072
rounding mode = 0
a   = -0x1.638e38e38e38ep+5
b   = -0x1.638e38e38e38ep+6
a+b = -0x1.0aaaaaaaaaaaap+7

Мой вопрос: почему наименее значимая часть суммы равна a и не округляется до b, поскольку включено округление до ближайшего?

В двойной эмуляции IEEE с 56 битами для декодированной мантиссы вычисление выглядит следующим образом:

# Printed the double values, same like on the host:
A   = -0x1.638e38e38e38ep5
B   = -0x1.638e38e38e38ep6
# Internal format with 56-bit mantissa. The digit after | indicates
# three extra bits compared to IEEE.
# 
A     = -0x1.638e38e38e38e|0, expo = 5
B     = -0x1.638e38e38e38e|0, expo = 6
A + B = -0x1.0aaaaaaaaaaaa|8, expo = 7

Поэтому, когда A + B упаковывается как двойной, это округляется до

(double) (A + B) = -0x1.0aaaaaaaaaaabp+7

Нет?