diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
| commit | 33be652b4db584a8441f7b1006ceed73eb091be6 (patch) | |
| tree | 6050f3143e35fed1b1053e9c9044a516a539d5da /Test/dafny0/MultiSets.dfy | |
| parent | 2e43fe69d087fb75213f67f735a3e85e0278a29f (diff) | |
Dafny: fixed regression tests
Diffstat (limited to 'Test/dafny0/MultiSets.dfy')
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 0bc1004f..e74873e3 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -80,7 +80,7 @@ method test8(a: array<int>, i: int, j: int) method test9(a: array<int>, i: int, j: int, limit: int)
requires a != null && 0 <= i < j < limit <= a.Length;
modifies a;
- ensures old(multiset(a[0..limit])) == multiset(a[0..limit]);
+ ensures multiset(a[0..limit]) == old(multiset(a[0..limit]));
ensures a[j] == old (a[i]) && a[i] == old(a[j]);
ensures forall k :: 0 <= k < limit && k !in {i, j} ==> a[k] == old(a[k]);
{
|