Map-related unsoundness
marcoeilers opened this issue · 0 comments
marcoeilers commented
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
}