[BUG] Out of order assignments

[konnov]

Something has changed in the behavior of the assignment finder and type checker between 0.6.0 and unstable.

Now the following test fails:

cd $HOME/devl/apalache-tests/performance/bcastByz
$HOME/devl/apalache/bin/apalache-mc check --length=1 \
  --init=IndInv_Unforg_NoBcast --inv=IndInv_Unforg_NoBcast --cinit=ConstInit4 APAbcastByz.tla

Apalache fails with the message:

Step 0, level 0: checking if 1 transition(s) are enabled and violate the invariant I@15:55:37.782
APAbcastByz.tla:182:6-182:36, '(...), type error: Failed to find type of variable sent' E@15:55:37.798
APAbcastByz.tla:182:6-182:36, =(...), type error: Expected a Boolean, found: None E@15:55:37.803
APAbcastByz.tla:183:34-183:50, '(...), type error: Failed to find type of variable sent' E@15:55:37.808
APAbcastByz.tla:183:15-183:54, [S -> T](...), type error: Expected a finite set, found: None E@15:55:37.811
The outcome is: Error                                             I@15:55:37.843
Checker has found an error                                        I@15:55:37.843
It took me 0 days  0 hours  0 min  2 sec                          I@15:55:37.846
Total time: 2.121 sec                                             I@15:55:37.846
EXITCODE: OK

The reason for that is that sent' is assigned a value after it is used:

Init$0 ==
  (BMC!Skolem((\E t_18$1 \in [Corr -> { "V0", "V1", "SE", "AC" }]: pc' <- t_18$1))
      /\ Corr \in SUBSET (Corr \union Faulty)
      /\ Faulty \in SUBSET (Corr \union Faulty)
      /\ BMC!Skolem((\E t_1b$1 \in SUBSET ({
        <<t_19$1, t_1a$1>>:
          t_19$1 \in Corr \union Faulty,
          t_1a$1 \in {"ECHO"}
      }):
        sent' = t_1b$1))
      /\ BMC!Skolem((\E t_1e$1 \in [Corr
        -> SUBSET (sent'
          \union { <<t_1c$1, t_1d$1>>: t_1c$1 \in Faulty, t_1d$1 \in {"ECHO"} })]:
        rcvd' <- t_1e$1)))
    /\ sent' <- ({} <: {<<Int, STRING>>})
    /\ pc' = [ i$1 \in Corr |-> "V0" ]

We have been discussing for some time that the assignment finder should change the order of subformulas so that the assignments always come first. For some reason, the assignment finder always picks the assignment under the existential,
even if we swap the subformulas.