Map-related unsoundness

[marcoeilers]

The following code verifies (found by @cmatheja):

field values: Map[Int, Ref]

field value: Int

method main()
{
  var x: Ref
  x := new(values)
  x.values := Map()
  assert x.values[1].value > 0
  assert false // verifies
}