syst_floatx80_to_int64
int64 syst_floatx80_to_int64( floatx80 );
test_a_floatx80_z_int64( floatx80_to_int64, syst_floatx80_to_int64 );