From 5b178fc570f09661fba1ac1bc4e987fa39b68d23 Mon Sep 17 00:00:00 2001
From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Date: Wed, 13 Sep 2023 21:21:16 +0200
Subject: [PATCH] Slice from array didn't have termination measure (#674)

---
 .../gobra/translator/encodings/slices/SliceEncoding.scala     | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
index 6171920e1..7dc2c151f 100644
--- a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -509,6 +509,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
     *   ensures slen(result) == j - i
     *   ensures scap(result) == alen(a) - i
     *   ensures sarray(result) == a
+    *   decreases _
     * {
     *   sfullSliceFromArray(a, i, j, alen(a))
     * }
@@ -525,6 +526,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
       val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative")
       val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound")
       val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, ctx.array.len(aDecl.localVar)()))("The high bound of the slice might exceed the array capacity")
+      val pre4 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       // postconditions
       val result = vpr.Result(ctx.slice.typ(typ))()
@@ -545,7 +547,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
         s"${Names.sliceFromArray}_${Names.serializeType(typ)}",
         Seq(aDecl, iDecl, jDecl),
         ctx.slice.typ(typ),
-        Seq(pre1, pre2, pre3),
+        Seq(pre1, pre2, pre3, pre4),
         Seq(post1, post2, post3, post4),
         if (generateFunctionBodies) Some(body) else None
       )()