// Description: This test has a single module with an init block that contains a for loop. The for loop runs over range 0 to 4 and initialises the first 5 elements of an array to 0. The invariant then checks that the first 5 elements of the array are equal to 0 but the 6th element is not, and is checked with bmc.

module main{
    var arr: [integer]integer;

    init{
        for i in range(0, 4){
            arr[i] = 0;
        }
        arr[5] = 10;
        arr[6] =10;
    }

property check: arr[0]+arr[1] + arr[2] + arr[3] + arr[4]==0 && arr[5]==10;
control{
    bmc(0);
    check;
}

}
