// Description: declare a record type for pairs. Create a variable of that type. Initialize it. Then, in a next block, assign a const_record to it. Check that the invariant holds.

module main {
    type pair = record { fst: integer, snd: integer };
    var p: pair;

    init {
        p.fst = 1;
        p.snd = 2;
    }

    next {
        p' = const_record(fst := 100, snd := 101);
    }

    invariant fst_lt_snd: p.fst < p.snd;

    control {
        induction;
        check;
        print_results;
    }
}
