Boogie:

* Bug fix:  Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case)
* Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants.  Previously, the only option was to instrument at the beginning and end of every basic block.  The new option, which is now the default, is to instrument only at the beginning of loop heads.
* Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized
* Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1

Boogie refactoring:
* Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand
* Cleaned up some parsing of command-line options

6 files changed, 107 insertions, 418 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 35175881..d6d7bbc5 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -279,16 +279,6 @@ namespace Microsoft.Boogie
     }

 

     /// <summary>

-    /// Instrument the "widen" blocks with a statement in the form of "assume J", where J is a loop predicate "variable"

-    /// </summary>

-    public void InstrumentWithLoopInvariantPredicates()

-    {

-      foreach (Declaration d in this.TopLevelDeclarations) {

-        d.InstrumentWithLoopInvariantPredicates();

-      }

-    }

-

-    /// <summary>

     /// Reset the abstract stated computed before

     /// </summary>

     public void ResetAbstractInterpretationState()

@@ -440,11 +430,6 @@ namespace Microsoft.Boogie
     public virtual void InstrumentWithInvariants () {}

 

     /// <summary>

-    /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks

-    /// </summary>

-    public virtual void InstrumentWithLoopInvariantPredicates() { /* by default it does nothing */ }

-

-    /// <summary>

     /// Reset the abstract stated computed before

     /// </summary>

     public virtual void ResetAbstractInterpretationState() { /* does nothing */    }

@@ -1993,56 +1978,39 @@ namespace Microsoft.Boogie
       {

         if (b.Lattice != null)

         {

-          CmdSeq newCommands = new CmdSeq();

-

           assert b.PreInvariant != null;      /* If the pre-abstract state is null, then something is wrong */

-

-          Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/

-          PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

-          newCommands.Add(cmd);

-          newCommands.AddRange(b.Cmds);

-

           assert b.PostInvariant != null;      /* If the post-state is null, then something is wrong */

 

- //         if(b.Cmds.Length > 0)               // If it is not an empty block

- //         {

-            inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);

-            cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

-            newCommands.Add(cmd);

- //         }

-

-          b.Cmds = newCommands;

-        }

-      }

-    }

-

-    /// <summary>

-    /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks

-    /// </summary>

-    override public void InstrumentWithLoopInvariantPredicates()

-    {

-      foreach(Block b in this.Blocks)

-      {

-        if(b.widenBlock) {  // if it is the head of a loop

-          CmdSeq newCommands = new CmdSeq();

-

-          Block! entryBlock = b;

-

-          ICollection<Block!> connectedComponents = this.GetConnectedComponents(b);       // Get the connected components from this block

-

-          // Duplicate the connected components.

-          // Note that as we duplicate all the nodes, in particular we have also to keep track of the *copy* of the entry node.

-          // This is the reason why we pass entryBlockByReference

-          ICollection<Block!> dupConnectedComponents = duplicate((!) connectedComponents, ref entryBlock);

-

-          Expr loopInvariantPredicate = new LoopPredicate(entryBlock, dupConnectedComponents);        // Create a new predicate J_{b.Label}

-

-          PredicateCmd cmd = new AssumeCmd(Token.NoToken, loopInvariantPredicate);

-

-          newCommands.Add(cmd);

-          newCommands.AddRange(b.Cmds);

-

-          b.Cmds = newCommands;

+          bool instrumentEntry;

+          bool instrumentExit;

+          switch (CommandLineOptions.Clo.InstrumentInfer) {

+            case CommandLineOptions.InstrumentationPlaces.Everywhere:

+              instrumentEntry = true;

+              instrumentExit = true;

+              break;

+            case CommandLineOptions.InstrumentationPlaces.LoopHeaders:

+              instrumentEntry = b.widenBlock;

+              instrumentExit = false;

+              break;

+            default:

+              assert false;  // unexpected InstrumentationPlaces value

+          }

+          

+          if (instrumentEntry || instrumentExit) {

+            CmdSeq newCommands = new CmdSeq();

+            if (instrumentEntry) {

+              Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/

+              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

+              newCommands.Add(cmd);

+            }

+            newCommands.AddRange(b.Cmds);

+            if (instrumentExit) {

+              Expr inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);

+              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

+              newCommands.Add(cmd);

+            }

+            b.Cmds = newCommands;

+          }

         }

       }

     }

@@ -2074,8 +2042,6 @@ namespace Microsoft.Boogie
       }

 

       assert false;   // if we are here, it means that the block is not in one of the components. This is an error.

-

-      return null;    // unreachable code, just to please the compiler

     }

 

     /// <summary>

