Fuzzer doesn't adjust function names or LitmusIDs when deleting functions

[MattWindsor91]

Observe the following output from a fuzzer run:

C SBSC

{
    iSTVWu0PW = -362;
    QDuEO8OibYwf = -2147483648;
    CLQ2FaUXOX3 = 438966;
    I5ez4Q = 32487;
    pAbVAxkp = 86706;
    SPYl53okzl = -2147483648;
    PgM2rwhrEn1 = 1842531;
    BDB8xlzjIfin = -186754;
    x = 0;
    y = 0;
}

void
P1(int *BDB8xlzjIfin, atomic_bool *CLQ2FaUXOX3, int *I5ez4Q,
   bool *PgM2rwhrEn1, atomic_int *QDuEO8OibYwf, atomic_bool *SPYl53okzl,
   int *iSTVWu0PW, atomic_int *pAbVAxkp, atomic_int *x, atomic_int *y)
{
    int a;
    atomic_store_explicit(x, 1, memory_order_relaxed);
    a = atomic_load_explicit(y, memory_order_relaxed);
}

void
P2(int *BDB8xlzjIfin, atomic_bool *CLQ2FaUXOX3, int *I5ez4Q,
   bool *PgM2rwhrEn1, atomic_int *QDuEO8OibYwf, atomic_bool *SPYl53okzl,
   int *iSTVWu0PW, atomic_int *pAbVAxkp, atomic_int *x, atomic_int *y)
{
    int a;
    atomic_store_explicit(y, 1, memory_order_relaxed);
    atomic_store_explicit(QDuEO8OibYwf, 180, memory_order_relaxed);
    a = atomic_load_explicit(x, memory_order_relaxed);
}

exists (0:a == 0 /\ 1:a == 0)

Note that:

• P0 is missing (it's been deleted);
• the postcondition still refers to 0 and 1, despite the threads actually being called 1 and 2;
• both of these taken together confuse the absolute Fanny Cradock out of litmus.

The fuzzer needs to take more care when dropping empty programs, and needs to remember to revise litmus IDs upwards and downwards whenever it changes the program list.

[MattWindsor91]

It does now, to the best of my knowledge.