Merge

18 files changed, 414 insertions, 316 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 0911cbd3..44adce15 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -701,7 +701,7 @@ namespace Microsoft.Boogie {
               Console.WriteLine();

             }

             else {

-              outcome = vcgen.VerifyImplementation(impl, program, out errors);

+              outcome = vcgen.VerifyImplementation(impl, out errors);

               if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {

                 for (int i = 0; i < errors.Count; i++) {

                   errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4cf64788..3534dcbf 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -616,7 +616,7 @@ namespace Microsoft.Dafny
             int prevAssertionCount = vcgen.CumulativeAssertionCount;

             try

             {

-                outcome = vcgen.VerifyImplementation(impl, program, out errors);

+                outcome = vcgen.VerifyImplementation(impl, out errors);

             }

             catch (VCGenException e)

             {

diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
index b202dbb3..20036abe 100644
--- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs
+++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
@@ -117,27 +117,28 @@ namespace GPUVerify
                 if (c is AssignCmd)

                 {

                     AssignCmd assignCmd = c as AssignCmd;

-                    Debug.Assert(assignCmd.Lhss.Count == 1);

-                    Debug.Assert(assignCmd.Rhss.Count == 1);

-                    if (assignCmd.Lhss[0] is SimpleAssignLhs)

+                    for (int i = 0; i != assignCmd.Lhss.Count; i++)

                     {

-                        SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

-                        Expr rhs = assignCmd.Rhss[0];

+                        if (assignCmd.Lhss[i] is SimpleAssignLhs)

+                        {

+                            SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

+                            Expr rhs = assignCmd.Rhss[i];

 

-                        VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();

-                        visitor.VisitExpr(rhs);

+                            VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();

+                            visitor.VisitExpr(rhs);

 

-                        foreach (Variable v in visitor.GetVariables())

-                        {

-                            if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))

-                            {

-                                continue;

-                            }

-                            foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])

+                            foreach (Variable v in visitor.GetVariables())

                             {

-                                if (!mayBeDerivedFrom[impl.Name][lhs.AssignedVariable.Name].Contains(s))

+                                if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))

                                 {

-                                    SetMayBeDerivedFrom(impl.Name, lhs.AssignedVariable.Name, s);

+                                    continue;

+                                }

+                                foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])

+                                {

+                                    if (!mayBeDerivedFrom[impl.Name][lhs.AssignedVariable.Name].Contains(s))

+                                    {

+                                        SetMayBeDerivedFrom(impl.Name, lhs.AssignedVariable.Name, s);

+                                    }

                                 }

                             }

                         }

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
index 15ad2432..80d97ebc 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -1,3 +1,4 @@
+using Graphing;
 using Microsoft.Boogie;
 using System;
 using System.Collections.Generic;
@@ -10,6 +11,7 @@ class BlockPredicator {
 
   Program prog;
   Implementation impl;
+  Graph<Block> blockGraph;
 
   Expr returnBlockId;
 
@@ -19,6 +21,7 @@ class BlockPredicator {
   Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
     new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
   Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+  HashSet<Block> doneBlocks = new HashSet<Block>();
 
   BlockPredicator(Program p, Implementation i) {
     prog = p;
@@ -95,6 +98,23 @@ class BlockPredicator {
         PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
                targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
       }
+
+      foreach (Block b in gCmd.labelTargets) {
+        if (blockGraph.Predecessors(b).Count() == 1) {
+          if (!doneBlocks.Contains(b)) {
+            var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd);
+            if (assumes.Count() > 0) {
+              foreach (AssumeCmd aCmd in assumes) {
+                cmdSeq.Add(new AssumeCmd(Token.NoToken,
+                                         Expr.Imp(Expr.Eq(cur, blockIds[b]),
+                                         aCmd.Expr)));
+              }
+              b.Cmds =
+                new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
+            }
+          }
+        }
+      }
     } else if (cmd is ReturnCmd) {
       PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
     } else {
@@ -103,8 +123,8 @@ class BlockPredicator {
   }
 
   void PredicateImplementation() {
-    var g = prog.ProcessLoops(impl);
-    var sortedBlocks = g.LoopyTopSort();
+    blockGraph = prog.ProcessLoops(impl);
+    var sortedBlocks = blockGraph.LoopyTopSort();
 
     int blockId = 0;
     foreach (var block in impl.Blocks)
@@ -163,6 +183,7 @@ class BlockPredicator {
         prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
                                             new BlockSeq(runBlock));
         prevBlock = runBlock;
+        doneBlocks.Add(runBlock);
       }
     }
 
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 6659566b..27ec052e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1374,7 +1374,8 @@ namespace GPUVerify
             IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));

             IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));

 

-            checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));

+            if (!CommandLineOptions.Unstructured)

