Dafny: Updated a test that would take a long time (almost 2h) to verify with Z3 4.1.

1 files changed, 1 insertions, 0 deletions

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 2a262d70..0f7c50c1 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -43,6 +43,7 @@ method M(N: int, A: array<int>, B: array<int>)
   assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i]));  // the elements of A were not changed by the loop

   // it now follows from the surjectivity of A that A is the inverse of B:

   assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);

+  assert (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);

 }

 

 static function inImage(i: int): bool { true }  // this function is used to trigger the surjective quantification