From 32896953d0067517985e7d93cce63e26d7b53af8 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 1 Feb 2024 09:26:30 -0800
Subject: [PATCH] Make VSComp2010/Problem2-Invert.dfy less brittle

---
 .../LitTest/VSComp2010/Problem2-Invert.dfy    | 23 ++++++++++---------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSComp2010/Problem2-Invert.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSComp2010/Problem2-Invert.dfy
index a7aed1b457a..0400e868a1d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSComp2010/Problem2-Invert.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSComp2010/Problem2-Invert.dfy
@@ -49,19 +49,20 @@ ghost function inImage(i: int): bool { true }  // this function is used to trigg
 method Main()
 {
   var a := new int[] [9, 3, 8, 2, 7, 4, 0, 1, 5, 6];
-  assert a[0] == 9;
-  assert a[1] == 3;
-  assert a[2] == 8;
-  assert a[3] == 2;
-  assert a[4] == 7;
-  assert a[5] == 4;
-  assert a[6] == 0;
-  assert a[7] == 1;
-  assert a[8] == 5;
-  assert a[9] == 6;
-
   var b := new int[10];
 
+  assert forall m :: 0 <= m < 10 && inImage(m) ==> exists k :: 0 <= k < 10 && a[k] == m by {
+    assert a[0] == 9;
+    assert a[1] == 3;
+    assert a[2] == 8;
+    assert a[3] == 2;
+    assert a[4] == 7;
+    assert a[5] == 4;
+    assert a[6] == 0;
+    assert a[7] == 1;
+    assert a[8] == 5;
+    assert a[9] == 6;
+  }
   M(10, a, b);
   print "a: ", a[..], "\n";
   print "b: ", b[..], "\n";