+                checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));

 

             if (!CommandLineOptions.OnlyDivergence)

             {

@@ -1520,8 +1521,10 @@ namespace GPUVerify
 

             impl.LocVars = NewLocVars;

 

-            impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);

-

+            if (CommandLineOptions.Unstructured)

+                impl.Blocks = impl.Blocks.Select(PerformFullSharedStateAbstraction).ToList();

+            else

+                impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);

         }

 

 

@@ -1538,50 +1541,78 @@ namespace GPUVerify
             return result;

         }

 

-        private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)

+        private CmdSeq PerformFullSharedStateAbstraction(CmdSeq cs)

         {

-            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

+            var result = new CmdSeq();

 

-            foreach (Cmd c in bb.simpleCmds)

+            foreach (Cmd c in cs)

             {

                 if (c is AssignCmd)

                 {

                     AssignCmd assign = c as AssignCmd;

-                    Debug.Assert(assign.Lhss.Count == 1);

-                    Debug.Assert(assign.Rhss.Count == 1);

-                    AssignLhs lhs = assign.Lhss[0];

-                    Expr rhs = assign.Rhss[0];

-                    ReadCollector rc = new ReadCollector(NonLocalState);

-                    rc.Visit(rhs);

-

-                    bool foundAdversarial = false;

-                    foreach (AccessRecord ar in rc.accesses)

+

+                    var lhss = new List<AssignLhs>(); 

+                    var rhss = new List<Expr>(); 

+

+                    for (int i = 0; i != assign.Lhss.Count; i++)

                     {

-                        if (ArrayModelledAdversarially(ar.v))

+                        AssignLhs lhs = assign.Lhss[i];

+                        Expr rhs = assign.Rhss[i];

+                        ReadCollector rc = new ReadCollector(NonLocalState);

+                        rc.Visit(rhs);

+

+                        bool foundAdversarial = false;

+                        foreach (AccessRecord ar in rc.accesses)

                         {

-                            foundAdversarial = true;

-                            break;

+                            if (ArrayModelledAdversarially(ar.v))

+                            {

+                                foundAdversarial = true;

+                                break;

+                            }

                         }

-                    }

 

-                    if (foundAdversarial)

-                    {

-                        Debug.Assert(lhs is SimpleAssignLhs);

-                        result.simpleCmds.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));

-                        continue;

+                        if (foundAdversarial)

+                        {

+                            Debug.Assert(lhs is SimpleAssignLhs);

+                            result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));

+                            continue;

+                        }

+

+                        WriteCollector wc = new WriteCollector(NonLocalState);

+                        wc.Visit(lhs);

+                        if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))

+                        {

+                            continue; // Just remove the write

+                        }

+

+                        lhss.Add(lhs);

+                        rhss.Add(rhs);

                     }

 

-                    WriteCollector wc = new WriteCollector(NonLocalState);

-                    wc.Visit(lhs);

-                    if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))

+                    if (lhss.Count != 0)

                     {

-                        continue; // Just remove the write

+                        result.Add(new AssignCmd(assign.tok, lhss, rhss));

                     }

-

+                    continue;

                 }

-                result.simpleCmds.Add(c);

+                result.Add(c);

             }

 

+            return result;

+        }

+

+        private Block PerformFullSharedStateAbstraction(Block b)

+        {

+            b.Cmds = PerformFullSharedStateAbstraction(b.Cmds);

+            return b;

+        }

+

+        private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)

+        {

+            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

+

+            result.simpleCmds = PerformFullSharedStateAbstraction(bb.simpleCmds);

+

             if (bb.ec is WhileCmd)

             {

                 WhileCmd WhileCommand = bb.ec as WhileCmd;

@@ -1874,19 +1905,18 @@ namespace GPUVerify
                 {

                     AssignCmd assign = c as AssignCmd;

 

-                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

-

-                    AssignLhs lhs = assign.Lhss.ElementAt(0);

-                    Expr rhs = assign.Rhss.ElementAt(0);

-

-                    if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) || 

-                        (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) && 

-                          NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))

