From 3529462400ccbd5e92ee50b0fb95fb5978ebec4a Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 17 Jan 2012 16:32:16 -0800
Subject: Dafny: allow parallel statements with an empty list of bound
 variables

---
 Source/Dafny/Compiler.cs | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Source/Dafny/Compiler.cs')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index c2cb9353..6ede64fb 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -907,6 +907,10 @@ namespace Microsoft.Dafny {
         if (s.Kind != ParallelStmt.ParBodyKind.Assign) {
           // Call and Proof have no side effects, so they can simply be optimized away.
           return;
+        } else if (s.BoundVars.Count == 0) {
+          // the bound variables just spell out a single point, so the parallel statement is equivalent to one execution of the body
+          TrStmt(s.Body, indent);
+          return;
         }
         var s0 = (AssignStmt)s.S0;
         if (s0.Rhs is HavocRhs) {
-- 
cgit v1.2.3