Merge

14 files changed, 334 insertions, 290 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);

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d6ac8754..d961eb3e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2434,6 +2434,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "preconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitRequires(this);

+    }

   }

 

   public class Ensures : Absy, IPotentialErrorNode {

@@ -2528,6 +2532,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "postconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitEnsures(this);

+    }

   }

 

   public class Procedure : DeclWithFormals {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7e71453b..33b3a818 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2122,12 +2122,16 @@ namespace Microsoft.Boogie {
         return false;

 

       NAryExpr other = (NAryExpr)obj;

-      return this.Args.ListEquals(other.Args) && object.Equals(this.Fun, other.Fun); 

+      return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args);

     }

     [Pure]

     public override int GetHashCode() {

       int h = this.Fun.GetHashCode();

-      h ^= this.Args.GetHashCode();

+      // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references

+      // We want structural equality

+      foreach (var arg in Args) {

+        h = (97*h) + arg.GetHashCode();

+      }

       return h;

     }

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9425f698..32985053 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -103,20 +103,35 @@ namespace Microsoft.Boogie {
 

       var other = (BinderExpr) obj;

 

-      var a = this.TypeParameters.ListEquals(other.TypeParameters);

-      var b = this.Dummies.ListEquals(other.Dummies);

-      var c = !CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes);

-      var d = object.Equals(this.Body, other.Body);

-

-      return a && b && c && d;

+      return this.TypeParameters.SequenceEqual(other.TypeParameters)

+             && this.Dummies.SequenceEqual(other.Dummies)

+             && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))

+             && object.Equals(this.Body, other.Body);

     }

 

     [Pure]

     public override int GetHashCode() {

-      int h = this.Dummies.GetHashCode();

       // Note, we don't hash triggers and attributes

+   

+      // DO NOT USE Dummies.GetHashCode() because we want structurally

+      // identical Expr to have the same hash code **not** identical references

+      // to have the same hash code.

+      int h = 0;

+      foreach (var dummyVar in this.Dummies) {

+        h = ( 53 * h ) + dummyVar.GetHashCode();

+      }

+

       h ^= this.Body.GetHashCode();

-      h = h * 5 + this.TypeParameters.GetHashCode();

+

+      // DO NOT USE TypeParameters.GetHashCode() because we want structural

+      // identical Expr to have the same hash code **not** identical references

+      // to have the same hash code.

+      int h2 = 0;

+      foreach (var typeParam in this.TypeParameters) {

+        h2 = ( 97 * h2 ) + typeParam.GetHashCode();

+      }

+

+      h = h * 5 + h2;

       h *= ((int)Kind + 1);

       return h;

     }

@@ -472,7 +487,7 @@ namespace Microsoft.Boogie {
       if (other == null) {

         return false;

       } else {

-        return this.Tr.ListEquals(other.Tr) && 

+        return this.Tr.SequenceEqual(other.Tr) && 

           (Next == null ? other.Next == null : object.Equals(Next, other.Next));

       }

     }