+                    if (assign.Lhss.Zip(assign.Rhss, (lhs, rhs) =>

+                            !NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) || 

+                              (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) && 

+                                NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState))).All(b => b))

                     {

                         result.simpleCmds.Add(c);

                     }

                     else

                     {

+                        Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

+                        AssignLhs lhs = assign.Lhss.ElementAt(0);

+                        Expr rhs = assign.Rhss.ElementAt(0);

                         rhs = PullOutNonLocalAccessesIntoTemps(result, rhs, impl);

                         List<AssignLhs> newLhss = new List<AssignLhs>();

                         newLhss.Add(lhs);

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 8d51e74e..49b04251 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -147,23 +147,22 @@ namespace GPUVerify
             {

                 AssignCmd assign = c as AssignCmd;

 

-                Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

-

-                if (assign.Lhss[0] is SimpleAssignLhs &&

-                    verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))

+                if (assign.Lhss.All(lhs =>

+                        lhs is SimpleAssignLhs &&

+                        verifier.uniformityAnalyser.IsUniform(procName, (lhs as SimpleAssignLhs).AssignedVariable.Name)))

                 {

                     cs.Add(assign);

                 }

                 else

                 {

-                    List<AssignLhs> newLhss = new List<AssignLhs>();

-                    List<Expr> newRhss = new List<Expr>();

-

-                    newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-                    newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-

-                    newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

-                    newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+                    List<AssignLhs> newLhss = assign.Lhss.SelectMany(lhs => new AssignLhs[] {

+                        new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(lhs.Clone() as AssignLhs) as AssignLhs,

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(lhs.Clone() as AssignLhs) as AssignLhs

+                    }).ToList();

+                    List<Expr> newRhss = assign.Rhss.SelectMany(rhs => new Expr[] {

+                        new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(rhs.Clone() as Expr),

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(rhs.Clone() as Expr)

+                    }).ToList();

 

                     AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

 

diff --git a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs
index 88ac000f..3d65ec61 100644
--- a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs
+++ b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs
@@ -186,19 +186,19 @@ namespace GPUVerify
 

         private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

         {

-            Debug.Assert(assignCmd.Lhss.Count == 1);

-            Debug.Assert(assignCmd.Rhss.Count == 1);

-            if (assignCmd.Lhss[0] is SimpleAssignLhs)

+            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

             {

-                SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

-                Expr rhs = assignCmd.Rhss[0];

-

-                if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                    && !MayBe(component, impl.Name, rhs))

+                if (assignCmd.Lhss[i] is SimpleAssignLhs)

                 {

-                    SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                }

+                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

+                    Expr rhs = assignCmd.Rhss[i];

 

+                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

+                        && !MayBe(component, impl.Name, rhs))

+                    {

+                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

+                    }

+                }

             }

         }

 

diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs
index bb0f8d22..969e8935 100644
--- a/Source/GPUVerify/MayBeGidAnalyser.cs
+++ b/Source/GPUVerify/MayBeGidAnalyser.cs
@@ -186,19 +186,19 @@ namespace GPUVerify
 

         private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

         {

-            Debug.Assert(assignCmd.Lhss.Count == 1);

-            Debug.Assert(assignCmd.Rhss.Count == 1);

-            if (assignCmd.Lhss[0] is SimpleAssignLhs)

+            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

             {

-                SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

-                Expr rhs = assignCmd.Rhss[0];

-

-                if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                    && !MayBe(component, impl.Name, rhs))

+                if (assignCmd.Lhss[i] is SimpleAssignLhs)

                 {

-                    SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                }

+                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

+                    Expr rhs = assignCmd.Rhss[i];

 

+                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

+                        && !MayBe(component, impl.Name, rhs))

+                    {

+                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

+                    }

+                }

             }

         }

 

diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
index cd3c27d6..579f6805 100644
--- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
+++ b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
@@ -186,19 +186,19 @@ namespace GPUVerify
 

         private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

         {

-            Debug.Assert(assignCmd.Lhss.Count == 1);

-            Debug.Assert(assignCmd.Rhss.Count == 1);

-            if (assignCmd.Lhss[0] is SimpleAssignLhs)

+            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

             {

-                SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

-                Expr rhs = assignCmd.Rhss[0];

-

-                if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                    && !MayBe(component, impl.Name, rhs))

+                if (assignCmd.Lhss[i] is SimpleAssignLhs)

                 {

-                    SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                }

+                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

+                    Expr rhs = assignCmd.Rhss[i];

 

+                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

+                        && !MayBe(component, impl.Name, rhs))

+                    {

+                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

+                    }

+                }

             }

         }

 

diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
index 676213e6..a8563dfa 100644
--- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
+++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
@@ -98,38 +98,38 @@ namespace GPUVerify
                 if (c is AssignCmd)

                 {

                     AssignCmd assign = c as AssignCmd;

-                    assign = c as AssignCmd;

-                    Debug.Assert(assign.Lhss.Count == 1);

-                    Debug.Assert(assign.Rhss.Count == 1);

 

-                    if (assign.Lhss[0] is SimpleAssignLhs)

+                    for (int i = 0; i != assign.Lhss.Count; i++)

                     {

-                        Variable lhsV = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;

-

-                        if (mayBeAssignedId[impl.Name].ContainsKey(lhsV.Name))

+                        if (assign.Lhss[i] is SimpleAssignLhs)

                         {

+                            Variable lhsV = (assign.Lhss[i] as SimpleAssignLhs).AssignedVariable.Decl;

 

-                            if (assign.Rhss[0] is IdentifierExpr)

+                            if (mayBeAssignedId[impl.Name].ContainsKey(lhsV.Name))

                             {

 

-                                Variable rhsV = (assign.Rhss[0] as IdentifierExpr).Decl;

-

-                                if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))

+                                if (assign.Rhss[i] is IdentifierExpr)

                                 {

-                                    mayBeAssignedId[impl.Name][lhsV.Name] = true;

-                                }

 

-                            }

-                            else

-                            {

+                                    Variable rhsV = (assign.Rhss[i] as IdentifierExpr).Decl;

 

-                                Expr constantIncrement = GetConstantIncrement(lhsV, assign.Rhss[0]);

+                                    if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))

