From 39154b18ac00e788710bd55090d045e18ce6c1c2 Mon Sep 17 00:00:00 2001
From: Ekanshdeep Gupta <ekanshdeep_gupta@yahoo.co.in>
Date: Mon, 28 Oct 2024 21:26:31 -0400
Subject: [PATCH] removed superfluous lemma calls

---
 test/iterated-star/array-max.rav | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test/iterated-star/array-max.rav b/test/iterated-star/array-max.rav
index 98646da..5e4f46f 100644
--- a/test/iterated-star/array-max.rav
+++ b/test/iterated-star/array-max.rav
@@ -33,8 +33,9 @@ module ArrayMax[M: IArray] {
     ensures  M.len(a) == 0 ? x == -1 : (0 <= x && x < M.len(a))
     ensures  is_max(x, m, M.len(a))
   {
-    M.all_diff();
-    M.len_nonneg();
+    // No longer needed, since autoLemma dependencies have been added.
+    // M.all_diff();
+    // M.len_nonneg();
     var z : Int;
     if (M.len(a) == 0) {
       x := -1;