Problem with static check on function application in the arrays encoding

[rodrigo7491]

Description

Work on #1461 exposed a bug with function application in the arrays encoding. In the case which the function's arguments can be computed statically the application's result is not being computed correctly.

Input specification

This problem was found on the mis spec.

The command line parameters used to run the tool

apalache-mc check --length=5 --inv=IsIndependent --smt-encoding=arrays mis.tla

Expected behavior

No error.

System information

• Apalache version [apalache-mc version]: v0.22.1-201-gbfdcd7d2
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Linux Mint 20.2
• JDK version [e.g. OpenJDK 0.8.0]: openjdk 11.0.14 2022-01-18

Additional context

CEX generated:

---------------------------- MODULE counterexample ----------------------------

EXTENDS mis

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 ==
  Nb = { <<1, 2>>, <<2, 1>> }
    /\ awake = SetAsFun({ <<1, TRUE>>, <<2, TRUE>>, <<3, TRUE>> })
    /\ msgs = SetAsFun({ <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ rem_nbrs = SetAsFun({ <<1, {2}>>, <<2, {1}>>, <<3, {}>> })
    /\ round = 1
    /\ status
      = SetAsFun({ <<1, "unknown">>, <<2, "unknown">>, <<3, "unknown">> })
    /\ val = SetAsFun({ <<1, 80>>, <<2, 1>>, <<3, 1>> })

(* Transition 0 to State1 *)
State1 ==
  Nb = { <<1, 2>>, <<2, 1>> }
    /\ awake = SetAsFun({ <<1, TRUE>>, <<2, TRUE>>, <<3, TRUE>> })
    /\ msgs
      = SetAsFun({ <<
          1, { [src |-> 1, type |-> "val", val |-> 81],
            [src |-> 2, type |-> "val", val |-> 81] }
        >>,
        <<2, {[src |-> 1, type |-> "val", val |-> 81]}>>,
        <<3, {}>> })
    /\ rem_nbrs = SetAsFun({ <<1, {2}>>, <<2, {1}>>, <<3, {}>> })
    /\ round = 2
    /\ status = SetAsFun({ <<1, "winner">>, <<2, "winner">>, <<3, "winner">> })
    /\ val = SetAsFun({ <<1, 77>>, <<2, 5>>, <<3, 27>> })

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation ==
  Skolem((\E edge$2 \in Nb:
    status[edge$2[1]] = "winner" /\ status[edge$2[2]] = "winner"))

================================================================================