PHP 7.1.3で時刻の差を取ると時々1マイクロ秒ズレる

本日はエイプリルフールなので、ウソでも本当でも誰も困らないPHPのバグの話をします。
PHP 7.1.0からPHPのDateTimeクラスでマイクロ秒の扱いを強化しているようで、挙動やコードの変更がチラホラ見受けられます。（参考：「PHP 7.1からDateTimeが現在時刻のマイクロ秒まで見るようになった – Qiita」）
時刻と時刻の差分を扱うDateIntervalクラスでもPHP 7.1.0以降マイクロ秒に対応したようで、DateInterval::formatメソッドもマイクロ秒の表示に対応しているようです。さっそく実験してみましょう。

<?php
$dt1=new DateTime("2000-01-01 00:00:00");
$dt2=new DateTime("2006-01-02 03:04:05.6");
$interval = $dt1->diff($dt2);
var_dump($interval->format("%R%Y-%M-%D %H:%I:%S.%F"));
/* Output: string(25) "+06-00-01 03:04:05.600000" */

パラメータ%Fで差分のマイクロ秒が表示できました。ところで、次のような例を試すと奇妙なことに気づきます。

<?php
$dt1=new DateTime("2000-01-01 00:00:00");
$dt2=new DateTime("2006-01-02 03:04:05.000251");
$interval = $dt1->diff($dt2);
var_dump($interval->format("%R%Y-%M-%D %H:%I:%S.%F"));
/* Output: string(25) "+06-00-01 03:04:05.000250" */

0と251の差なので「000251」と表示されるはずが「000250」となっており、1マイクロ秒ズレた結果になっています。

ドキュメント化もされていない機能なので誰も困らないと思いますが、一応バグ報告しておきました。