Identity comparison with other slices fails after appending to slice

[ThomasMayerl]

If we use append, Gobra is unable to prove that the slice we appended to is still different (by identity - comparing using ===/!==) from other slices. In the following code, the fold acc_cache(dict(cache)) fails due to Gobra not being able to prove injectivity over acc_slice. Indeed, the first assert succeeds, whereas the one after the append fails.

var cache@ = map[string][]string{}

requires acc(&cache, 1/2)
requires acc(cache, 1/2)
ensures res === let entry, ok := cache[str] in entry
decreases
pure func getSliceFromCache(str string) (res []string)

pred acc_slice(sl []string) {
    forall k int :: {&sl[k]} 0 <= k && k < len(sl) ==> acc(&sl[k])
}

pred acc_cache(cache dict[string][]string) {
    forall str string :: {str in domain(cache)} str in domain(cache) ==> acc_slice(cache[str])
}

requires acc(&cache)
requires acc(cache)
requires acc_cache(dict(cache))
requires key in domain(cache)
ensures acc(&cache)
ensures acc(cache)
ensures acc_cache(dict(cache))
func tmp(key string, str string) {
    unfold acc_cache(dict(cache))
    unfold acc_slice(cache[key])
    assert forall str string :: {cache[str]} str in cache && str != key ==> cache[str] !== cache[key]
    cache[key] = append(perm(1), getSliceFromCache(key), str)
    assert forall str string :: {cache[str]} str in cache && str != key ==> cache[str] !== cache[key]
    fold acc_slice(cache[key])
    fold acc_cache(dict(cache))
}