double
foo (double a, double b)
{
  if (!__builtin_isfinite (a))
    return 42.0;
  if (!__builtin_isfinite (b))
    return 42.0;
  double res = a + b;
  __attribute__((assume (__builtin_isfinite (res))));
  return res;
}

double
bar (double a, double b)
{
  if (!__builtin_isfinite (a))
    return 42.0;
  if (!__builtin_isfinite (b))
    return 42.0;
  double res = a - b;
  __attribute__((assume (__builtin_isfinite (res))));
  return res;
}

double
baz (double a, double b)
{
  if (!__builtin_isfinite (a))
    return 42.0;
  if (!__builtin_isfinite (b))
    return 42.0;
  double res = a * b;
  __attribute__((assume (__builtin_isfinite (res))));
  return res;
}

double
qux (double a, double b)
{
  if (!__builtin_isfinite (a))
    return 42.0;
  double res = a / b;
  __attribute__((assume (__builtin_isfinite (res))));
  return res;
}

double
quux (double a, double b)
{
  if (!__builtin_isfinite (b))
    return 42.0;
  double res = a  / b;
  __attribute__((assume (!__builtin_isnan (res) && res != 0.0)));
  return res;
}