deleted the free assume about gates after parallel calls

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);