Support C99 semantics of `restrict` pointers

[fbrausse]

Example:

#include <assert.h>

void f(void *restrict a, void *restrict b)
{
    assert(a != b);
}

esbmc --func f reports a counter-example, by setting a == b. However, a conforming C program is not allowed to call f with a == b, so I wonder whether ESBMC should adhere to this "conformance" when assigning nondet values to both variables.

[rafaelsamenezes]

As a entry point I would say that adding the assumption that a != b seems reasonable.