CIF to CIF transformation to eliminate state invariants incorrect for synchronizing events

Consider the following CIF model in which automata A anb B synchronize over event a, thereby update their own local variables A.x and B.x, and a state plant invariant to keep the local variables equal:

event a;

automaton A:
  disc bool x = false;

  location:
    initial;
    edge a do x := true;
end

automaton B:
  disc bool x = false;

  location:
    initial;
    edge a do x := not x;
end

plant invariant A.x = B.x;

The state space of this CIF model is

event a;
automaton statespace:
  alphabet a;
  @state(A: "*", A.x: false, B: "*", B.x: false)
  location loc1:
    initial;
    edge a goto loc2;
  @state(A: "*", A.x: true, B: "*", B.x: true)
  location loc2;
end

Now, if we apply the CIF to CIF transformation to eliminate state invariants, we obtain the model

event a;
automaton A:
  disc bool x = false;
  location:
    initial;
    edge a when true = B.x do x := true;
end
automaton B:
  disc bool x = false;
  location:
    initial;
    edge a when A.x = not x do x := not x;
end

which has the following different state space:

event a;
automaton statespace:
  alphabet a;
  @state(A: "*", A.x: false, B: "*", B.x: false)
  location loc1:
    initial;
end

As you can see, the transformed model where the state invariant has been eliminated does not consider the update of 'other' local variable: for edge a in A, the invariant A.x = B.x is translated to true = B.x where the update on A.x has been considered, but the update of B.x is not.