Pointer encoding renders comparison wrongly constant

[tautschnig]

The following is a condensed version of the single benchmark that CBMC got wrong in SV-COMP'17:

#include <stdlib.h>

int main()
{
  if(sizeof(void*)!=8)
    return 0;

  char* p=malloc(1);
  if(p==0)
    return 0;

  unsigned long x=0xFFFFFFFF;
  if((unsigned long)p > x) // unsoundly evaluates to true due to pointer encoding
    return 0;

  __CPROVER_assert(0, "");

  return 0;
}

This is related to #311.