#include #include #ifdef _CIVL #include $input int B=5, N; $assume(1<=N && N<=B); #else #define N 100 #endif int sum=0; int main() { for (int i = 1; i <= N; i++) sum += i; printf("N=%d, sum = %d\n", N, sum); assert(sum == (N+1)*N/2); }