From 4d73949ea5ec0859669f58acbf2b0c85773de55b Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Thu, 14 Sep 2023 16:43:33 +0200
Subject: [PATCH] sliceconstruct termination measure

---
 .../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 7dc2c151f..5590c54f7 100644
--- a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -342,6 +342,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
     *   ensures soffset(result) == offset
     *   ensures slen(result) == len
     *   ensures scap(result) == cap
+    *   dereases _
     * }}}
     */
   private val constructGenerator : FunctionGenerator[vpr.Type] = new FunctionGenerator[vpr.Type] {
@@ -357,6 +358,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
       val pre2 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), lenDecl.localVar))("Slice length might be negative")
       val pre3 = synthesized(vpr.LeCmp(lenDecl.localVar, capDecl.localVar))("Slice length might exceed capacity")
       val pre4 = synthesized(vpr.LeCmp(vpr.Add(offsetDecl.localVar, capDecl.localVar)(), ctx.array.len(aDecl.localVar)()))("Slice capacity might exceed the capacity of the underlying array")
+      val pre5 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       // postconditions
       val result = vpr.Result(ctx.slice.typ(typ))()
@@ -369,7 +371,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
         s"${Names.sliceConstruct}_${Names.serializeType(typ)}",
         Seq(aDecl, offsetDecl, lenDecl, capDecl),
         ctx.slice.typ(typ),
-        Seq(pre1, pre2, pre3, pre4),
+        Seq(pre1, pre2, pre3, pre4, pre5),
         Seq(post1, post2, post3, post4),
         None
       )()