ThomasMayerl

I have found another case where this issue can still be reproduced: DCE works in the following snippet: ```c #include void DCEMarker0_(); void f(bool s, bool c, bool r, bool...

> Manually specifying the following triggers solves the problem: > > ``` > package test5 > > type Bar struct { > } > > type FooCacheEntry struct { >...

The following is another example of where the issue shows up. Gobra cannot prove that we have access to arr[k] for the second acc(..) in the invariant even though the...

Then invalid triggers are inserted again by Gobra, meaning that Viper cannot verify the assertions

In this instance, the triggers seem to be the issue. The correct invariant would be ```go forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> forall k int...

Also the Viper code doesn't seem to terminate. However, e.g. removing the assert false manually in the generated Viper code, makes Viper terminate again, so this might be a Viper...

Here's a smaller example (not using predicates) where this issue occurs. In this instance, the struct needs to have at least three string slices and the permission must be less...

`requires forall k int :: {&arr[k]} 0 acc(&arr[k]) && acc(arr[k], 1/2)` expands to ```go requires forall k int :: {&arr[k]} 0 acc(&arr[k]) requires forall k int :: {&arr[k]} 0 acc(&arr[k].strs,...

Note: This only works for slices, not for maps. If we don't specify triggers for the same code just with maps, then Gobra will generate equal triggers for the different...

For maps, a (not so nice) workaround, would be the following (note how we have to change the code from m["test"] to getElemsFromMap(m, "test") so that the triggers match): ```go...