source: CIVL/examples/experimental/whenAssert.cvl@ a88887d

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

void main(){
int n = 2;
int i = 1;

int s = 0;

if(n > 2)
        s = sum(5);
else
        s = sum(8);

$when(n >= 2) $assert s == 9*8/2;
}