diff options
author | wuestholz <unknown> | 2012-09-18 14:57:34 +0200 |
---|---|---|
committer | wuestholz <unknown> | 2012-09-18 14:57:34 +0200 |
commit | b2d4485e611149d2cf1e8998a60b186090cd3e80 (patch) | |
tree | b60e9b91f9bb324e14444b8fff23aa6b20005076 | |
parent | 7f821fd8842255765b74b7fc14789fe4364271ce (diff) |
Dafny: Updated a test that would take a long time (almost 2h) to verify with Z3 4.1.
-rw-r--r-- | Test/VSComp2010/Problem2-Invert.dfy | 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
|