@@ -853,4 +868,4 @@ namespace Microsoft.Boogie {
     }

 

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 65554a1e..d61c9941 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -496,8 +496,6 @@ namespace Microsoft.Boogie {
     public int TrustPhasesUpto = -1;

     public int TrustPhasesDownto = int.MaxValue;

 

-    public bool UseParallelism = true;

-

     public enum VCVariety {

       Structured,

       Block,

@@ -1431,7 +1429,6 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||

               ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||

               ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||

-              ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false) ||

               ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName)

               ) {

             // one of the boolean flags matched

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 1b8353e1..0a2e5a22 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -66,18 +66,6 @@ namespace Microsoft.Boogie {
     {

       return source1.Zip(source2, (e1, e2) => new Tuple<TSource1, TSource2>(e1, e2));

     }

-

-    public static bool ListEquals<A>(this List<A> xs, List<A> ys) {

-      var equal = xs.Count == ys.Count;

-      for (int i = 0; equal && i < xs.Count; i++) {

-        equal = object.Equals(xs[i], ys[i]);

-      }

-      return equal;

-    }

-

-    public static int ListHash<A>(this List<A> xs) {

-      return xs.Aggregate(xs.Count, (current, x) => current ^ xs.GetHashCode());

-    }

   }

 

   public class TokenTextWriter : IDisposable {

@@ -264,6 +252,11 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public TokenTextWriter(string filename)

+        : this(filename, false)

+    {

+    }

+

     public TokenTextWriter(string filename, bool pretty)

       : base() {

       Contract.Requires(filename != null);

@@ -300,6 +293,11 @@ namespace Microsoft.Boogie {
       this.writer = writer;

     }

 

+    public TokenTextWriter(TextWriter writer)

+        : this(writer, false)

+    {

+    }

+

     public TokenTextWriter(TextWriter writer, bool pretty)

       : base() {

       Contract.Requires(writer != null);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index a568176b..05c4b44b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -417,10 +417,9 @@ namespace Microsoft.Boogie
     

     static List<Checker> Checkers = new List<Checker>();

 

-    static IDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

-

-    static IDictionary<string, IList<CancellationTokenSource>> RequestIdToCancellationTokenSources = new ConcurrentDictionary<string, IList<CancellationTokenSource>>();

+    static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

 

+    static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

 

     public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)

     {

@@ -811,8 +810,6 @@ namespace Microsoft.Boogie
         requestId = FreshRequestId();

       }

 

-      RequestIdToCancellationTokenSources[requestId] = new List<CancellationTokenSource>();

-

       #region Do some pre-abstract-interpretation preprocessing on the program

       // Doing lambda expansion before abstract interpretation means that the abstract interpreter

       // never needs to see any lambda expressions.  (On the other hand, if it were useful for it

@@ -903,41 +900,67 @@ namespace Microsoft.Boogie
 

       try

       {

-          if (CommandLineOptions.Clo.UseParallelism)

+          var cts = new CancellationTokenSource();

+          RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);

+

+          var tasks = new Task[stablePrioritizedImpls.Length];

+          // We use this semaphore to limit the number of tasks that are currently executing.

+          var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores);

+

+          // Create a task per implementation.

+          for (int i = 0; i < stablePrioritizedImpls.Length; i++)

           {

-              var tasks = new Task[stablePrioritizedImpls.Length];

-              for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)

+              var taskIndex = i;

+              var id = stablePrioritizedImpls[taskIndex].Id;

+

+              CancellationTokenSource old;

+              if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))

               {

-                  var taskIndex = i;

-                  var id = stablePrioritizedImpls[i].Id;

-                  CancellationTokenSource src;

-                  if (ImplIdToCancellationTokenSource.TryGetValue(id, out src))

-                  {

-                      src.Cancel();

-                  }

-                  src = new CancellationTokenSource();

-                  RequestIdToCancellationTokenSources[requestId].Add(src);

-                  ImplIdToCancellationTokenSource[id] = src;

-                  var t = Task.Factory.StartNew((dummy) =>

+                  old.Cancel();

+              }

+              ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);

+

+              var t = new Task((dummy) =>

                   {

-                      if (src.Token.IsCancellationRequested)

+                      try

                       {

-                          src.Token.ThrowIfCancellationRequested();

+                          if (outcome == PipelineOutcome.FatalError)

+                          {

+                              return;

+                          }

+                          if (cts.Token.IsCancellationRequested)

+                          {

+                              cts.Token.ThrowIfCancellationRequested();

+                          }

+                          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId);

+                          ImplIdToCancellationTokenSource.TryRemove(id, out old);

                       }

-                      VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId);

-                      ImplIdToCancellationTokenSource.Remove(id);

-                  }, src.Token, TaskCreationOptions.LongRunning);

-                  tasks[taskIndex] = t;

-              }

-              Task.WaitAll(tasks);

+                      finally

+                      {

+                          semaphore.Release();

+                      }

+                  }, cts.Token, TaskCreationOptions.LongRunning);

+              tasks[taskIndex] = t;

           }

-          else

+

+          // Execute the tasks.

+          int j = 0;

+          for (; j < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; j++)

           {

-              for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)

+              try

               {

-                  VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, i, outputCollector, Checkers, programId);

+                  semaphore.Wait(cts.Token);

+              }

+              catch (OperationCanceledException)

+              {                  

+                  break;

               }

