[BUG] Sets becoming unconstrained after set minus operation

[rodrigo7491]

Description

In the arrays encoding, when set minus is used it leaves the updated set unconstrained. This is due to a break in the chain of SSA constraints.

Input specification

This bug was found when testing the encoding with SetSndRcv.tla.

The command line parameters used to run the tool

check --inv=Inv --smt-encoding=arrays --length=4 --cinit=CInit4 SetSndRcv.tla

Expected behavior

No invariant violation.

Additional context

Counter-example generated:

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

EXTENDS SetSndRcv

(* Constant initialization state *)
ConstInit == Values = { 0, 1, 2, 3, 4 }

(* Initial state *)
State0 ==
  Values = { 0, 1, 2, 3, 4 }
    /\ medium = {}
    /\ receiver = {}
    /\ sender = { 0, 1, 2, 3, 4 }

(* Transition 0 to State1 *)
State1 ==
  Values = { 0, 1, 2, 3, 4 }
    /\ medium = {0}
    /\ receiver = {}
    /\ sender = { 1, 2, 3, 4 }

(* Transition 1 to State2 *)
State2 ==
  Values = { 0, 1, 2, 3, 4 }
    /\ medium = {0}
    /\ receiver = {}
    /\ sender = {}

(* Transition 1 to State3 *)
State3 == Values = { 0, 1, 2, 3, 4 }/\ medium = {}/\ receiver = {}/\ sender = {}

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == sender = {} /\ medium = {} /\ receiver = {}

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