Pointer initialized via integer literal to same address as allocated memory does not point to same memory

[danpoe]

#include <assert.h>
#include <stdlib.h>

void main()
{
  char *p = malloc(1);
  __CPROVER_assume(__CPROVER_POINTER_OBJECT(p) == 2);
  assert(0); // fails as expected

  // same value as the malloc'd pointer above
  char *q = (char *)((size_t)2 << sizeof(char *) * 8 - 8);

  *p = 1;
  *q = 2;

  assert(*p == 1); // currently succeeds
}

The problem is likely that q indexes into __CPROVER_memory whereas p targets the malloced memory.

CBMC version: 03ab5c7
Operating system: Ubuntu
Exact command line resulting in the issue: cbmc --pointer-check --no-simplify --no-propagation main.c
What behaviour did you expect: verification failed
What happened instead: verification successful