Gobra crashes when specifying invariants over a key or value of a range over a map

[ThomasMayerl]

The invariant in the following code makes Gobra crash with the error message java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException:

var cache = map[string]*int{}

requires acc(cache, _) 
requires forall s string :: s in cache ==> acc(cache[s], _)
func key_val_range() {
    invariant acc(cache[k], _)
    for k, v := range cache {
        
    }
}

The same is true when instead of cache[k] v is used:

var cache = map[string]*int{}

requires acc(cache, _) 
requires forall s string :: s in cache ==> acc(cache[s], _)
func key_val_range() {
    invariant acc(v, _)
    for k, v := range cache {
        
    }
}

When adding invariants that match the preconditions, Gobra will report that the invariants cannot be established (even if we add asserts before that work):

var cache = map[string]*int{}

requires acc(cache, _) 
requires forall s string :: s in cache ==> acc(cache[s], _)
func key_val_range() {
    assert acc(cache, _) 
    assert forall s string :: s in cache ==> acc(cache[s], _)

    invariant acc(cache, _) 
    invariant forall s string :: s in cache ==> acc(cache[s], _)
    for k, v := range cache {
        
    }
}

According to the generated Viper code and by manually verifying the generated code, the issue seems to be about missing injectivity. However, even by adding that constraint the generated Viper code can not be verified for holding on loop-entry:

var cache = map[string]*int{}

requires acc(cache, _) 
requires len(cache) > 0
requires forall s string :: s in cache ==> (forall s2 string :: s2 in cache && s != s2 ==> cache[s] != cache[s2])
requires forall s string :: s in cache ==> acc(cache[s], _)
func key_val_range() {
    assert acc(cache, _) 
    assert forall s string :: s in cache ==> (forall s2 string :: s2 in cache && s != s2 ==> cache[s] != cache[s2])
    assert forall s string :: s in cache ==> acc(cache[s], _)

    invariant acc(cache, _) 
    invariant forall s string :: s in cache ==> (forall s2 string :: s2 in cache && s != s2 ==> cache[s] != cache[s2])
    invariant forall s string :: s in cache ==> acc(cache[s], _)
    for k, v := range cache {
        
    }
}

[jcp19]

I wonder if this exception is caused by the iteration variables k and v not being in the scope of the invariant. @Dspil do you have an idea of what is going on here?