+                                    {

+                                        mayBeAssignedId[impl.Name][lhsV.Name] = true;

+                                    }

 

-                                if (constantIncrement != null)

-                                {

-                                    incrementedBy[impl.Name][lhsV.Name].Add(constantIncrement);

                                 }

+                                else

+                                {

+

+                                    Expr constantIncrement = GetConstantIncrement(lhsV, assign.Rhss[i]);

 

+                                    if (constantIncrement != null)

+                                    {

+                                        incrementedBy[impl.Name][lhsV.Name].Add(constantIncrement);

+                                    }

+

+                                }

                             }

                         }

                     }

diff --git a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs
index a00462c8..506add7c 100644
--- a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs
+++ b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs
@@ -85,18 +85,18 @@ namespace GPUVerify
                 if (c is AssignCmd)

                 {

                     AssignCmd assign = c as AssignCmd;

-                    assign = c as AssignCmd;

-                    Debug.Assert(assign.Lhss.Count == 1);

-                    Debug.Assert(assign.Rhss.Count == 1);

 

-                    if (assign.Lhss[0] is SimpleAssignLhs)

+                    for (int i = 0; i != assign.Lhss.Count; i++)

                     {

-                        Variable v = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;

-                        if (mayBePowerOfTwoInfo[impl.Name].ContainsKey(v.Name))

+                        if (assign.Lhss[i] is SimpleAssignLhs)

                         {

-                            if (isPowerOfTwoOperation(v, assign.Rhss[0]))

+                            Variable v = (assign.Lhss[i] as SimpleAssignLhs).AssignedVariable.Decl;

+                            if (mayBePowerOfTwoInfo[impl.Name].ContainsKey(v.Name))

                             {

-                                mayBePowerOfTwoInfo[impl.Name][v.Name] = true;

+                                if (isPowerOfTwoOperation(v, assign.Rhss[i]))

+                                {

+                                    mayBePowerOfTwoInfo[impl.Name][v.Name] = true;

+                                }

                             }

                         }

                     }

diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
index bca71171..53efbea8 100644
--- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
+++ b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
@@ -221,19 +221,19 @@ namespace GPUVerify
 

         private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

         {

-            Debug.Assert(assignCmd.Lhss.Count == 1);

-            Debug.Assert(assignCmd.Rhss.Count == 1);

-            if (assignCmd.Lhss[0] is SimpleAssignLhs)

+            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

             {

-                SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

-                Expr rhs = assignCmd.Rhss[0];

-

-                if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                    && !MayBe(component, impl.Name, rhs))

+                if (assignCmd.Lhss[i] is SimpleAssignLhs)

                 {

-                    SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                }

+                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

+                    Expr rhs = assignCmd.Rhss[i];

 

+                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

+                        && !MayBe(component, impl.Name, rhs))

+                    {

+                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

+                    }

+                }

             }

         }

 

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 11feb017..a0c4b5f7 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -800,7 +800,8 @@ namespace GPUVerify
 

         private Block AddRaceCheckCalls(Block b)

         {

-            return new Block(Token.NoToken, b.Label, AddRaceCheckCalls(b.Cmds), b.TransferCmd);

+            b.Cmds = AddRaceCheckCalls(b.Cmds);

+            return b;

         }

 

         private void AddRaceCheckCalls(Implementation impl)

