/* Commandline execution:
 *		civl verify chooseInt.cvl
 * */
#include <civlc.cvh>

int sum(int n){
	int sum = 0;
	
	for(int i = 1; i <= n; i++){
		sum += i;
	}
	return sum;
}

void main(){
	int k = $choose_int(5);
	int result = sum(k);
	
	$assert(result == k*(k+1)/2);
}