#include <stdio.h>
#include "sumlib.h"
$input int B=5, N;
$assume(1<=N && N<=B);
int main() {
  int result = sum(N);
  printf("N=%d, sum = %d\n", N, result);
  $assert(result == (N+1)*N/2);
}