removed superfluous lemma calls

nyu-acsys · Oct 29, 2024 · 39154b1 · 39154b1
1 parent a549521
commit 39154b1
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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;