1extern void abort(void);
   2extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
   3void reach_error() { __assert_fail("0", "for_bounded_loop1.c", 3, "reach_error"); }
   4
   5extern void abort(void);
   6void assume_abort_if_not(int cond) {
   7  if(!cond) {abort();}○NONE
   8}
   9void __VERIFIER_assert(int cond) {
  10  if (!(cond)) {●FULL
  11    ERROR: {reach_error();abort();}
  12  }
  13  return;
  14}
  15
  16int __VERIFIER_nondet_int();
  17
  18int main() {
  19  int i=0, x=0, y=0;
  20  int n=__VERIFIER_nondet_int();
  21  if (!(n>0)) return 0;●FULL
  22  for(i=0; i<n; i++)●FULL
  23  {
  24    x = x-y;
  25    __VERIFIER_assert(x==0);
  26    y = __VERIFIER_nondet_int();
  27    if (!(y!=0)) return 0;●FULL
  28    x = x+y;
  29    __VERIFIER_assert(x!=0);
  30  }
  31  __VERIFIER_assert(x==0);
  32}
  33