From b3954dd7d62d58b1e6f15e6b1a578567b442691c Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 26 Jul 2014 15:36:48 -0700
Subject: deleted the free assume about gates after parallel calls

---
 Source/Concurrency/OwickiGries.cs | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'Source')

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e5201809..23c8945b 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -945,13 +945,6 @@ namespace Microsoft.Boogie
                         ParCallCmd parCallCmd = cmd as ParCallCmd;
                         AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
                         DesugarParallelCallCmd(newCmds, parCallCmd);
-                        if (globalMods.Count > 0 && pc != null)
-                        {
-                            // assume pc || alpha(i, g);
-                            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
-                            assumeExpr.Type = Type.Bool;
-                            newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
-                        }
                         HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
                         linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
                         Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
-- 
cgit v1.2.3