Simulator should produce a minimal violated invariant

[konnov]

When the simulator finds a violation to and { A_1, ..., A_n }, it should report one of A_i that was violated.

[p-offtermatt]

+1, this is a great idea, and seems relatively simple to implement? The and variant is clearly better to run than e.g. running in sequence to check separately A_1 to A_n, but the fact that you don't really know which invariant was actually violated makes this really annoying.