// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
// RUN: %klee --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log
// grep -q "Finished successfully!\n"

/* This is testing the const array optimization.  On my 2.3GHz machine
   this takes under 2 seconds w/ the optimization and almost 6 minutes
   w/o.  So we kill it in 10 sec and check if it has finished
   successfully. */

#include <unistd.h>
#include <assert.h>
#include <stdio.h>
  
int main() {
#define N 8192
#define N_IDX 16
  unsigned char a[N];
  unsigned i, k[N_IDX];

  for (i=0; i<N; i++)
    a[i] = i % 256;
  
  klee_make_symbolic(k, sizeof(k), "k");
  
  for (i=0; i<N_IDX; i++) {
    if (k[i] >= N)
      klee_silent_exit(0);

    if (a[k[i]] == i)
      assert(k[i] % 256 == i);
    else klee_silent_exit(0);
  }

  printf("Finished successfully!\n");

  return 0;
}