witemap

The following spec causes Gobra to crash: ``` ensures forall e int :: e in s1 ==> e in s2 pure func test(ghost s1 set[int]) (ghost s2 set[any]) ``` The...