source: CIVL/examples/library/civlc/chooseInt.cvl

/* 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);
}