From 5cfd22fcc3c6584d6e105ad4fbeb3f5ccc90ef7a Mon Sep 17 00:00:00 2001
From: Georg Stefan Schmid <georg.schmid@epfl.ch>
Date: Sat, 16 Jan 2021 11:32:22 +0100
Subject: [PATCH] Fix old imperative benchmarks breaking after
 assertionInjector not running on unfolded functions

---
 .../benchmarks/imperative/valid/ArrayParamMutation2.scala     | 4 ++--
 .../benchmarks/imperative/valid/ArrayParamMutation3.scala     | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

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)
 
 }