-- { echo }
SELECT CAST(1111111111.222 AS DateTime64(3));
SELECT toDateTime(1111111111.222, 3);
SELECT toDateTime64(1111111111.222, 3);