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", "count_up_down-1.c", 3, "reach_error"); }
   4
   5void __VERIFIER_assert(int cond) {
   6  if (!(cond)) {◐PART
   7    ERROR: {reach_error();abort();}
   8  }
   9  return;
  10}
  11unsigned int __VERIFIER_nondet_uint();
  12
  13int main()
  14{
  15  unsigned int n = __VERIFIER_nondet_uint();
  16  unsigned int x=n, y=0;
  17  while(x>0)●FULL
  18  {
  19    x--;
  20    y++;
  21  }
  22  __VERIFIER_assert(y==n);
  23}
  24