Description:
------------
In the following code gmp_intval returns bad results. Replace it with gmp_strval to see the difference:




Reproduce code:
---------------
$val = "19991231235958";
$value = gmp_init($val);
$res = gmp_div_qr($value, "0x100000000");
$b1 = (string) gmp_intval($res[1]);
$b2 = (string) gmp_intval($res[0]);
echo "$b1 $b2";