Frama-C 24.0归纳策略疑似Bug：归纳目标为true问题求助

我正在对一段C代码做形式化证明，针对循环不变量result_val采用以begin为基例、对i的归纳策略验证。在Frama-C 24.0中，归纳的sup分支需要证明的目标是true，可直接得证；但切换至25.0版本后，该分支生成了更复杂的条件（显式计算最弱前置条件，更符合正确归纳逻辑），然而所有尝试的SMT解算器均无法证明该条件。我对24.0版本结果的正确性存疑，因归纳证明目标为true不符合常理，想知道这是24.0的Bug还是版本间的实现差异？

相关代码 #

#include <stdbool.h>
#define  SIZE       1000

bool data[SIZE] ;


/*@
    logic integer count(integer begin, integer end)=
        begin >= end ? 0 : (data[begin]==true) ? count(begin+1, end)+1 : count(begin+1, end);
*/

/*@
    requires SIZE > begin >= 0;
    requires SIZE >= end >= 0;
    requires begin <= end;
    assigns \nothing;
    ensures \result == count(begin, end);
 */
unsigned int occurrences_of(int begin, int end)
{
    unsigned int result = 0;

    /*@
        loop invariant i_bound: begin <= i <= end;
        loop invariant result_bound: 0 <= result <= i-begin;
        loop invariant result_val: result == count(begin, i);
        loop assigns i, result;
        loop variant end-i;
    */
    for (unsigned int i = begin; i < end; ++i){
        result += (data[i] == true) ? 1 : 0;
    }
    return result;
}

Frama-C 24.0输出结果 #

Proof:
  Goal Invariant 'result_val' (preserved) (Induction: proved)
   + Goal Induction (Base) (proved)
   + Goal Induction (Induction (sup)) (proved)
   + Goal Induction (Induction (inf)) (proved)
Qed.
--------------------------------------------------------------------------------

Goal Induction (Induction (sup)):
Prove: true.

Frama-C 25.0输出结果 #

--------------------------------------------------------------------------------
Proof:
  Goal Invariant 'result_val' (preserved) (Induction: pending)
   + Goal Induction (Base) (proved)
   + Goal Induction (Induction (sup)) (pending)
   + Goal Induction (Induction (inf)) (proved)
End.
--------------------------------------------------------------------------------

Goal Induction (Induction (sup)):
Let x_0 = to_uint32(end@L1).
Let x_1 = to_uint32(tmp@L12).
Let x_2 = data@L1[i@L6].
Let x_3 = result@L6.
Let x_4 = result@L13.
Let x_5 = to_uint32(1 + i@L6).
Assume {
  Have: begin@L1 < i@L6.
  Have: i@L6 <= end@L1.
  Have: i@L6 < x_0.
  Have: 0 <= x_3.
  Have: x_5 <= end@L1.
  Have: begin@L1 <= x_5.
  Have: (begin@L1 + x_3) <= i@L6.
  Have: (begin@L1 + x_4) <= x_5.
  Have: is_uint32(i@L6).
  Have: is_bool(x_2).
  Have: is_uint32(x_3).
  Have: if (x_2 = 1) then (tmp@L12 = 1) else (tmp@L12 = 0).
  Have: forall i_0 : Z. let x_6 = L_count(data@L1, begin@L1, i_0) in
      let x_7 = to_uint32(1 + i_0) in let x_8 = to_uint32(x_1 + x_6) in
      let x_9 = data@L1[i_0] in ((i_0 <= end@L1) -> ((begin@L1 <= i_0) ->
      ((i_0 < i@L6) -> ((i_0 < x_0) -> ((0 <= x_6) -> ((x_7 <= end@L1) ->
      ((begin@L1 <= x_7) -> (((begin@L1 + x_6) <= i_0) ->
      (((begin@L1 + x_8) <= x_7) -> (is_uint32(i_0) -> (is_bool(x_9) ->
      (is_uint32(x_6) ->
      ((if (x_9 = 1) then (tmp@L12 = 1) else (tmp@L12 = 0)) ->
      (L_count(data@L1, begin@L1, x_7) = x_8)))))))))))))).
  [...]
  Stmt { L6:  }
  Stmt { tmp = tmp_0;  }
  Stmt { L12: result = x_4;  }
  Stmt { L13:  }
}
Prove: L_count(data@L1, begin@L1, x_5) = x_4.

Goal id:  typed_occurrences_of_loop_invariant_result_val_preserved
Short id: occurrences_of_loop_invariant_result_val_preserved
--------------------------------------------------------------------------------
Prover Alt-Ergo 2.4.2: Timeout (Qed:52ms) (10s).

内容的提问来源于stack exchange，提问作者Yu-Fang Chen