summaryrefslogtreecommitdiff
path: root/Test/dafny0/Parallel.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
-rw-r--r--Test/dafny0/Parallel.dfy11
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 817120ce..539974fd 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -187,3 +187,14 @@ method DuplicateUpdate() {
}
}
}
+
+ghost method DontDoMuch(x: int)
+{
+}
+
+method OmittedRange() {
+ parallel (x) { }
+ parallel (x) {
+ DontDoMuch(x);
+ }
+}