diff --git a/frontends/benchmarks/imperative/valid/ArrayParamMutation2.scala b/frontends/benchmarks/imperative/valid/ArrayParamMutation2.scala
index f7d5919227..db71a15d0a 100644
--- a/frontends/benchmarks/imperative/valid/ArrayParamMutation2.scala
+++ b/frontends/benchmarks/imperative/valid/ArrayParamMutation2.scala
@@ -4,13 +4,13 @@ object ArrayParamMutation2 {
 
   def rec(a: Array[BigInt]): BigInt = {
     require(a.length > 1 && a(0) >= 0)
-    if(a(0) == 0) 
+    if(a(0) == 0)
       a(1)
     else {
       a(0) = a(0) - 1
       a(1) = a(1) + a(0)
       rec(a)
     }
-  } ensuring(res => a(0) == 0)
+  } ensuring(res => a.length > 0 && a(0) == 0)
 
 }
diff --git a/frontends/benchmarks/imperative/valid/ArrayParamMutation3.scala b/frontends/benchmarks/imperative/valid/ArrayParamMutation3.scala
index a1e0ab941e..d3731de83f 100644
--- a/frontends/benchmarks/imperative/valid/ArrayParamMutation3.scala
+++ b/frontends/benchmarks/imperative/valid/ArrayParamMutation3.scala
@@ -9,7 +9,7 @@ object ArrayParamMutation3 {
       a(0) = a(0) - 1
       even(a)
     }
-  } ensuring(res => a(0) == 0)
+  } ensuring(res => a.length > 0 && a(0) == 0)
 
   def even(a: Array[BigInt]): Boolean = {
     require(a.length > 0 && a(0) >= 0)
@@ -18,6 +18,6 @@ object ArrayParamMutation3 {
       a(0) = a(0) - 1
       odd(a)
     }
-  } ensuring(res => a(0) == 0)
+  } ensuring(res => a.length > 0 && a(0) == 0)
 
 }