1extern void abort(void);
   2#include <assert.h>
   3void reach_error() { assert(0); }
   4extern int __VERIFIER_nondet_int(void);
   5void __VERIFIER_assert(int cond) {
   6  if (!(cond)) {◐PART
   7    ERROR: {reach_error();abort();}
   8  }
   9  return;
  10}
  11
  12#define SZ 2048
  13
  14int main(void) {
  15  int A[SZ];
  16  int B[SZ];
  17  int i;
  18  int tmp;
  19
  20  for (i = 0; i < SZ; i++) {●FULL
  21    A[i] = __VERIFIER_nondet_int();
  22    B[i] = __VERIFIER_nondet_int();
  23  }
  24
  25  for (i = 0; i < SZ; i++) {●FULL
  26    tmp = A[i];
  27    B[i] = tmp;
  28  }
  29
  30  __VERIFIER_assert(A[SZ/2] != B[SZ/2]);
  31}