1  int f(unsigned number_of_digits_to_use)
       2  {
       3    if (number_of_digits_to_use >1294)
       4      return 0;
       5    return (number_of_digits_to_use * 3321928 / 1000000 + 1) /16;
       6  }
       7  
       8  int main(void)
       9  {
      10    if (f(11) != 2)
      11      __builtin_abort ();
      12    exit (0);
      13  }