Fix issue #489

src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala

@@ -298,7 +298,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
   /**
     * Generates:
     * function arrayConversion(x: [([n]T)@]): ([n]T)°
-    *   requires Footprint[x]
+    *   requires acc(Footprint[x], _)
     *   ensures  [x == result]
     * */
   private val conversionFunc: FunctionGenerator[ComponentParameter] = new FunctionGenerator[ComponentParameter]{
@@ -318,7 +318,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         name = s"${Names.arrayConversionFunc}_${t.serialize}",
         formalArgs = Vector(variable(ctx)(x)),
         typ = vResultType,
-        pres = Vector(pure(addressFootprint(ctx)(x, in.FullPerm(Source.Parser.Internal)))(ctx).res),
+        pres = Vector(pure(addressFootprint(ctx)(x, in.WildcardPerm(Source.Parser.Internal)))(ctx).res),
         posts = Vector(post),
         body = None
       )()

src/test/resources/regressions/issues/000489.gobra

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+pred (t *T) Mem() {
+	acc(t) && t.Cons()
+}
+
+pred (t T) Cons() {
+	t.f[0] == 0
+}
+
+type T struct {
+	f [1]int
+}
+
+preserves acc(t.Mem(), 1/2)
+func (t *T) foo() {
+	unfold acc(t.Mem(), 1/2)
+	unfold acc(t.Cons(), 1/2)
+	fold acc(t.Cons(), 1/2)
+	fold acc(t.Mem(), 1/2)
+	return
+}