Gobra's append is unable to preserve invariant

[ThomasMayerl]

If we assume a function that takes in a slice of strings and we want to convert that to a map mapping from strings to slices of strings (in the real world example, the key would be some hash, s.t. all the strings with the same hash land in the same slice). If we take Gobra's append, Gobra is unable to prove that after the append the condition that for all processed strings of the initial slice, there is some entry in a slice in the map, that matches it, still holds:

requires acc(m)
ensures res === let arr, ok := m[str] in arr
decreases
pure func getFromMap(m map[string][]string, str string) (res []string)

requires acc(strs)
requires len(strs) > 0
func tmp(strs []string) {
    m := map[string][]string{}
    invariant 0 <= i && i <= len(strs)
    invariant acc(m)
    invariant acc(strs)
    invariant forall str string :: {m[str]} {getFromMap(m, str)} str in domain(m) ==> getFromMap(m, str) === m[str]
    invariant forall str string, k int :: {&getFromMap(m, str)[k]} str in domain(m) && 0 <= k && k < len(getFromMap(m, str)) ==> acc(&getFromMap(m, str)[k])
    invariant forall k int :: {&strs[k]} 0 <= k && k < idx ==> exists str string, l int :: {&getFromMap(m, str)[l]} str in domain(m) && 0 <= l && l < len(getFromMap(m, str)) && strs[k] == getFromMap(m, str)[l]
    for i, str := range(strs) with idx {
        v := m[str]
        if v == nil {
            m[str] = []string{}
        }
        entry, _ := m[str]
        m[str] = append(perm(1/2), entry, str)
    }
}

The error message I get is:

Loop invariant might not be preserved. 
[info] Assertion forall k int :: {&strs[k]} 0 <= k && k < idx ==> exists str string, l int :: {&getFromMap(m, str)[l]} str in domain(m) && 0 <= l && l < len(getFromMap(m, str)) && strs[k] == getFromMap(m, str)[l] might not hold.

If I write an append on my own, it seems to work:

requires acc(m)
ensures res === let arr, ok := m[str] in arr
decreases
pure func getFromMap(m map[string][]string, str string) (res []string)

requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k])
ensures forall k int :: {&newArr[k]} 0 <= k && k < len(newArr) ==> acc(&newArr[k]) 
ensures len(newArr) == old(len(arr)) + 1
ensures newArr[len(newArr) - 1] == toAdd
ensures forall k int :: {&newArr[k]} {&arr[k]} 0 <= k && k < len(arr) ==> old(arr[k]) == newArr[k]
func app(arr []string, toAdd string) (newArr []string)

requires acc(strs)
requires len(strs) > 0
func tmp(strs []string) {
    m := map[string][]string{}
    invariant 0 <= i && i <= len(strs)
    invariant acc(m)
    invariant acc(strs)
    invariant forall str string :: {m[str]} {getFromMap(m, str)} str in domain(m) ==> getFromMap(m, str) === m[str]
    invariant forall str string, k int :: {&getFromMap(m, str)[k]} str in domain(m) && 0 <= k && k < len(getFromMap(m, str)) ==> acc(&getFromMap(m, str)[k])
    invariant forall k int :: {&strs[k]} 0 <= k && k < idx ==> exists str string, l int :: {&getFromMap(m, str)[l]} str in domain(m) && 0 <= l && l < len(getFromMap(m, str)) && strs[k] == getFromMap(m, str)[l]
    for i, str := range(strs) with idx {
        v := m[str]
        if v == nil {
            m[str] = []string{}
        }
        entry, _ := m[str]
        m[str] = app(entry, str)
    }
}