@@ -2164,57 +2130,6 @@ namespace Microsoft.Boogie
       this.BlockPredecessorsComputed = true;

     }

 

-    /// <summary>

-    /// Make a deep copy of the set of blocks in the input.

-    /// The input must NOT contain two copies of the same block

-    /// </summary>

-    private ICollection<Block!>! duplicate(ICollection<Block!>! blocks, ref Block! head)

-    {

-      Dictionary<Block!, Block!> transMap = new Dictionary<Block!, Block!>();     // A map from the old block to a fresh one

-

-      foreach(Block! block in blocks)                                             // Create fresh copies for the blocks

-      {

-        Block! freshBlock = new Block(block.tok, block.Label, block.Cmds, block.TransferCmd);       // Construct a copy of the block

-        freshBlock.widenBlock = block.widenBlock;

-        freshBlock.Predecessors = new BlockSeq();

-        transMap.Add(block, freshBlock);                                                            // Add a link block -> freshblock

-      }

-

-      foreach(Block! block in blocks)                                             // Update the references

-      {

-        Block! freshBlock = transMap[block];

-

-        GotoCmd gotoCmd = freshBlock.TransferCmd as GotoCmd;

-        if(gotoCmd != null)

-        {

-          StringSeq! targetNames = new StringSeq();

-          BlockSeq! targetBlocks = new BlockSeq();

-

-          foreach(Block! next in (!) gotoCmd.labelTargets)

-          {

-            if(blocks.Contains(next))

-            {

-              assert transMap[next] != null;

-              targetNames.Add(next.Label);

-              targetBlocks.Add(transMap[next]);

-            }

-          }

-

-          GotoCmd freshGotoCmd = new GotoCmd(gotoCmd.tok, targetNames, targetBlocks);

-          freshBlock.TransferCmd = freshGotoCmd;

-        }

-        else

-        {

-          assert freshBlock.TransferCmd is ReturnCmd; // Do nothing as we do not need to update a returnCmd.

-                                                      // However, as we want to make the code robust, we check that it is a ReturnCmd

-        }

-      }

-

-      head = transMap[head];

-

-      return transMap.Values;

-    }

-

     public void PruneUnreachableBlocks() {

       ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ ();

       List<Block!> reachableBlocks = new List<Block!>();

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index 926724cb..41a62515 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -672,7 +672,7 @@ namespace Microsoft.Boogie
   // Block

   public sealed class Block : Absy

   {

-    public readonly string! Label;

+    public string! Label;  // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal

     [Rep] [ElementsPeer] public CmdSeq! Cmds;

     [Rep]  //PM: needed to verify Traverse.Visit

     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index baf12310..eaf4e640 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -836,8 +836,6 @@ namespace Microsoft.Boogie
     

     T Visit(FunctionCall! functionCall);

     

-    T Visit(LoopPredicateName! loopPredicateName);

-    

     T Visit(MapSelect! mapSelect);

     

     T Visit(MapStore! mapStore);

@@ -1572,171 +1570,6 @@ namespace Microsoft.Boogie
 

   }

 

-  /// <summary>

-  /// A subclass of FunctionCall that stands for a zero-argument function call, used as a loop invariant placeholder

-  /// </summary>

-  public class LoopPredicateName : FunctionCall

-  {         

-    private Block! block;             // The block the predicate refers to    

-    public Block! Block

-    {    

-      get                       

-      {

-        return block;

-      }

-    }

-

-    private string! blockName;      // The name of the block

-    private ICollection<Block!>! component;

-    public ICollection<Block!>! Component

-    { 

-      get

-      {

-        return this.component;

-      }

-    }

-

-    public string! Name 

-    {

-      get

-      {

-        return "J_" + this.blockName;

-      }

-    } 

-

-    invariant block.Label == blockName;   // Note that we ask for object equality of strings...

-

-    private Hashtable /* Var -> Incarnations */ preHavocIncarnationMap;

-    public Hashtable PreHavocIncarnationMap

-    {

-      get 

-      {

-        return this.preHavocIncarnationMap;

-      }

-    }

-

-    private Hashtable /* Var -> Incarnations */ postHavocIncarnationMap;

-    public Hashtable PostHavocIncarnationMap

-    {

-      get 

-      {

-        return this.postHavocIncarnationMap;

-      }

-    }

-

-

-    // Those below are the inverse maps of the maps between variables and incarnations

-    private Hashtable /* String -> Var */ preHavocIncarnationInverseMap;

-    private Hashtable /* String -> Var */ postHavocIncarnationInverseMap;

-

-    public Hashtable PreHavocInverseMap 

-    {

-      get 

-      {

-        if(this.preHavocIncarnationInverseMap == null) 

-        {

-          this.preHavocIncarnationInverseMap = new Hashtable();

-          assert this.preHavocIncarnationMap != null;                   // If we get at this point, then something is wrong with the program

-          foreach(object! key in (!) (this.preHavocIncarnationMap).Keys) 

-          {

-            object! val = (!) this.preHavocIncarnationMap[key];

-            if(!this.preHavocIncarnationInverseMap.ContainsKey(val.ToString()))

-              this.preHavocIncarnationInverseMap.Add(val.ToString(), key);

-          }

-        }

-        return this.preHavocIncarnationInverseMap;

-      }

-    }

-

-    public Hashtable PostHavocInverseMap 

-    {

-      get 

-      {

-        if(this.postHavocIncarnationInverseMap == null) 

-        {

-          this.postHavocIncarnationInverseMap = new Hashtable();

-          assert this.postHavocIncarnationMap != null;        // If it is null, something is wrong before...

-          foreach(object! key in (!) (this.postHavocIncarnationMap).Keys) 

-          {

-            object! val = (!) this.postHavocIncarnationMap[key];

-            if(!this.postHavocIncarnationInverseMap.ContainsKey(val.ToString()))

-            this.postHavocIncarnationInverseMap.Add(val.ToString(), key);

-          }

-        }

-        return this.postHavocIncarnationInverseMap;

-      }

-    }

-

-    /// <summary>

-    /// Create a new LoopPredicate

-    /// </summary>      

-    public LoopPredicateName(Block! block, ICollection<Block!>! component) 

-      : base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool))

