Проверка функции, которая суммирует массив int vs массив float с помощью FramaC / WP

Я пытаюсь определить и проверить эту простую функцию, которая суммирует массив. Эта спецификация для массива целых чисел принята WP:

/*@ axiomatic Sum_Int {
      logic int sum_int(int *values, integer begin, integer end)
          reads values[begin .. (end - 1)];

      axiom empty_int:
        \forall int *p, integer begin, end; begin >= end
            ==> sum_int(p, begin, end) == 0;

      axiom range_int:
        \forall int *p, integer begin, end; begin < end
            ==> sum_int(p, begin, end) == sum_int(p, begin, end - 1) + p[end - 1];
}
*/

/*@ requires \valid_read(values + (0 .. size - 1));

    assigns \nothing;

    ensures \result == sum_int(values, 0, size);
*/
int sum_int_array(const int *values, size_t size) {
    int sum = 0;
    /*@ loop invariant 0 <= index <= size;
        loop invariant sum == sum_int(values, 0, index);
        loop assigns sum, index;
        loop variant size - index;
    */
    for (size_t index = 0; index < size; index++) {
        sum += values[index];
    }
    return sum;
}

Но та же спецификация для массива с плавающей запятой не может быть подтверждена WP:

/*@ axiomatic Sum_Real {
      logic float sum_real(float *values, integer begin, integer end)
          reads values[begin .. (end - 1)];

      axiom empty_real:
        \forall float *p, integer begin, end; begin >= end
            ==> sum_real(p, begin, end) == 0;

      axiom range_real:
        \forall float *p, integer begin, end; begin < end
            ==> sum_real(p, begin, end) == sum_real(p, begin, end - 1) + p[end - 1];
}
*/

/*@ requires \valid_read(values + (0 .. size - 1));

    requires \forall integer i; 0 <= i < size ==> \is_finite(values[i]);
    assigns \nothing;

    ensures \result == sum_real(values, 0, size);
*/
float sum_float_array(const float *values, size_t size) {
    float sum = 0;
    /*@ loop invariant 0 <= index <= size;
        loop invariant sum == sum_real(values, 0, index);
        loop assigns sum, index;
        loop variant size - index;
    */
    for (size_t index = 0; index < size; index++) {
        sum += values[index];
    }
    return sum;
}

Аксиоматическое определение такое же (и я думаю, что оно должно быть таким же, если оно верное). Единственное отличие - добавленное предварительное условие для массива с плавающей запятой:

requires \forall integer i; 0 <= i < size ==> \is_finite(values[i]);

Я не уверен, что это необходимо. Какой информации здесь не хватает, чтобы WP мог проверить версию с плавающей запятой?