Group by - probable bug

I’m grouping by a double column. The following 2 rows are not aggregated into the same group.

1,

1,

My first thought was a floating point situation where one of the floats is not 1, but 0.999999999 or so. However, that’s not the case. When I copy the values from the table view, I get 1 and 1.0 respectively. Obviously, they should be grouped.