Apalache seems to cache Gen expressions

[Kukovec]

When encountering two syntactically-equal and type-equal Gen-initializations, apalache appears to cache the RHS, making it impossible to generate different values for two variables initializaed this way. For the attached module, apalache-mc check --length=0 results in a deadlock with --init=InitDeadlock, and no error with --init=InitNoDeadlock, even though the two Init- operators should behave exactly the same. The same bug occurs even if the types of a and b are more complex, e.g. Set({x: Int}).

----------------------------- MODULE module -----------------------------
EXTENDS Apalache, Integers

VARIABLES 
    \* @type: Int;
    a,
    \* @type: Int;
    b

InitDeadlock == 
    /\ a = Gen(1)
    /\ b = Gen(1)
    /\ a /= b

InitNoDeadlock == 
    /\ a = Gen(1)
    /\ b = Gen(2)
    /\ a /= b

Next == UNCHANGED <<a,b>>
=============================================================================