1#include "assert.h"
   2
   3int main() {
   4    int n, sum, i;
   5    n = __VERIFIER_nondet_int();
   6    if (!(1 <= n && n <= 1000)) return 0;◐PART
   7    sum = 0;
   8    for(i = 1; i <= n; i++) {○NONE
   9        sum = sum + i;
  10    }
  11    __VERIFIER_assert(2*sum == n*(n+1));
  12    return 0;
  13}