@@ -845,79 +846,79 @@ namespace GPUVerify
                 if (c is AssignCmd)

                 {

                     AssignCmd assign = c as AssignCmd;

-                    Debug.Assert(assign.Lhss.Count == 1);

-                    Debug.Assert(assign.Rhss.Count == 1);

-                    AssignLhs lhs = assign.Lhss[0];

-                    Expr rhs = assign.Rhss[0];

 

                     ReadCollector rc = new ReadCollector(NonLocalStateToCheck);

-                    rc.Visit(rhs);

+                    foreach (var rhs in assign.Rhss)

+                        rc.Visit(rhs);

                     if (rc.accesses.Count > 0)

                     {

-                        Debug.Assert(rc.accesses.Count == 1);

-                        AccessRecord ar = rc.accesses[0];

-

-                        if (shouldAddLogCallAndIncr())

+                        foreach (AccessRecord ar in rc.accesses)

                         {

-

-                            ExprSeq inParams = new ExprSeq();

-                            if (ar.IndexZ != null)

+                            if (shouldAddLogCallAndIncr())

                             {

-                                inParams.Add(ar.IndexZ);

-                            }

-                            if (ar.IndexY != null)

-                            {

-                                inParams.Add(ar.IndexY);

-                            }

-                            if (ar.IndexX != null)

-                            {

-                                inParams.Add(ar.IndexX);

-                            }

 

-                            Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);

+                                ExprSeq inParams = new ExprSeq();

+                                if (ar.IndexZ != null)

+                                {

+                                    inParams.Add(ar.IndexZ);

+                                }

+                                if (ar.IndexY != null)

+                                {

+                                    inParams.Add(ar.IndexY);

+                                }

+                                if (ar.IndexX != null)

+                                {

+                                    inParams.Add(ar.IndexX);

+                                }

 

-                            CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

+                                Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);

 

-                            logAccessCallCmd.Proc = logProcedure;

+                                CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

 

-                            cs.Add(logAccessCallCmd);

+                                logAccessCallCmd.Proc = logProcedure;

 

+                                cs.Add(logAccessCallCmd);

+

+                            }

                         }

                     }

 

-                    WriteCollector wc = new WriteCollector(NonLocalStateToCheck);

-                    wc.Visit(lhs);

-                    if (wc.GetAccess() != null)

+                    foreach (var lhs in assign.Lhss)

                     {

-                        AccessRecord ar = wc.GetAccess();

-

-                        if (shouldAddLogCallAndIncr())

+                        WriteCollector wc = new WriteCollector(NonLocalStateToCheck);

+                        wc.Visit(lhs);

+                        if (wc.GetAccess() != null)

                         {

+                            AccessRecord ar = wc.GetAccess();

 

-                            ExprSeq inParams = new ExprSeq();

-                            if (ar.IndexZ != null)

-                            {

-                                inParams.Add(ar.IndexZ);

-                            }

-                            if (ar.IndexY != null)

-                            {

-                                inParams.Add(ar.IndexY);

-                            }

-                            if (ar.IndexX != null)

+                            if (shouldAddLogCallAndIncr())

                             {

-                                inParams.Add(ar.IndexX);

-                            }

 

-                            Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);

+                                ExprSeq inParams = new ExprSeq();

+                                if (ar.IndexZ != null)

+                                {

+                                    inParams.Add(ar.IndexZ);

+                                }

+                                if (ar.IndexY != null)

+                                {

+                                    inParams.Add(ar.IndexY);

+                                }

+                                if (ar.IndexX != null)

+                                {

+                                    inParams.Add(ar.IndexX);

+                                }

 

-                            CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

+                                Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);

 

-                            logAccessCallCmd.Proc = logProcedure;

+                                CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

 

-                            cs.Add(logAccessCallCmd);

+                                logAccessCallCmd.Proc = logProcedure;

 

-                            addedLogWrite = true;

+                                cs.Add(logAccessCallCmd);

 

+                                addedLogWrite = true;

+

