From 77a38428ffe11806c8bc61d2fbb324d1523de635 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 18 Sep 2012 14:57:34 +0200
Subject: Dafny: Updated a test that would take a long time (almost 2h) to
 verify with Z3 4.1.

---
 Test/VSComp2010/Problem2-Invert.dfy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Test/VSComp2010')

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
-- 
cgit v1.2.3