Description:
------------
When multiplying two float, the truncated result is not correct.

Reproduce code:
---------------
<?php
$v1 = (float)0x5a05df1b;
$v2 = (float)0x2d02ef8d;

echo 'v1='.sprintf("0x%X (%d)", $v1, $v1).'<br>';
echo 'v2='.sprintf("0x%X (%d)", $v2, $v2).'<br>';
(float)$v3=(float)$v1*(float)$v2;
echo 'v1*v2='.sprintf("0x%X (%d)", (float)$v3, (float)$v3).'<br>';

// Actual result is :
//   v1=0x5A05DF1B (1510334235)
//   v2=0x2D02EF8D (755167117)
//   v1*v2=0x8DBC1700 (-1917053184)
//
// Result should be : 0xFD410808DBC16DF
// Truncated should be : 0x8DBC16DF

?>

Expected result:
----------------
Result should be : 0xFD410808DBC16DF, because variable is a float, result should be truncated like that :
0x8DBC16DF

Actual result:
--------------
v1*v2=0x8DBC1700 (-1917053184)