// Purpose: Test nested arrays
// Description: A module with two arrays. The first is indexed by integers and contains integers. The second is indexed by the type of the first array and contains elements of the type of the first array. We then assert a contradiction using axioms that say that the first array is inside the second array, but that an element that should match does not. Finally, we add a dummy invariant that would trivially fail if there are no contradictions.
// Expectation: The verification should pass.
// Validation: If we insert a bug into axioms or array indexing (selects) this should fail.

module main {
    var a1 : [integer]integer;
    var a2 : [[integer]integer][integer]integer;

    axiom a1[0] == 0;
    axiom a2[a1] == a1;
    axiom a2[a1][0] != 0;

    invariant dummy: false;

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