source: CIVL/examples/focus/sv-benchmarks-main-c-array-industry-pattern/c/array-industry-pattern/array_mul_init.c@ a7752a9

/* Verifiable with -memeq but fails without. TODO: Figure out what the discrepency is.
 */
#include <stdlib.h>
#include <assert.h>

#pragma CIVL ACSL

$input int N;
$assume(0 < N);
short __VERIFIER_nondet_short() {
  short x;
  $havoc(&x);
  return x;
}
int main()
{
        int a[N];
        int b[N];
        int k;
        int i;

  //@ focus I;
        for (i  = 0; i<N ; i++)
        {
                a[i] = i; 
                b[i] = i ;
        }

  //@ focus I;
        for (i=0; i< N; i++)
        {
                if(__VERIFIER_nondet_short())
                {
                        k = __VERIFIER_nondet_short();
                        a[i] = k;
                        b[i] = k * k ;
                }
        }

  // Modified
  //@ focus I;
  $assert($forall(int i:0..N-1) a[i] == b[i] || b[i] == a[i] * a[i]);
  // Original
  /*
        for (i=0; i< N; i++)
        {
                __VERIFIER_assert(a[i] == b[i] || b[i]  == a[i] * a[i]);
        }
  */
}