diff options
| author |  Rustan Leino <unknown> | 2013-03-27 13:51:16 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-03-27 13:51:16 -0700 |
| commit | 5296b17758c3e27bf551e9a322323a37983d7abb (patch) | |
| tree | a7c818eedf1608eec0e59ff73ac3ee8356939751 /Test/dafny0/ParallelResolveErrors.dfy | |
| parent | 5f05e3a1c194dcda48115d7b6a1c5777bd2d5287 (diff) | |
The "choose" statement, hacky and specialized as it was, is now gone. Use the assign-such-that statement instead. For example: x :| x in S;
Diffstat (limited to 'Test/dafny0/ParallelResolveErrors.dfy')
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index d3bfe97b..affc765d 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -48,11 +48,6 @@ method M0(IS: set<int>) x := x + 1; // cool
}
- var ia := new int[20];
- forall (i | 0 <= i < 20) {
- ia[i] := choose IS; // error: set choose not allowed
- }
-
var ca := new C[20];
forall (i | 0 <= i < 20) {
ca[i] := new C; // error: new allocation not allowed
|