diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
index 343e66fd4..5eb0a288e 100644
--- a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -340,6 +340,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * function arrayDefault(): ([n]T)°
     *   ensures len(result) == n
     *   ensures Forall idx :: {result[idx]} 0 <= idx < n ==> [result[idx] == dflt(T)]
+    *   decreases _
     * */
   private val exDfltFunc: FunctionGenerator[ComponentParameter] = new FunctionGenerator[ComponentParameter]{
     def genFunction(t: ComponentParameter)(ctx: Context): vpr.Function = {
diff --git a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
index 8424c6775..cd81a08c0 100644
--- a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
@@ -226,6 +226,7 @@ class SequenceEncoding extends LeafTypeEncoding {
     *   requires 0 <= n
     *   ensures |result| == n
     *   ensures forall i : Int :: { result[i] } 0 <= i < n ==> result[i] == dfltVal(`T`)
+    *   decreases _
     * }}}
     */
   private val emptySeqFunc: FunctionGenerator[in.Type] = new FunctionGenerator[in.Type] {