ThomasMayerl

So I think the issue is that at https://github.com/viperproject/gobra/blob/5d748d4e45f9eb824899f4216ac27594cec8c244/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala#L103 we try to cast something of type DefinedT to type ArrayT, a subtyping relation that does not exist in Scala

A fix like the one from #940 does not seem to work. Probably because primaryExpr can also contain parentheses. Maybe we can find a similar syntactic way

So far, I found two possible solutions for an improved syntax. In the rule for reveal (REVEAL primaryExpr arguments) we can either put the parentheses only around primaryExpr (allowing something...

So what happens is that Gobra basically creates a conditional, where, if `len(x) == 0`, we don't create any assumptions about i, nor i0. We just assume that `i ==...

Yes, with ints the same issue is reproducible. For example, the following code shows the same issue: ```go requires acc(cache, 1/2) ensures res === let entry, ok := cache[key] in...

Another interesting aspect: If we access the map entry that we have access to, then we suddenly receive a postcondition error, that injectivity cannot be proven, instead of the assertion...

Upon further inspection, I think that Gobra is unable to reason about this with the addition of the getSlice function. However, we need this to specify valid triggers (this is...

I do think that the problem is that the triggers are not issued and when we change the map that Z3 cannot prove anymore that the conditions hold since nothing...

Another (temporary) workaround seems to be to combine using the map triggers and a function call by adding an assertion that the map access equals the function call, like so:...