// Description: A module with an array variable, an index variable, and a boolean variable. The array is indexed by integers and contains booleans. The system starts by setting that value true at index 0 of the array. At each step, the system increments the index and sets the value of the array at that index to true. There is one invaraint that uses a universal quantifier to say that every element of the array is true between 0 and the current index.

module main {
    var a : [integer]boolean;
    var i : integer;
    var b : boolean;

    init {
        i = 0;
        b = true;
        a[i] = b;
    }

    next {
        i' = i + 1;
        a' = a[i -> b];
    }

    invariant more_true: forall (j : integer) :: (0 <= j && j < i) ==> a[j];

    control {
        bmc(10);
        check;
        print_results;
    }
}