-    {

-      this.block = block;

-      this.blockName = block.Label;

-      this.component = component;

-      // base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool));

-    }       

-

-    public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post) 

-    {

-      assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null;

-        

-      this.preHavocIncarnationMap = pre;

-      this.postHavocIncarnationMap = post;

-    }

-

-    /// <summary>

-    /// Writes down the loop predicate and the incarnations map before and after the havoc statements

-    /// </summary>

-    public override void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext) 

-    {

-      string! pre, post;

-

-      if(this.postHavocIncarnationMap != null && this.preHavocIncarnationMap != null)        

-      {

-        pre = "pre: [ " + hashtableToString(this.preHavocIncarnationMap) +" ]";  

-        post = "post: [ " + hashtableToString(this.postHavocIncarnationMap) +" ]";        

-      }

-      else 

-      {

-        pre = post = "[]";

-      }

-

-      stream.Write("J_" + this.blockName);

-      stream.Write("(");

-      stream.Write(pre + ", " + post);

-      stream.Write(")");

-    }

-

-    public override Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc) 

-    {

-      tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

-      return Type.Bool;

-    }

-

-    public override int ArgumentCount { get { return 0; } }

-

-    private string! hashtableToString(Hashtable! map) 

-    {

-      string! outVal = "";

-

-      foreach (object! key in map.Keys) 

-      {

-        object val = map[key];

-        outVal += key + " -> " + val + ",";

-      }

-

-      return outVal;

-    }    

-

-    public override T Dispatch<T>(IAppliableVisitor<T>! visitor) {

-      return visitor.Visit(this);

-    }

-

-  }

-

   public class NAryExpr : Expr, AI.IFunApp

   {

     [Additive] [Peer]

@@ -1870,68 +1703,6 @@ namespace Microsoft.Boogie
     }

   }

 

-  /// <summary>

-  /// An instance of LoopPredicate stands for a loop invariant predicate 

-  /// </summary>

-  public class LoopPredicate : NAryExpr 

-  {

-    private static ExprSeq! emptyArgs = new ExprSeq(new Expr[0]);         // Share the emptylist of arguments among several instances

-    

-    invariant loopPredicateName == Fun;                                   // loopPredicateName is just a way of subtyping Fun...

-    LoopPredicateName! loopPredicateName; 

-

-    Hashtable /* Var -> Expr */ preHavocIncarnationMap;

-    Hashtable /* Var -> Expr */ postHavocIncarnationMap;    

-

-    private Block! block;                         // The block the predicate refers to

-    private string! BlockName;                    // Name of the widen block the predicate refers to 

-    private ICollection<Block!> component;        // The component the block belongs to 

-    

-    /// <summary>

-    /// Create a predicate (standing for a loop invariant). The parameter are the name of the block and the (strong) connect components the block belongs to

-    /// </summary>

-    public LoopPredicate(Block! block, ICollection<Block!>! component) 

-    {

-      this.block = block;

-      this.BlockName = block.Label;

-      this.component = component;      

-

-      LoopPredicateName! tmp;        // to please the compiler we introde a temp variable

-      this.loopPredicateName = tmp = new LoopPredicateName(block, component); 

-      base(Token.NoToken, tmp, emptyArgs); // due to locally computed data

-    } 

-

-    public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post) 

