diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 6c0cfe81..457bc894 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -54,6 +54,7 @@ class Array { method Set(i: int, x: int);
requires 0 <= i && i < |contents|;
modifies this;
+ ensures |contents| == |old(contents)|;
ensures contents[..i] == old(contents[..i]);
ensures contents[i] == x;
ensures contents[i+1..] == old(contents[i+1..]);
|