Monolithic BMC generates internal error

[leuschel]

The monolithic symbolic bounded model checking generates an error message for unknown identifiers (cannot find identifier empty'' and S'') for the machine below.

The generated predicate is

S = {} & empty = TRUE & ((#S_n.(#X.(X : POW({"1","8","A","B","Z"}) & S_n = S \/ {X}) & (empty′ = FALSE & S′ = S_n)) or #S_n.(not(empty = TRUE) & S_n : POW(S) & (empty′ = bool(S_n = {}) & S′ = S_n))) & (#S_n′.(#X′.(X′ : POW({"1","8","A","B","Z"}) & S_n′ = S′ \/ {X′}) & (empty′′ = FALSE & S′′ = S_n′)) or #S_n′.(not(empty′ = TRUE) & S_n′ : POW(S′) & (empty′′ = bool(S_n′ = {}) & S′′ = S_n′)))) & ((#S_n′′.(#X′′.(X′′ : POW({"1","8","A","B","Z"}) & S_n′′ = S′′ \/ {X′′}) & (empty′′′ = FALSE & S′′′ = S_n′′)) & /* falsity */ empty : BOOL) or (#S_n′′.(not(empty′′ = TRUE) & S_n′′ : POW(S′′) & (empty′′′ = bool(S_n′′ = {}) & S′′′ = S_n′′)) & /* falsity */ empty : BOOL))

[leuschel]

The machine is

MACHINE prodcons
ABSTRACT_VARIABLES
  S,
  empty
/* PROMOTED OPERATIONS
  Produce,
  Consume */
INVARIANT
    S <: POW(STRING) & empty:BOOL
INITIALISATION
    S,empty : (S = {} & empty = TRUE)
OPERATIONS
  Produce =
    ANY S_n
    WHERE
        #X.(X : POW({"1","8","A","B","Z"}) & S_n = S \/ {X})
    THEN
      empty,S := FALSE,S_n
    END;

  Consume =
    ANY S_n
    WHERE
        not(empty = TRUE)
      & S_n : POW(S)
    THEN
      empty,S := bool(S_n = {}),S_n
    END
DEFINITIONS
  SET_PREF_MAX_OPERATIONS ==
  33;
END

[leuschel]

The file above is available in prob_examples under public_examples/B/Tickets/Github-108/prodcons_b.mch