Fix old imperative benchmarks breaking after assertionInjector not ru…

…nning on unfolded functions
epfl-lara · Aug 26, 2021 · f76e4fe · f76e4fe
1 parent e90964b
commit f76e4fe
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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)
 
 }