Collision in address is "possible" as per hevm, even though it's not

[zoep]

Should hevm enforce freshness conditions on newly created symbolic addresses?

I am working with this example:

contract A {
    uint public x;

    constructor ()  {
    x = 42;
    }
}

contract B {

    A a1;
    A a2;

    constructor() {
    a1 = new A();
    a2 = new A();
    assert (address(a1) != address(a2));
    }
}

running hevm symbolic --sig "B()" --code <the-creation-code> returns

Discovered the following counterexamples:

Calldata:
  0x32e7c5bf

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0),(0x1,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

the same happens with --initial-storage Empty.

Removing the assertion results in QED.

[msooseth]

Aliasing bug