+              tasks[j].Start(TaskScheduler.Default);

           }

+

+          // Don't wait for tasks that haven't been started yet.

+          tasks = tasks.Take(j).ToArray();

+          Task.WaitAll(tasks);

       }

       catch (AggregateException ae)

       {

@@ -981,10 +1004,10 @@ namespace Microsoft.Boogie
     {

       Contract.Requires(requestId != null);

 

-      IList<CancellationTokenSource> ctss;

-      if (RequestIdToCancellationTokenSources.TryGetValue(requestId, out ctss))

+      CancellationTokenSource cts;

+      if (RequestIdToCancellationTokenSource.TryGetValue(requestId, out cts))

       {

-        ctss.Iter(cts => cts.Cancel());

+        cts.Cancel();

 

         CleanupCheckers(requestId);

       }

@@ -993,9 +1016,14 @@ namespace Microsoft.Boogie
 

     private static void CleanupCheckers(string requestId)

     {

-      lock (RequestIdToCancellationTokenSources)

+      if (requestId != null)

+      {

+        CancellationTokenSource old;

+        RequestIdToCancellationTokenSource.TryRemove(requestId, out old);

+      }

+      lock (RequestIdToCancellationTokenSource)

       {

-        if (RequestIdToCancellationTokenSources.Count == 1)

+        if (RequestIdToCancellationTokenSource.IsEmpty)

         {

           lock (Checkers)

           {

@@ -1006,10 +1034,6 @@ namespace Microsoft.Boogie
             }

           }

         }

-        if (requestId != null)

-        {

-          RequestIdToCancellationTokenSources.Remove(requestId);

-        }

       }

     }

 

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 6ffaef22..30056d99 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -385,6 +385,9 @@ namespace Microsoft.Boogie.Houdini {
                 break;

 

             unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString()));

+            var reason1 = new HashSet<string>(); //these are the reasons for inconsistency

+            unsatisfiedSoftAssumptions2.Iter(i => reason1.Add(softAssumptions2[i].ToString()));

+

             if (CommandLineOptions.Clo.Trace)

             {

                 Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name);

@@ -395,6 +398,11 @@ namespace Microsoft.Boogie.Houdini {
             {

                 Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName);

             }

+            //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0)

+            foreach (var r in reason1)

+            {

+                Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];", refutedConstant.Name, r, descriptiveName);

+            }

         } while (false);

 

         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 22127c5a..d88d4667 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -120,12 +120,15 @@ namespace VC {
     public Block block;

     public int numInstr;  // for TraceLocation

     public VCExprVar callSiteVar;

-    public CallSite(string callee, List<VCExpr> interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr) {

+    public QKeyValue Attributes; // attributes on the call cmd

+    public CallSite(string callee, List<VCExpr> interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr, QKeyValue Attributes)

+    {

       this.calleeName = callee;

       this.interfaceExprs = interfaceExprs;

       this.callSiteVar = callSiteVar;

       this.block = block;

       this.numInstr = numInstr;

+      this.Attributes = Attributes;

     }

   }

 

@@ -401,7 +404,7 @@ namespace VC {
           i++;

           AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i];

           IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr;

-          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr);

+          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, callSiteAssumeCmd.Attributes);

           if (!callSites.ContainsKey(block))

             callSites[block] = new List<CallSite>();

           callSites[block].Add(cs);

@@ -423,7 +426,7 @@ namespace VC {
           foreach (Expr e in naryExpr.Args) {

             interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));

           }

-          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, null, block, i);

+          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, null, block, i, assumeCmd.Attributes);

           if (!callSites.ContainsKey(block))

             callSites[block] = new List<CallSite>();

           callSites[block].Add(cs);