+                            }

                         }

                     }

                 }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index dd898c36..ba58a5de 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -447,9 +447,8 @@ namespace VC {
   }

   [ContractClassFor(typeof(ConditionGeneration))]

   public abstract class ConditionGenerationContracts : ConditionGeneration {

-    public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {

+    public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {

       Contract.Requires(impl != null);

-      Contract.Requires(program != null);

       Contract.Requires(callback != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

@@ -522,9 +521,8 @@ namespace VC {
     /// each counterexample consisting of an array of labels.

     /// </summary>

     /// <param name="impl"></param>

-    public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {

+    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {

       Contract.Requires(impl != null);

-      Contract.Requires(program != null);

 

       Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

       Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);

@@ -532,7 +530,7 @@ namespace VC {
       Helpers.ExtraTraceInformation("Starting implementation verification");

 

       CounterexampleCollector collector = new CounterexampleCollector();

-      Outcome outcome = VerifyImplementation(impl, program, collector);

+      Outcome outcome = VerifyImplementation(impl, collector);

       if (outcome == Outcome.Errors) {

         errors = collector.examples;

       } else {

@@ -550,7 +548,7 @@ namespace VC {
     /// each counterexample consisting of an array of labels.

     /// </summary>

     /// <param name="impl"></param>

-    public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<Model> errorsModel)

+    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample> errors, out List<Model> errorsModel)

     {

         Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);

         Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

@@ -558,14 +556,14 @@ namespace VC {
 

         Outcome outcome;

         errorModelList = new List<Model>();

-        outcome = VerifyImplementation(impl, program, out errorsOut);

+        outcome = VerifyImplementation(impl, out errorsOut);

         errors = errorsOut;

         errorsModel = errorModelList;

 

         return outcome;

     }

 

-    public abstract Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback);

+    public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback);

 

     /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 65aa8486..563cbf40 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -21,15 +21,13 @@ namespace VC {
     public int id;

     public List<VCExprVar> interfaceExprVars;

     public Dictionary<Block, List<StratifiedCallSite>> callSites;

+    public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;

     public VCExpr vcexpr;

     public Dictionary<Block, VCExprVar> reachVars;

 

     public StratifiedVC(StratifiedInliningInfo siInfo) {

       info = siInfo;

-      if (!info.initialized) {

-        info.GenerateVC();

-      }

-

+      info.GenerateVC();

       vcexpr = info.vcexpr;

       var vcgen = info.vcgen;

       var prover = vcgen.prover;

@@ -84,6 +82,14 @@ namespace VC {
           callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

         }

       }

+

+      recordProcCallSites = new Dictionary<Block, List<StratifiedCallSite>>();

+      foreach (Block b in info.recordProcCallSites.Keys) {

+        recordProcCallSites[b] = new List<StratifiedCallSite>();

+        foreach (CallSite cs in info.recordProcCallSites[b]) {

+          recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

+        }

+      }

     }

 

     public List<StratifiedCallSite> CallSites {

@@ -150,6 +156,7 @@ namespace VC {
     public Hashtable/*<int, Absy!>*/ label2absy;

     public ModelViewInfo mvInfo;

     public Dictionary<Block, List<CallSite>> callSites;

+    public Dictionary<Block, List<CallSite>> recordProcCallSites;

     public bool initialized { get; private set; }

 

     public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {

@@ -232,9 +239,8 @@ namespace VC {
       var exprGen = proverInterface.Context.ExprGen;

       var translator = proverInterface.Context.BoogieExprTranslator;

       VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);

-

       vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));

-      if (!CommandLineOptions.Clo.UseLabels) {

+      if (controlFlowVariableExpr != null) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));

         VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

         vcexpr = exprGen.And(eqExpr, vcexpr);

@@ -260,6 +266,7 @@ namespace VC {
       }

 

       callSites = vcgen.CollectCallSites(impl);

+      recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);

       initialized = true;

     }

   }

@@ -303,7 +310,8 @@ namespace VC {
     }

   }

 

-  public class StratifiedVCGenBase : VCGen {

+  public abstract class StratifiedVCGenBase : VCGen {

+    public readonly static string recordProcName = "boogie_si_record";

     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

@@ -316,6 +324,37 @@ namespace VC {
         if (impl == null) continue;

         implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

       }

+      GenerateRecordFunctions();

+    }

+

+    private void GenerateRecordFunctions() {

+      foreach (var decl in program.TopLevelDeclarations) {

+        var proc = decl as Procedure;

+        if (proc == null) continue;

+        if (!proc.Name.StartsWith(recordProcName)) continue;

+        Contract.Assert(proc.InParams.Length == 1);

+

+        // Make a new function

+        TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

+        Contract.Assert(ti != null);

+        Formal returnVar = new Formal(Token.NoToken, ti, false);

+        Contract.Assert(returnVar != null);

+

+        // Get record type

+        var argtype = proc.InParams[0].TypedIdent.Type;

+

+        var ins = new VariableSeq();

+        ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

+

+        var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

+        prover.Context.DeclareFunction(recordFunc, "");

+

+        var exprs = new ExprSeq();

+        exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

+

+        Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

+        proc.Ensures.Add(new Ensures(true, freePostExpr));

+      }

     }

 

     public override void Close() {

@@ -345,6 +384,28 @@ namespace VC {
       return callSites;

     }

 

+    public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {

+      var callSites = new Dictionary<Block, List<CallSite>>();

+      foreach (Block block in implementation.Blocks) {

+        for (int i = 0; i < block.Cmds.Length; i++) {

+          AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;

+          if (assumeCmd == null) continue;

+          NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+          if (naryExpr == null) continue;

+          if (!naryExpr.Fun.FunctionName.StartsWith(recordProcName)) continue;

+          List<VCExpr> interfaceExprs = new List<VCExpr>();

+          foreach (Expr e in naryExpr.Args) {

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

+          }

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

+          if (!callSites.ContainsKey(block))

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

+          callSites[block].Add(cs);

+        }

+      }

+      return callSites;

+    }

+

     private int newVarCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

       string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();

@@ -357,29 +418,94 @@ namespace VC {
     public int CreateNewId() {

       return idCountForStratifiedInlining++;

     }

+

+    // Used inside PassifyImpl

+    protected override void addExitAssert(string implName, Block exitBlock) {

+      if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {

+        Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;

+        Contract.Assert(assertExpr != null);

+        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

+      }

+    }

+

+    public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {

+      // Construct the set of inlined procs in the original program

+      var inlinedProcs = new HashSet<string>();

+      foreach (var decl in program.TopLevelDeclarations) {

+        // Implementations

+        if (decl is Implementation) {

+          var impl = decl as Implementation;

+          if (!(impl.Proc is LoopProcedure)) {

+            inlinedProcs.Add(impl.Name);

+          }

+        }

+

+        // And recording procedures

+        if (decl is Procedure) {

+          var proc = decl as Procedure;

+          if (proc.Name.StartsWith(recordProcName)) {

+            Debug.Assert(!(decl is LoopProcedure));

+            inlinedProcs.Add(proc.Name);

+          }

+        }

+      }

+

+      return extractLoopTraceRec(

+          new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

+          mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

+    }

+

+    protected override bool elIsLoop(string procname) {

+      StratifiedInliningInfo info = null;

+      if (implName2StratifiedInliningInfo.ContainsKey(procname)) {

+        info = implName2StratifiedInliningInfo[procname];

+      }

+

+      if (info == null) return false;

+

+      var lp = info.impl.Proc as LoopProcedure;

+

+      if (lp == null) return false;

+      return true;

+    }

+

+    public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);

   }

 

   public class StratifiedVCGen : StratifiedVCGenBase {

     public bool PersistCallTree;

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

     public int numInlined = 0;

-    public readonly static string recordProcName = "boogie_si_record";

     private bool useSummary;

     private SummaryComputation summaryComputation;

     private HashSet<string> procsThatReachedRecBound;

-    public int boundUsedInLastQuery { get; private set; }

     public HashSet<string> procsToSkip;

     public Dictionary<string, int> extraRecBound;

 

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

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

+                           Program program, string/*?*/ logFilePath, bool appendLogFile) 

+    : this(program, logFilePath, appendLogFile)

+    {

+      this.procsToSkip = new HashSet<string>(procsToSkip);

+      this.extraRecBound = new Dictionary<string, int>(extraRecBound);

+

+      if (usePrevCallTree) {

+        callTree = prevCallTree;

+        PersistCallTree = true;

+      }

+      else {

+        PersistCallTree = false;

+      }

+    }

+

     public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

       : base(program, logFilePath, appendLogFile) {

-      this.GenerateRecordFunctions();

       PersistCallTree = false;

       useSummary = false;

       procsThatReachedRecBound = new HashSet<string>();

       procsToSkip = new HashSet<string>();

       extraRecBound = new Dictionary<string, int>();

-      boundUsedInLastQuery = -1;

     }

 

     // Is this procedure to be "skipped" 

@@ -397,36 +523,6 @@ namespace VC {
       else return extraRecBound[procName];

     }

 

-    public void GenerateRecordFunctions() {

-      foreach (var decl in program.TopLevelDeclarations) {

-        var proc = decl as Procedure;

-        if (proc == null) continue;

-        if (!proc.Name.StartsWith(recordProcName)) continue;

-        Contract.Assert(proc.InParams.Length == 1);

-

-        // Make a new function

-        TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

-        Contract.Assert(ti != null);

-        Formal returnVar = new Formal(Token.NoToken, ti, false);

-        Contract.Assert(returnVar != null);

-

-        // Get record type

-        var argtype = proc.InParams[0].TypedIdent.Type;

-

-        var ins = new VariableSeq();

-        ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

-

-        var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

-        prover.Context.DeclareFunction(recordFunc, "");

-

-        var exprs = new ExprSeq();

-        exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

-

-        Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

-        proc.Ensures.Add(new Ensures(true, freePostExpr));

-      }

-    }

-

     public class SummaryComputation {

       // The verification state

       VerificationState vState;

@@ -1008,7 +1104,7 @@ namespace VC {
       }

     }

 

-    public Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {

+    public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

       // Record current time

@@ -1189,7 +1285,7 @@ namespace VC {
       }

     }

 

-    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {

+    public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {

       Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));

       Debug.Assert(this.program == program);

 

@@ -1318,8 +1414,6 @@ namespace VC {
       //   case 2: (bug)     We find a bug

       //   case 3: (internal error)   The theorem prover TimesOut of runs OutOfMemory

       while (true) {

-        boundUsedInLastQuery = bound;

-

         // Check timeout

         if (CommandLineOptions.Clo.ProverKillTime != -1) {

           if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {

@@ -1630,9 +1724,7 @@ namespace VC {
         if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;

 

         StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];

-        if (!info.initialized) {

-          info.GenerateVC();

-        }

+        info.GenerateVC();

         //Console.WriteLine("Inlining {0}", procName);

         VCExpr expansion = cce.NonNull(info.vcexpr);

 

@@ -1857,9 +1949,21 @@ namespace VC {
           if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;

         }

 

-        if (extraRecursion.ContainsKey(str)) ret -= extraRecursion[str];

+        // Usual

+        if (!extraRecursion.ContainsKey(str))

+            return ret;

 

-        return ret;

+        // Usual

+        if (ret <= CommandLineOptions.Clo.RecursionBound - 1)

+            return ret;

+

+        // Special

+        if (ret >= CommandLineOptions.Clo.RecursionBound &&

+            ret <= CommandLineOptions.Clo.RecursionBound + extraRecursion[str] - 1)

+            return CommandLineOptions.Clo.RecursionBound - 1;

+

+        // Special

+        return ret - extraRecursion[str];

       }

 

       // Set user-define increment/decrement to recursionBound

@@ -2581,56 +2685,6 @@ namespace VC {
       }

     }

 

-    // Used inside PassifyImpl

-    protected override void addExitAssert(string implName, Block exitBlock) {

-      if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {

-        Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;

-        Contract.Assert(assertExpr != null);

-        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

-      }

-    }

-

-    public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {

-      // Construct the set of inlined procs in the original program

-      var inlinedProcs = new HashSet<string>();

-      foreach (var decl in program.TopLevelDeclarations) {

-        // Implementations

-        if (decl is Implementation) {

-          var impl = decl as Implementation;

-          if (!(impl.Proc is LoopProcedure)) {

-            inlinedProcs.Add(impl.Name);

-          }

-        }

-

-        // And recording procedures

-        if (decl is Procedure) {

-          var proc = decl as Procedure;

-          if (proc.Name.StartsWith(recordProcName)) {

-            Debug.Assert(!(decl is LoopProcedure));

-            inlinedProcs.Add(proc.Name);

-          }

-        }

-      }

-

-      return extractLoopTraceRec(

-          new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

-          mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

-    }

-

-    protected override bool elIsLoop(string procname) {

-      StratifiedInliningInfo info = null;

-      if (implName2StratifiedInliningInfo.ContainsKey(procname)) {

-        info = implName2StratifiedInliningInfo[procname];

-      }

-

-      if (info == null) return false;

-

-      var lp = info.impl.Proc as LoopProcedure;

-

-      if (lp == null) return false;

-      return true;

-    }

-

   } // class StratifiedVCGen

 

 } // namespace VC

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 7e3e3f17..373b685a 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1384,10 +1384,7 @@ namespace VC {
       }

     }

 

-    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {

-      //Contract.Requires(impl != null);

-      //Contract.Requires(program != null);

-      //Contract.Requires(callback != null);

+    public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

       if (impl.SkipVerification) {

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 4d2e0775..15c6e2aa 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -101,10 +101,7 @@ namespace VC {
     /// - check if |= (reach=false) => wlp.S.false holds for each reach

     ///

     /// </summary>

-    public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {

-      //Contract.Requires(impl != null);

-      //Contract.Requires(program != null);

-      //Contract.Requires(callback != null);

+    public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

       Console.WriteLine();

@@ -115,7 +112,7 @@ namespace VC {
 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));      

 

-      Transform4DoomedCheck(impl, program);

+      Transform4DoomedCheck(impl);

 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));

     

@@ -694,7 +691,7 @@ namespace VC {
     // this might be redundant, but I didn't find a better place to get this information.     

     private Dictionary<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();

 

-    private void Transform4DoomedCheck(Implementation impl, Program program)

+    private void Transform4DoomedCheck(Implementation impl)

     {

         variable2SequenceNumber = new Hashtable/*Variable -> int*/();

         incarnationOriginMap = new Dictionary<Incarnation, Absy>();

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 2d0eae82..81442950 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,15 +1,15 @@
-# Aste started: 2012-05-29 07:00:01

+# Aste started: 2012-05-30 07:00:05

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2012-05-29 07:01:20] SpecSharp revision: 221320b2a485

-# [2012-05-29 07:01:20] SscBoogie revision: 221320b2a485

-# [2012-05-29 07:02:08] Boogie revision: cd6a26bacb0d

-[2012-05-29 07:03:56] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2012-05-30 07:01:49] SpecSharp revision: f992747219c4

+# [2012-05-30 07:01:49] SscBoogie revision: f992747219c4

+# [2012-05-30 07:02:37] Boogie revision: c78721acaf27

+[2012-05-30 07:04:36] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


-[2012-05-29 07:05:22] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+[2012-05-30 07:06:04] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -22,8 +22,8 @@
     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(247,7): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(266,7): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\AbsInt\IntervalDomain.cs(49,9): warning CC1036: Detected call to method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.StrictlyBefore(Microsoft.Boogie.Variable,Microsoft.Boogie.Variable)' without [Pure] in contracts of method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.#ctor(Microsoft.Boogie.Variable,System.Nullable`1<System.Numerics.BigInteger>,System.Nullable`1<System.Numerics.BigInteger>,Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node)'.


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1402,11): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1560,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1399,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1557,11): warning CS0162: Unreachable code detected


     EXEC : warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     EXEC : warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -41,5 +41,5 @@
     warning CS0162: Unreachable code detected


     warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


-[2012-05-29 08:04:11] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2012-05-29 08:04:53] Released nightly of Boogie

+[2012-05-30 08:07:19] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2012-05-30 08:08:25] Released nightly of Boogie