> Double precision usually refers to 64-bit floating point, like you say.

Is it? Doesn't `double` in c refers to a 32bit value?

EDIT:

So, it seems I've not dealt with this in much too long and am misremembering and therefor wrong.

    #include <stdio.h>
    int main() {
      printf("sizeof(float) = %d\n", sizeof(float));
      printf("sizeof(double) = %d\n", sizeof(double));
      return 0;
    }

yields

    sizeof(float) = 4
    sizeof(double) = 8

on an Intel(R) Core(TM) i5-6200U (more-or-less a run-of-the-mill-not-that-mill 64-bit x86-family core. I don't have a 32-bit processor handy to test, but I don't believe it'd change the results.