source: CIVL/examples/focus/sv-benchmarks-main-c-array-industry-pattern/c/array-industry-pattern/array_range_init.c@ 3d3af8f

/* Bug found!
 * Fixed assertion and verified.
 */
#include <stdlib.h>
#include <assert.h>
#pragma CIVL ACSL
$input int N;
$assume(0 < N);

signed int a[N];

int main()
{
        int i;
  //@ transform flatten i;
        for(i = 0; i < N; i++)
        {
                if(i>=0 && i<=10000)
                        a[i] = 10;
                else
                a[i] = 0;
        }

  // fixed:
  //@ transform flatten i;
  $assert($forall(int i:0..N-1) (i>=0 && i <= 10000) => a[i] == 10);
  /* modified:
  // transform flatten i;
  $assert($forall(int i:0..N-1) a[i] == 10);
  */
  /* original:
        for(i = 0; i < N; i++)
        {
                __VERIFIER_assert(a[i] == 10);
        }
  */

        return 0;
}