Indirect pointer arithmetics on different memory objects confuses klee

[tomsik68]

Verifying memsafety of the following program using Symbiotic confuses klee:

#include <stdlib.h>
#include <stddef.h>

int main()
{
    int *a = malloc(1000*sizeof(int));
    int *b = malloc(1000*sizeof(int));

    ptrdiff_t diff = a - b;

    if (diff > 0) {
        free(a);
        free(b);
    }

    return 0;
}

This program compares pointers, but does it indirectly using subtraction as an intermediate step.

I expect Symbiotic to answer consistently. However, Symbiotic's answer varies -- sometimes it is true, sometimes false(valid-memtrack) and sometimes unknown when slicing is enabled.

This could be because klee returns concrete addresses from malloc instead of symbolic ones. However, klee should be able to detect these two things:

1. the pointer comparison
2. the subtraction uses addresses of two different blocks, which is undefined in C (C11 6.5.6.9)