float64_t __float64_div(float64_t dividend, float64_t divisor);
__float64_div divides dividend by divisor and returns the quotient as the result.