property ShouldUseEntries start -> start: * start -> gotKeys: "Map.keySet"(M, S) => m := M; s := S gotKeys -> iteratingKeys: "Set.iterator"(S, I) when S == s => i := I iteratingKeys -> iteratingKeys: * iteratingKeys -> gotOneKey: "Iterator.next"(I, K) when I == i => k := K gotOneKey -> error: ".*Map.get"(M, K, IgnoreRet) when M == m && K == k