GCC compile time division error

Can someone explain this behaviour?

test.c:

#include <stdio.h>

int main(void)
{
    printf("%d, %d\n", (int) (300.6000/0.05000), (int) (300.65000/0.05000));
    printf("%f, %f\n", (300.6000/0.05000), (300.65000/0.05000));
    return 0;
}

$ gcc test.c

$ ./a.out
6012, 6012
6012.000000, 6013.000000

I checked the assembly code and it puts both the arguments of the first printf as 6012, so it seems to be a compile time bug.

Run

#include <stdio.h>

int main(void)
{
    printf("%d, %d\n", (int) (300.6000/0.05000), (int) (300.65000/0.05000));
    printf("%.20f %.20f\n", (300.6000/0.05000), (300.65000/0.05000));
    return 0;
}

and it should be more clear. The value of the second one (after floating point division, which is not exact) is ~6012.9999999999991, so when you truncate it with (int), gcc is smart enough to put in 6012 at compile time.

When you print the floats, printf by default formats them for display with only 6 digits of precision, which means the second prints as 6013.000000.