E.g., when given as input to gr1c version 0.7.4, the following results in a two-node automaton with both nodes labeled with the system value loc=0.

ENV: x;
SYS: loc [0,2];

ENVINIT: x;
ENVTRANS: [](x -> !x');
ENVGOAL: []<> x;

SYSINIT: loc = 0;
SYSTRANS:
  []((loc = 0) -> ((loc'=0) | (loc'=1)))
& []((loc = 1) -> ((loc'=0) | (loc'=1) | (loc'=2)))
& []((loc = 2) -> ((loc'=1) | (loc'=2)));
SYSGOAL: []<> (loc = 2);

This bug is also known to affect master branch at time of writing (3994b9a).

This behavior was first reported by @wmgithub in an issue for a different project: tulip-control/tulip-control#85. The specification reported there was larger. The above is the smallest one demonstrating the bug that I have found so far.