AV: Deadcode detection not working for null test after deref

[shaobo-he]

Consider the following program:

struct X {int* p;};

int foo(struct X* x)
{
  int a = x->p;
  if (!x)
    return -1;
  else
    return a;
}

AV does not detect deadcode of the if branch given the blocking condition x != NULL because we disable the assertion assert x != NULL into assume x != NULL when checking inconsistency. The reachability angelic assertion is proved at the beginning therefore the consistency will trivially hold.

To reproduce this issue, please try,
avh null-test-before-deref-null.inst.bpl hinst.bpl /entryPointProc:foo /unknownProc:malloc /unknownProc:$alloc /killAfter:1000 /noAA /deadCodeDetection
avn hinst.bpl /sdv /timeoutEE:200 /timeout:1000 /noEbasic /EE:ignoreAllAssumes+ /dontGeneralize /dumpResults:results.txt /EE:onlySlicAssumes+ /EE:ignoreAllAssumes- /killAfter:3600

[zvonimir]

I am guessing nobody will work on this any time soon, if ever.
@shuvendu-lahiri and @akashlal : are you ok if I mark this as "won't fix" and close the issue?