@@ -506,7 +509,7 @@ namespace VC {
 

   public class StratifiedVCGen : StratifiedVCGenBase {

     public bool PersistCallTree;

-    public static Dictionary<string, int> callTree = null;

+    public static HashSet<string> callTree = null;

     public int numInlined = 0;

     public int vcsize = 0;

     private bool useSummary;

@@ -515,7 +518,7 @@ namespace VC {
     public HashSet<string> procsToSkip;

     public Dictionary<string, int> extraRecBound;

 

-    public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree, 

+    public StratifiedVCGen(bool usePrevCallTree, HashSet<string> prevCallTree, 

                            HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,

                            Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) 

     : this(program, logFilePath, appendLogFile, checkers)

@@ -1103,7 +1106,7 @@ namespace VC {
         while (expand) {

           List<int> toExpand = new List<int>();

           foreach (int id in calls.currCandidates) {

-            if (callTree.ContainsKey(calls.getPersistentId(id))) {

+            if (callTree.Contains(calls.getPersistentId(id))) {

               toExpand.Add(id);

             }

           }

@@ -1281,14 +1284,16 @@ namespace VC {
 

       // Store current call tree

       if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound)) {

-        callTree = new Dictionary<string, int>();

+        callTree = new HashSet<string>();

         //var persistentNodes = new HashSet<int>(calls.candidateParent.Values);

         var persistentNodes = new HashSet<int>(calls.candidateParent.Keys);

         persistentNodes.Add(0);

         persistentNodes.ExceptWith(calls.currCandidates);

 

         foreach (var id in persistentNodes) {

-          callTree.Add(calls.getPersistentId(id), 0);

+          var pid = calls.getPersistentId(id);

+          Debug.Assert(!callTree.Contains(pid));

+          callTree.Add(pid);

         }

       }

       if (prover2 != null) prover2.Close();

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index eadf81e3..be519470 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,86 +15,123 @@ function map(lmap): [int]int;
 function cons([int]bool, [int]int) : lmap;

 axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);

 

-var {:phase 2} {:linear "mem"} g: lmap;

+var {:phase 3} {:linear "mem"} g: lmap;

+var {:phase 3} lock: X;

+var {:phase 1} b: bool;

 

 const p: int;

 

-procedure {:yields} {:phase 1,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

-ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+procedure {:yields} {:phase 1} Yield1()

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

+{

+    yield;

+    assert {:phase 1} InvLock(lock, b);

+}

 

-procedure {:yields} {:phase 1,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

-ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+function {:inline} InvLock(lock: X, b: bool) : bool

+{

+    lock != nil <==> b

+}

 

-procedure {:yields} {:phase 1} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

-ensures {:both} |{ A: v := map(l)[a]; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} {:phase 2} Yield2()

+{

+    yield;

+}

 

-procedure {:yields} {:phase 1} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

-ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} {:phase 3} Yield3()

+requires {:phase 3} Inv(g);

+ensures {:phase 3} Inv(g);

+{

+    yield;

+    assert {:phase 3} Inv(g);

+}

 

-procedure {:yields} {:phase 2} P({:linear "tid"} tid: X)

-requires {:phase 1} InvLock(lock, b);

+function {:inline} Inv(g: lmap) : bool

+{

+    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

+}

+

+procedure {:yields} {:phase 3} P({:linear "tid"} tid: X)

+requires {:phase 1} tid != nil && InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-requires {:phase 2} tid != nil && Inv(g);

-ensures {:phase 2} Inv(g);

+requires {:phase 3} tid != nil && Inv(g);

+ensures {:phase 3} Inv(g);

 {

     var t: int;

     var {:linear "mem"} l: lmap;

 

-    par Yield() | YieldLock();

-    call Acquire(tid);

-    call l := TransferFromGlobal(tid);

+    par Yield3() | Yield1();

+    call AcquireProtected(tid);

+    call l := TransferFromGlobalProtected(tid);

     call t := Load(l, p);

     call l := Store(l, p, t+1);

     call t := Load(l, p+4);

     call l := Store(l, p+4, t+1);

-    call TransferToGlobal(tid, l);

-    call Release(tid);

-    par Yield() | YieldLock();

+    call TransferToGlobalProtected(tid, l);

+    call ReleaseProtected(tid);

+    par Yield3() | Yield1();

 }

 

-procedure {:yields} {:phase 2} Yield()

-requires {:phase 2} Inv(g);

-ensures {:phase 2} Inv(g);

+

+procedure {:yields} {:phase 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

+ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

 {

-    yield;

-    assert {:phase 2} Inv(g);

+  par Yield1() | Yield2();

+  call TransferToGlobal(tid, l);

+  par Yield1() | Yield2();

 }

 

-function {:inline} Inv(g: lmap) : bool

+procedure {:yields} {:phase 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

+ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

 {

-    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

+  par Yield1() | Yield2();

+  call l := TransferFromGlobal(tid);

+  par Yield1() | Yield2();

 }

 

+procedure {:yields} {:phase 2,3} AcquireProtected({:linear "tid"} tid: X)

+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+requires {:phase 1} tid != nil && InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+  par Yield1() | Yield2();

+  call Acquire(tid);

+  par Yield1() | Yield2();

+}

 

-var {:phase 1} b: bool;

-var {:phase 2} lock: X;

+procedure {:yields} {:phase 2,3} ReleaseProtected({:linear "tid"} tid: X)

+ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+  par Yield1() | Yield2();

+  call Release(tid);

+  par Yield1() | Yield2();

+}

 

 procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)

-requires {:phase 1} InvLock(lock, b);

+requires {:phase 1} tid != nil && InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

     var tmp: X;

 

-    par YieldLock();

+    par Yield1();

     L: 

 	assert {:phase 1} InvLock(lock, b);

         call status := CAS(tid, false, true);

-	par YieldLock();

+	par Yield1();

         goto A, B;

 

     A: 

         assume status;

-	par YieldLock();	

+	par Yield1();	

 	return;

 

     B:

@@ -103,15 +140,27 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
 }

 

 procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)

-ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

+ensures {:atomic} |{ A: lock := nil; return true; }|;

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

 {

-    par YieldLock();

+    par Yield1();

     call CLEAR(tid, false);

-    par YieldLock();

+    par Yield1();

 }

 

+procedure {:yields} {:phase 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

+ensures {:atomic} |{ A: g := l; return true; }|;

+

+procedure {:yields} {:phase 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

+ensures {:atomic} |{ A: l := g; return true; }|;

+

+procedure {:yields} {:phase 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

+ensures {:both} |{ A: v := map(l)[a]; return true; }|;

+

+procedure {:yields} {:phase 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

+ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

+

 procedure {:yields} {:phase 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

 ensures {:atomic} |{ 

 A: goto B, C; 

@@ -124,15 +173,3 @@ ensures {:atomic} |{
 A: b := next; lock := nil; return true; 

 }|;

 

-procedure {:yields} {:phase 1} YieldLock()

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

-{

-    yield;

-    assert {:phase 1} InvLock(lock, b);

-}

-

-function {:inline} InvLock(lock: X, b: bool) : bool

-{

-    lock != nil <==> b

-}

diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect
index ac38b46e..4bcd03fb 100644
--- a/Test/og/civl-paper.bpl.expect
+++ b/Test/og/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 23 verified, 0 errors

+Boogie program verifier finished with 35 verified, 0 errors

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 8ee661c6..a522f304 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,92 +20,85 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

-procedure {:yields} {:phase 0} acquire(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tid: X);

 ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

-                      assert tidIn != nil && tidIn != done;

+                      assert tid != nil && tid != done;

                       assume lock[i] == nil;

-                      tidOut := tidIn;

-	              lock[i] := tidOut;

+	              lock[i] := tid;

                       return true;

                     }|;

 

 

-procedure {:yields} {:phase 0} release(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

-                     assert lock[i] == tidIn;

-                     assert tidIn != nil && tidIn != done; 

-                     tidOut := tidIn;

+                     assert lock[i] == tid;

+                     assert tid != nil && tid != done; 

 	             lock[i] := nil;

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0,1} getElt(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

+procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

 	             elt_j := elt[j];

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

 	             elt[j] := x;

-                     owner[j] := tidIn;

+                     owner[j] := tid;

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

-                     assert owner[j] == tidIn;

+                     assert owner[j] == tid;

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

+                     assert lock[j] == tid;

                      assert !valid[j];

-                     assert tidIn != nil  && tidIn != done;

-                     tidOut := tidIn;

+                     assert tid != nil  && tid != done;

 	             elt[j] := null;

                      owner[j] := nil;

                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} setValid(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     assert owner[j] == tidIn;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

+                     assert owner[j] == tid;

 	             valid[j] := true;

                      owner[j] := done;

                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);

+procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

 ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

-                       assert lock[j] == tidIn;

-                       assert tidIn != nil && tidIn != done;

-                       tidOut := tidIn;

+                       assert lock[j] == tid;

+                       assert tid != nil && tid != done;

                        fnd := (elt[j] == x) && valid[j];

                        return true;

                     }|;

 

-procedure {:yields} {:phase 1} FindSlot(x : int, {:linear_in "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)

-requires {:phase 1} Inv(valid, elt, owner);

+procedure {:yields} {:phase 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-ensures {:right}  |{ A: assert tidIn != nil && tidIn != done; 

+ensures {:right}  |{   A: assert tid != nil && tid != done; 

                           assert x != null; 

 			  goto B, C;

                        B: assume (0 <= r && r < max); 

@@ -113,112 +106,91 @@ ensures {:right}  |{ A: assert tidIn != nil && tidIn != done;
                                             assume owner[r] == nil;

 					    assume !valid[r];

                                             elt[r] := x; 

-                                            owner[r] := tidIn;

-                                            tidOut := tidIn; 

+                                            owner[r] := tid;

                                             return true;

-                       C: assume (r == -1); tidOut := tidIn; return true; 

+                       C: assume (r == -1); return true; 

                    }|;

 {

 	var j : int;

 	var elt_j : int;

-        var {:linear "tid"} tidTmp: X;

         

         par Yield1();

 

 	j := 0;

-        tidTmp := tidIn;

-

-	

 	while(j < max)

-        invariant {:phase 1} tidTmp != nil && tidTmp != done;

-        invariant {:phase 1} tidTmp == tidIn;

         invariant {:phase 1} Inv(valid, elt, owner);

 	invariant {:phase 1} 0 <= j;

 	{

-                call tidTmp := acquire(j, tidTmp);

-                call tidTmp, elt_j := getElt(j, tidTmp);

+                call acquire(j, tid);

+                call elt_j := getElt(j, tid);

 		if(elt_j == null)

 		{

-                        call tidTmp := setElt(j, x, tidTmp);

-			call tidTmp := release(j, tidTmp);

+                        call setElt(j, x, tid);

+			call release(j, tid);

 			r := j;

-                        tidOut := tidTmp;

 

                         par Yield1();

 			return;		

 		}

-		call tidTmp := release(j,tidTmp);

+		call release(j,tid);

 

                 par Yield1();

 

 		j := j + 1;	

 	}

 	r := -1;

-        tidOut := tidTmp;

 

         par Yield1();

 	return;

 }

 

-procedure {:yields} {:phase 2} Insert(x : int, {:linear_in "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X) 

-requires {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

+ensures {:phase 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var r:int;

-                        A: assert tidIn != nil && tidIn != done; 

-                           assert x != null;

-                           goto B, C;

+                        A: goto B, C;

                         B: assume (0 <= r && r < max); 

                            assume valid[r] == false; 

                            assume elt[r] == null; 

                            assume owner[r] == nil; 

                            elt[r] := x; valid[r] := true; owner[r] := done;

-                           tidOut := tidIn; result := true; return true;

-                        C: tidOut := tidIn; result := false; return true; 

+                           result := true; return true;

+                        C: result := false; return true; 

                       }|;

  {

         var i: int;

-        var {:linear "tid"} tidTmp: X;

         par Yield12();

-        tidTmp := tidIn;

-        call i, tidTmp := FindSlot(x, tidTmp);

+        call i := FindSlot(x, tid);

         

 	if(i == -1)

 	{

 		result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

         par Yield1();

         assert {:phase 1} i != -1;

         assert {:phase 2} i != -1;

-	call tidTmp := acquire(i, tidTmp);

+	call acquire(i, tid);

         assert {:phase 2} elt[i] == x;

 	assert {:phase 2}  valid[i] == false;

-        call tidTmp := setValid(i, tidTmp);   

-	call tidTmp := release(i, tidTmp);

+        call setValid(i, tid);   

+	call release(i, tid);

 	result := true; 

-        tidOut := tidTmp;

         par Yield12();

 	return;

 }

 

-procedure {:yields} {:phase 2} InsertPair(x : int, 

-                               y : int, 

-                               {:linear_in "tid"} tidIn: X) 

-                               returns (result : bool, 

-                                        {:linear "tid"} tidOut: X) 

-requires {:phase 1} Inv(valid, elt, owner);

+procedure {:yields} {:phase 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

+requires {:phase 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

 ensures {:phase 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var rx:int;

                         var ry:int;

-                        A: assert tidIn != nil && tidIn != done; 

-                           assert x != null && y != null;

-                           goto B, C;

+                        A: goto B, C;

                         B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); 

                            assume valid[rx] == false; 

                            assume valid[ry] == false; 

@@ -230,68 +202,60 @@ ensures {:atomic}  |{ var rx:int;
                            valid[ry] := true;

                            owner[rx] := done;

                            owner[ry] := done; 

-                           tidOut := tidIn; 

                            result := true; return true;

-                        C: tidOut := tidIn; 

-                           result := false; return true; 

+                        C: result := false; return true; 

                       }|;

  {

         var i : int; 

         var j : int;

-        var {:linear "tid"} tidTmp: X;

         par Yield12();

 

-        tidTmp := tidIn;

-

-        call i, tidTmp := FindSlot(x, tidTmp);

+        call i := FindSlot(x, tid);

         

 	if (i == -1)

 	{

 	 	result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

 

         par Yield1();

-        call j, tidTmp := FindSlot(y, tidTmp);

+        call j := FindSlot(y, tid);

         

 	if(j == -1)

 	{

                 par Yield1();

-                call tidTmp := acquire(i,tidTmp);  

-                call tidTmp := setEltToNull(i, tidTmp);

-                call tidTmp := release(i,tidTmp);  

+                call acquire(i,tid);  

+                call setEltToNull(i, tid);

+                call release(i,tid);  

 		result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

 

         par Yield1();

         assert {:phase 2} i != -1 && j != -1;

-	call tidTmp := acquire(i, tidTmp);

-	call tidTmp := acquire(j, tidTmp);

+	call acquire(i, tid);

+	call acquire(j, tid);

         assert {:phase 2} elt[i] == x;

         assert {:phase 2} elt[j] == y;

 	assert {:phase 2}  valid[i] == false;

 	assert {:phase 2}  valid[j] == false;

-        call tidTmp := setValid(i, tidTmp);   

-        call tidTmp := setValid(j, tidTmp);   

-	call tidTmp := release(j, tidTmp);

-	call tidTmp := release(i, tidTmp);

+        call setValid(i, tid);   

+        call setValid(j, tid);   

+	call release(j, tid);

+	call release(i, tid);

 	result := true; 

-        tidOut := tidTmp;

         par Yield12();

 	return;

 }

 

-procedure {:yields} {:phase 2} LookUp(x : int, {:linear_in "tid"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)

+procedure {:yields} {:phase 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

 requires {:phase 1} {:phase 2} old_valid == valid && old_elt == elt;

 requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

-requires {:phase 1} {:phase 2} (tidIn != nil && tidIn != done);

+requires {:phase 1} {:phase 2} (tid != nil && tid != done);

 ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done; 

+ensures {:atomic}  |{ A: assert tid != nil && tid != done; 

                           assert x != null;

                           assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);

 			  assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));

@@ -300,37 +264,31 @@ ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done;
 {

 	var j : int;

 	var isThere : bool;

-        var {:linear "tid"} tidTmp: X;

         

         par Yield12() | YieldLookUp(old_valid, old_elt);

 

 	j := 0;

-        tidTmp := tidIn;

 

 	while(j < max)

-        invariant {:phase 1} {:phase 2} tidTmp != nil && tidTmp != done;

-        invariant {:phase 1} {:phase 2} tidTmp == tidIn;

         invariant {:phase 1} {:phase 2} Inv(valid, elt, owner);

         invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

 	invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 	invariant {:phase 1} {:phase 2} 0 <= j;

 	{

-                call tidTmp := acquire(j, tidTmp);

-                call tidTmp, isThere := isEltThereAndValid(j, x, tidTmp);

+                call acquire(j, tid);

+                call isThere := isEltThereAndValid(j, x, tid);

 		if(isThere)

 		{

-			 call tidTmp := release(j, tidTmp);

+			 call release(j, tid);

                          found := true; 

-                         tidOut := tidTmp;

                          par Yield12() | YieldLookUp(old_valid, old_elt);

 		 	 return;		

 		}

-		call tidTmp := release(j,tidTmp);

+		call release(j,tid);

                 par Yield12() | YieldLookUp(old_valid, old_elt);

 		j := j + 1;	

 	}

 	found := false;

-        tidOut := tidTmp;

 

         par Yield12() | YieldLookUp(old_valid, old_elt);

 	return;

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 552a4007..9c1b7c9a 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 3} t: int;

-var {:phase 3} s: int;

-var {:phase 3} cs: X;

-var {:phase 3} T: [int]bool;

+var {:phase 2} t: int;

+var {:phase 2} s: int;

+var {:phase 2} cs: X;

+var {:phase 2} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -36,17 +36,18 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} {:phase 2} xl != nil;

 

-procedure {:yields} {:phase 3} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 3} xls' == mapconstbool(true);

+procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)

+requires {:phase 2} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

 

     yield;

 

-    call xls := Init(xls');

+    call Init(xls');

+    xls := xls';

 

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 

     while (*)

     invariant {:phase 1} Inv1(T, t);

@@ -54,63 +55,59 @@ requires {:phase 3} xls' == mapconstbool(true);
     {

         call xls, tid := Allocate(xls);

         async call Customer(tid);

-    	par Yield1() | Yield2() | Yield();

+    	par Yield1() | Yield2();

     }

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 3} Customer({:linear_in "tid"} tid': X)

+procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)

 requires {:phase 1} Inv1(T, t);

-requires {:phase 2} tid' != nil && Inv2(T, s, cs);

-requires {:phase 3} true;

+requires {:phase 2} tid != nil && Inv2(T, s, cs);

 {

-    var {:linear "tid"} tid: X;

-    tid := tid';

-    

-    par Yield1() | Yield2() | Yield();    

+    par Yield1() | Yield2();    

     while (*) 

     invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} tid != nil && Inv2(T, s, cs);

+    invariant {:phase 2} Inv2(T, s, cs);

     {

-        call tid := Enter(tid);

+        call Enter(tid);

+        par Yield1() | Yield2() | YieldSpec(tid);

+    	call Leave(tid);

         par Yield1() | Yield2();

-    	call tid := Leave(tid);

-        par Yield1() | Yield2() | Yield();

     }

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2,3} Enter({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

-requires {:phase 2} tid' != nil && Inv2(T, s, cs);

-ensures {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

+requires {:phase 2} tid != nil && Inv2(T, s, cs);

+ensures {:phase 2} Inv2(T, s, cs) && cs == tid;

 {

     var m: int;

 

     par Yield1() | Yield2();

-    tid := tid';

-    call tid, m := GetTicketAbstract(tid);

+    call m := GetTicketAbstract(tid);

     par Yield1();

-    call tid := WaitAndEnter(tid, m);

-    par Yield1() | Yield2();

+    call WaitAndEnter(tid, m);

+    par Yield1() | Yield2() | YieldSpec(tid);

 }

 

-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

+procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T, t);

-ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

+ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

-    tid := tid';

-    call tid, m := GetTicket(tid);

+    call m := GetTicket(tid);

     par Yield1();

 }

 

-procedure {:yields} {:phase 3} Yield()

+procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)

+requires {:phase 2} tid != nil && cs == tid;

+ensures {:phase 2} cs == tid;

 {

     yield;

+    assert {:phase 2} tid != nil && cs == tid;

 }

 

 procedure {:yields} {:phase 2} Yield2()

@@ -129,15 +126,15 @@ ensures {:phase 1} Inv1(T,t);
     assert {:phase 1} Inv1(T,t);

 }

 

-procedure {:yields} {:phase 0,3} Init({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

+procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);

+ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} {:phase 0,1} GetTicket({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

-ensures {:atomic} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

+procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

+ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear_in "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

+ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} {:phase 0,3} Leave({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;

+procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

 

diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
index bc10e4e3..f7c1129d 100644
--- a/Test/og/ticket.bpl.expect
+++ b/Test/og/ticket.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 21 verified, 0 errors

+Boogie program verifier finished with 14 verified, 0 errors