When compiling SYSTEM and checking G2_Realizability_Under_A we see a trace that is not part of the model. And the output mixes up the actual property that is checking.
