diff options
author | wuestholz <unknown> | 2012-09-18 14:57:34 +0200 |
---|---|---|
committer | wuestholz <unknown> | 2012-09-18 14:57:34 +0200 |
commit | 77a38428ffe11806c8bc61d2fbb324d1523de635 (patch) | |
tree | a544307034a09236e297dfe0a3a196597b9f1a7b /Test | |
parent | 27491d37f0eff051033ee85b58f1648c257acdef (diff) |
Dafny: Updated a test that would take a long time (almost 2h) to verify with Z3 4.1.
Diffstat (limited to 'Test')
-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
|