summaryrefslogtreecommitdiff
path: root/Source/Concurrency
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-07-26 15:36:48 -0700
committerGravatar qadeer <unknown>2014-07-26 15:36:48 -0700
commitb3954dd7d62d58b1e6f15e6b1a578567b442691c (patch)
treefe9ad386ec6824484cae6b26a8a83ff3a6681350 /Source/Concurrency
parent315922109c235044f985ca19e1bfbe5b95d1873c (diff)
deleted the free assume about gates after parallel calls
Diffstat (limited to 'Source/Concurrency')
-rw-r--r--Source/Concurrency/OwickiGries.cs7
1 files changed, 0 insertions, 7 deletions
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);