source: CIVL/examples/languageFeatures/chooseInt.cvl@ 1258be5

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

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;
}