-    {

-      assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null; // The method must be called just once

-        

-      this.preHavocIncarnationMap = pre;

-      this.postHavocIncarnationMap = post;

-      this.loopPredicateName.SetPreAndPostHavocIncarnationMaps(pre, post);

-    }  

-

-    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj)

-    {

-      if (obj == null) return false;

-      if (!(obj is LoopPredicate)) return false;

-

-      LoopPredicate pred = (LoopPredicate) obj;

-      return this.BlockName.Equals(pred.BlockName);

-    }

-

-    [Pure]

-    public override int GetHashCode() 

-    {

-      return this.BlockName.GetHashCode();

-    }

-

-    public override Absy! StdDispatch(StandardVisitor! visitor)

-    {

-      return visitor.VisitLoopPredicate(this);

-    }

-  }

-

   public class MapSelect : IAppliable, AI.IFunctionSymbol {

 

     public readonly int Arity;

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index da8ee0fe..1d16b569 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -75,6 +75,8 @@ namespace Microsoft.Boogie
     public string! LogPrefix = "";

     public bool PrintInstrumented = false;

     public bool InstrumentWithAsserts = false;

+    public enum InstrumentationPlaces { LoopHeaders, Everywhere }

+    public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders;

     public bool PrintWithUniqueASTIds = false;

     private string XmlSinkFilename = null;

     [Peer] public XmlSink XmlSink = null;

@@ -604,48 +606,46 @@ namespace Microsoft.Boogie
             break;

   

           case "-proverWarnings":

-          case "/proverWarnings":

-            if (ps.ConfirmArgumentCount(1))

-            {

-              switch (args[ps.i])

-              {

-                case "0":

+          case "/proverWarnings": {

+            int pw = 0;

+            if (ps.GetNumericArgument(ref pw, 3)) {

+              switch (pw) {

+                case 0:

                   PrintProverWarnings = ProverWarnings.None;

                   break;

-                case "1":

+                case 1:

                   PrintProverWarnings = ProverWarnings.Stdout;

                   break;

-                case "2":

+                case 2:

                   PrintProverWarnings = ProverWarnings.Stderr;

                   break;

                 default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

+                  assert false;  // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

             break;

+          }

 

           case "-env":

-          case "/env":

-            if (ps.ConfirmArgumentCount(1))

-            {

-              switch (args[ps.i])

-              {

-                case "0":

+          case "/env": {

+            int e = 0;

+            if (ps.GetNumericArgument(ref e, 3)) {

+              switch (e) {

+                case 0:

                   ShowEnv = ShowEnvironment.Never;

                   break;

-                case "1":

+                case 1:

                   ShowEnv = ShowEnvironment.DuringPrint;

                   break;

-                case "2":

+                case 2:

                   ShowEnv = ShowEnvironment.Always;

                   break;

                 default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

+                  assert false;  // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

             break;

+          }

 

           case "-loopUnroll":

           case "/loopUnroll":

@@ -805,64 +805,52 @@ namespace Microsoft.Boogie
             break;

            

           case "-subsumption":

-          case "/subsumption":

-            if (ps.ConfirmArgumentCount(1))

-            {

-              switch (args[ps.i])

-              {

-                case "0":

+          case "/subsumption": {

+            int s = 0;

+            if (ps.GetNumericArgument(ref s, 3)) {

+              switch (s) {

+                case 0:

                   UseSubsumption = SubsumptionOption.Never;

                   break;

-                case "1":

+                case 1:

                   UseSubsumption = SubsumptionOption.NotForQuantifiers;

                   break;

-                case "2":

+                case 2:

                   UseSubsumption = SubsumptionOption.Always;

                   break;

                 default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

+                  assert false;  // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

             break;

+          }

           

           case "-liveVariableAnalysis":

-          case "/liveVariableAnalysis":

-            if (ps.ConfirmArgumentCount(1))

-            {

-              switch (args[ps.i])

-              {

-                case "0": 

-                  LiveVariableAnalysis = false;

-                  break;

-                case "1":

-                  LiveVariableAnalysis = true;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

+          case "/liveVariableAnalysis": {

+            int lva = 0;

+            if (ps.GetNumericArgument(ref lva, 2)) {

+              LiveVariableAnalysis = lva == 1;

             }

             break;

+          }

+            

+          case "-removeEmptyBlocks":

+          case "/removeEmptyBlocks": {

+            int reb = 0;

+            if (ps.GetNumericArgument(ref reb, 2)) {

+              RemoveEmptyBlocks = reb == 1;

+            }

+            break;

+          }

             

           case "-coalesceBlocks":

-          case "/coalesceBlocks":

-            if (ps.ConfirmArgumentCount(1))

-            {

-              switch (args[ps.i])

-              {

-                case "0": 

-                  CoalesceBlocks = false;

-                  break;

-                case "1":

-                  CoalesceBlocks = true;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

+          case "/coalesceBlocks": {

+            int cb = 0;

+            if (ps.GetNumericArgument(ref cb, 2)) {

+              CoalesceBlocks = cb == 1;

             }

             break;

+          }

 

           case "/DoomDebug":

             vcVariety = VCVariety.Doomed;

@@ -983,7 +971,25 @@ namespace Microsoft.Boogie
               }

             }

             break;

-            

+

+          case "-instrumentInfer":

+          case "/instrumentInfer":

+            if (ps.ConfirmArgumentCount(1)) {

+              switch (args[ps.i])

+              {

+                case "e":

+                  InstrumentInfer = InstrumentationPlaces.Everywhere;

+                  break;

+                case "h":

+                  InstrumentInfer = InstrumentationPlaces.LoopHeaders;

+                  break;

+                default:

+                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                  break;

+              }

+            }

+            break;

+

           case "-vcBrackets":

           case "/vcBrackets":

             ps.GetNumericArgument(ref BracketIdsInVC, 2);

@@ -1163,7 +1169,6 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||

               ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) ||

               ps.CheckBooleanFlag("noVerify", ref Verify, false) ||

-              ps.CheckBooleanFlag("noRemoveEmptyBlocks", ref RemoveEmptyBlocks, false) ||

               ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||

               ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) ||

               ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||

@@ -1840,7 +1845,6 @@ namespace Microsoft.Boogie
                    p = polyhedra for linear inequalities

                    s = debug statistics

                 0..9 = number of iterations before applying a widen (default=0)

-  /loopInvOnDemand : Infer loop invariants on demand      

   /noinfer       : turn off the default inference, and overrides the /infer

                    switch on its left

   /checkInfer    : instrument inferred invariants as asserts to be checked by

@@ -1849,6 +1853,10 @@ namespace Microsoft.Boogie
                     supported)

   /contractInfer : perform procedure contract inference

   /logInfer      : print debug output during inference

+  /instrumentInfer : h - instrument inferred invariants only at beginning of

+                         loop headers (default)

+                     e - instrument inferred invariants at beginning and end

+                         of every block

   /printInstrumented : print Boogie program after it has been

                    instrumented with invariants

   /Houdini[:<flags>] : perform procedure Houdini

@@ -1869,7 +1877,8 @@ namespace Microsoft.Boogie
   /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis 

                               1 = perform live variable analysis (default)

   /noVerify      : skip VC generation and invocation of the theorem prover

-  /noRemoveEmptyBlocks : do not remove empty blocks during VC generation

+  /removeEmptyBlocks:<c> : 0 - do not remove empty blocks during VC generation

+                           1 - remove empty blocks (default)

   /coalesceBlocks:<c> : 0 = do not coalesce blocks

                         1 = coalesce blocks (default)

   /vc:<variety>  : n = nested block (default for non-/prover:z3),

diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
index 506739bf..0686212e 100644
--- a/Source/Core/DeadVarElim.ssc
+++ b/Source/Core/DeadVarElim.ssc
@@ -197,8 +197,10 @@ namespace Microsoft.Boogie
               b.Cmds.Add(cmd);

             }

             b.TransferCmd = succ.TransferCmd;

-            if (!b.tok.IsValid && succ.tok.IsValid)

+            if (!b.tok.IsValid && succ.tok.IsValid) {

               b.tok = succ.tok;

+              b.Label = succ.Label;

+            }

             removedBlocks.Add(succ);

             dfsStack.Push(b);

             visitedBlocks.Remove(b);

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index c6b50b24..6e50f6db 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -319,14 +319,6 @@ namespace Microsoft.Boogie
       return node; 

     }

 

-    /// <summary>

-    /// Just invoke VisitNAryExpr

-    /// </summary>

-    public virtual Expr! VisitLoopPredicate(LoopPredicate! node) 

-    {

-      return this.VisitNAryExpr(node);            

-    }

-

     public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)

     {

       node.Map = (AssignLhs!)this.Visit(node.Map);