使用Frama-C WP插件验证希尔排序时持续超时问题求助

各位大佬好！我最近在折腾Frama-C的WP插件，想验证一段希尔排序的实现，但一直卡在超时的问题上——试了调整参数、简化初始规范，都没用，实在没辙了来这儿求指点！

我目前写的代码和对应的ACSL规范如下：

/*@ requires n > 0;
  @ requires \valid(v + (0..n-1));
  @ ensures \forall integer k; 0 <= k < n-1 ==> v[k] <= v[k+1];
  @ assigns v[0..n-1];
  */
void shellsort(int v[], int n) {
    int gap = n / 2;
    /*@ loop invariant 0 < gap <= n/2;
      */
    // 后续的希尔排序核心逻辑（目前仅完成gap初始化和基础循环不变式定义，就已触发超时）
}

具体情况是：我刚给gap的循环加上最基础的不变式，还没来得及补充数组有序性相关的复杂不变式，运行WP验证就直接卡住然后超时了。想问问有Frama-C验证经验的朋友，这种情况通常是哪里出了问题？比如是不是初始不变式的写法有疏漏，还是WP插件对希尔排序这类带间隔的排序算法有特殊的验证技巧或者优化参数？

内容来源于stack exchange