Converting array behind pointer to slice using type definition crashes Gobra

[ThomasMayerl]

For my project, I try to verify code where we have a type that represents an array (with a fixed number of elements). I need to convert this array into a slice. Usually, in Go, we can achieve this by using the [:] syntax. However, the following code causes Gobra to crash:

type arrT [4]int

requires acc(arr)
func tmp(arr *arrT) {
    sl := (*arr)[:]
}

(Usually, in Go, arr[:] (without the dereferencing) should also work but in Gobra I get the error invalid slice with base *arrT and indexes None, None, and None)

The error message I get is:

[info] An unknown Exception was thrown.
[info] class viper.gobra.ast.internal.DefinedT cannot be cast to class viper.gobra.ast.internal.ArrayT (viper.gobra.ast.internal.DefinedT and viper.gobra.ast.internal.ArrayT are in unnamed module of loader 'app')

This issue only happens if we use arrT instead of directly writing [4]int.

[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