// Description: create a colour enum and a record to represent triples of colours. Create a variable of this type and assume that all three colours are the same. Then, havoc the variable and assert that all three colours are the same. Finally, do BMC.

module main {
    type colour = enum {red, green, blue};
    type triple = record { x: colour, y: colour, z: colour };

    var t: triple;

    init {
        assume t.x == t.y && t.y == t.z;
    }

    next {
        havoc t;
        assert t.x == t.y && t.y == t.z;
    }

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