Incorrect verification failed when threads write to adjacent memory

[ldr709]

CBMC incorrectly outputs "VERIFICATION FAILED" when giving the following source file.

#include <assert.h>
#include <pthread.h>
#include <stdlib.h>

unsigned long data[2];

void *thread0(void *arg)
{
    data[0] = 1;
    return NULL;
}

void *thread1(void *arg)
{
    data[1] = 1;
    return NULL;
}

int main(int argc, char *argv[])
{
    pthread_t t0;
    pthread_t t1;

    if (pthread_create(&t0, NULL, thread0, NULL))
        abort();
    if (pthread_create(&t1, NULL, thread1, NULL))
        abort();
    if (pthread_join(t0, NULL))
        abort();
    if (pthread_join(t1, NULL))
        abort();

    assert(data[0] == 1);
    assert(data[1] == 1);

    return 0;
}

CBMC output is in this gist.

[kroening]

Added as regression/cbmc-concurrency/norace_array2

[peterschrammel]

Same observation as in #123