diff options
Diffstat (limited to 'Test/dafny0/TypeAntecedents.dfy')
| -rw-r--r-- | Test/dafny0/TypeAntecedents.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 5982a9e6..b6ef0d68 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -68,8 +68,8 @@ method M(list: List, S: set<MyClass>) returns (ret: int) ghost var l := NF();
assert l != null ==> l.H() == 5;
- foreach (s in S) {
- assert s == null || s.H() == 5;
+ parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }
+ parallel (s | s != null && s in S) {
s.x := 0;
}
|