Pointer comparison can be used to drop unrelated execution paths #12

I was investigating results in reachsafety category again and an interesting issue popped up.
Symbiotic version is:

version: 7.0.0-dev
LLVM version: 8.0.1
symbiotic            -> 2e2ceb4735887125c1c81e4194f8cad8eb0409e7 (Release)
dg                   -> ccbc3536de659896c4ecac7f4b619733b14b5b9a (Release)
sbt-slicer           -> 85c8cb482fecdd065329a55551bae93af2408c7b (Release)
sbt-instrumentation  -> 62c481990db07679f3e3e0e086d5c27a6d28f757 (Release)
klee                 -> 236d99208f15e125aa89008c9652965ad89d3005 (Release)

I ran Symbiotic like this: ./symbiotic --no-slice --sv-comp --save-files --prp sv-benchmarks/c/properties/unreach-call.prp ldv_malloc.c and it reported true, but my expected result was false.

ldv_malloc.c:

extern int __VERIFIER_nondet_int();
extern void abort(void);
extern void *malloc(unsigned long);
void reach_error(void) {}

int ldv_is_err(void *ptr) {
    const unsigned long errs = ((unsigned long) -4095);
    unsigned long p = (unsigned long) ptr;
    return p > errs;
}

void assume_abort_if_not(int cond) {
    if (!cond) {
        abort();
    }
}

void *ldv_malloc(unsigned long size) {
    if (__VERIFIER_nondet_int())
        return 0;
    void *p = malloc(size);
    assume_abort_if_not(!ldv_is_err(p));
    return p;
}

int main()
{
    void *a = ldv_malloc(512);
    if (a != 0)
        reach_error();
    free(a);
    return 0;
}

Commenting out the call of assume_abort_if_not solves the problem. I suspect that assume_abort_if_not drops all the execution paths where klee decides not to return 0 from ldv_malloc. The expected behavior is to define constraints on the pointer's numeric value. I believe this is the cause of many incorrect true answers we have in Linux drivers ReachSafety as ldv_is_err is used very often in those benchmarks.

Possibly related to fix for staticafi/symbiotic#174