public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
      //modifies ctxt.*;
    {
      Contract.Requires(b != null);
      Contract.Requires(N != null);
      Contract.Requires(ctxt != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      VCExpressionGenerator gen = ctxt.Ctxt.ExprGen;
      Contract.Assert(gen != null);
      
      VCExpr res = N;

      for (int i = b.Cmds.Count; --i >= 0; )
      {
        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
      }
      
      int id = b.UniqueId;
      if (ctxt.Label2absy != null) {
        ctxt.Label2absy[id] = b;
      }

      try {
        cce.BeginExpose(ctxt);
        if (ctxt.Label2absy == null) {
          return res;
        }
        else {
          return gen.Implies(gen.LabelPos(cce.NonNull(id.ToString()), VCExpressionGenerator.True), res);
        }
      } finally {
        cce.EndExpose();
      }
    }

    public static List<Block/*!*/>/*!*/ UnrollLoops(Block start, int unrollMaxDepth, bool soundLoopUnrolling) {
      Contract.Requires(start != null);

      Contract.Requires(0 <= unrollMaxDepth);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
      Dictionary<Block, GraphNode/*!*/> gd = new Dictionary<Block, GraphNode/*!*/>();
      HashSet<Block> beingVisited = new HashSet<Block>();
      GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);

      // Compute SCCs
      StronglyConnectedComponents<GraphNode/*!*/> sccs =
        new StronglyConnectedComponents<GraphNode/*!*/>(gd.Values, Preds, Succs);
      Contract.Assert(sccs != null);
      sccs.Compute();
      Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> containingSCC = new Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>();
      foreach (SCC<GraphNode/*!*/> scc in sccs) {
        foreach (GraphNode/*!*/ n in scc) {
          Contract.Assert(n != null);
          containingSCC[n] = scc;
        }
      }

      LoopUnroll lu = new LoopUnroll(unrollMaxDepth, soundLoopUnrolling, containingSCC, new List<Block/*!*/>());
      lu.Visit(gStart);
      lu.newBlockSeqGlobal.Reverse();
      return lu.newBlockSeqGlobal;
    }

  void PredicateCmd(Expr p, Expr pDom, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
    var cCmd = cmd as CallCmd;
    if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
      if (p == null) {
        block.Cmds.Add(cmd);
        nextBlock = block;
        return;
      }

      var trueBlock = new Block();
      blocks.Add(trueBlock);
      trueBlock.Label = block.Label + ".call.true";
      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
      trueBlock.Cmds.Add(cmd);

      var falseBlock = new Block();
      blocks.Add(falseBlock);
      falseBlock.Label = block.Label + ".call.false";
      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));

      var contBlock = new Block();
      blocks.Add(contBlock);
      contBlock.Label = block.Label + ".call.cont";

      block.TransferCmd =
        new GotoCmd(Token.NoToken, new List<Block> { trueBlock, falseBlock });
      trueBlock.TransferCmd = falseBlock.TransferCmd =
        new GotoCmd(Token.NoToken, new List<Block> { contBlock });
      nextBlock = contBlock;
    } else {
      PredicateCmd(p, pDom, block.Cmds, cmd);
      nextBlock = block;
    }
  }

    static void Visit(Block b) {
      Contract.Requires(b != null);
      Contract.Assume(cce.IsExposable(b));
      if (b.TraversingStatus == Block.VisitState.BeingVisited) {
        cce.BeginExpose(b);
        // we got here through a back-edge
        b.widenBlock = true;
        cce.EndExpose();
      } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {
        // do nothing... we already saw this node
      } else if (b.TransferCmd is GotoCmd) {
        Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

        GotoCmd g = (GotoCmd)b.TransferCmd;
        cce.BeginExpose(b);

        cce.BeginExpose(g);   //PM: required for the subsequent expose (g.labelTargets)
        b.TraversingStatus = Block.VisitState.BeingVisited;

        // labelTargets is made non-null by Resolve, which we assume
        // has already called in a prior pass.
        Contract.Assume(g.labelTargets != null);
        cce.BeginExpose(g.labelTargets);
        foreach (Block succ in g.labelTargets)
        //              invariant b.currentlyTraversed;
        //PM: The following loop invariant will work once properties are axiomatized
        //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
              {
          Contract.Assert(succ != null);
          Visit(succ);
        }
        cce.EndExpose();

        Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);
        //            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

        b.TraversingStatus = Block.VisitState.AlreadyVisited;

        //PM: The folowing assumption is needed because we cannot prove that a simple field update
        //PM: leaves the value of a property unchanged.
        Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
        cce.EndExpose();
      } else {
        Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd);        // It must be a returnCmd;
      }
    }

        /// <summary>
        /// Compute the blocks in the body loop. 
        /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>
        /// <return> The blocks that are in the loop from block </return>
        /// </summary>
        public static List<Block> ComputeLoopBodyFrom(Block block)
        {
            Contract.Requires(block.widenBlock);
              Contract.Requires(block != null);
              Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

              Contract.Assert(rootBlock == null);
              rootBlock = block;

              List<Block/*!*/> blocksInLoop = new List<Block/*!*/>();         // We use a list just because .net does not define a set
              List<Block/*!*/> visitingPath = new List<Block/*!*/>();         // The order is important, as we want paths

              blocksInLoop.Add(block);

              DoDFSVisit(block, visitingPath, blocksInLoop);

              visitingPath.Add(block);

              rootBlock = null;   // We reset the invariant

              return blocksInLoop;
        }

        // There is no default constructor, because these parameters are needed for most subclasses
        public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach) 
        {
            m_BlockH = new BlockHierachy(imp, unifiedexit);
            __DEBUG_EQCLeaf = m_BlockH.Leaves.Count;
            
            //foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
            //{
            //    if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]);
            //}
            //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);


            if (__DEBUGOUT)
            {
                Console.WriteLine("MaBranchingDepth {0}  MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK);

                Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0);
            }

            MaxBlocks = imp.Blocks.Count;
            MinBlocks = imp.Blocks.Count;
            HACK_NewCheck = false;
            __DEBUG_BlocksTotal = imp.Blocks.Count;
        }

 private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks,
     Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
 {
     // Add initial block
     List<AssignLhs> lhss = new List<AssignLhs>();
     List<Expr> rhss = new List<Expr>();
     if (pc != null)
     {
         lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
         rhss.Add(Expr.False);
         foreach (Variable oldPc in oldPcs)
         {
             lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));
             rhss.Add(Expr.False);
         }
         lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
         rhss.Add(Expr.False);
         foreach (Variable oldOk in oldOks)
         {
             lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));
             rhss.Add(Expr.False);
         }
     }
     Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
     foreach (var domainName in linearTypeChecker.linearDomains.Keys)
     {
         domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);
     }
     for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
     {
         Variable v = impl.InParams[i];
         var domainName = linearTypeChecker.FindDomainName(v);
         if (domainName == null) continue;
         if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
         var domain = linearTypeChecker.linearDomains[domainName];
         if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
         Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });
         domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });
     }
     foreach (string domainName in linearTypeChecker.linearDomains.Keys)
     {
         lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
         rhss.Add(domainNameToExpr[domainName]);
     }
     foreach (Variable g in ogOldGlobalMap.Keys)
     {
         lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
         rhss.Add(Expr.Ident(g));
     }
     if (lhss.Count > 0)
     {
         Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));
         impl.Blocks.Insert(0, initBlock);
     }
 }

 public override Block VisitBlock(Block node)
 {
     Block block = base.VisitBlock(node);
     absyMap[block] = node;
     return block;
 }

        public override Procedure VisitProcedure(Procedure node)
        {
            if (!civlTypeChecker.procToActionInfo.ContainsKey(node))
                return node;
            if (!procMap.ContainsKey(node))
            {
                enclosingProc = node;
                Procedure proc = (Procedure)node.Clone();
                proc.Name = string.Format("{0}_{1}", node.Name, layerNum);
                proc.InParams = this.VisitVariableSeq(node.InParams);
                proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
                proc.OutParams = this.VisitVariableSeq(node.OutParams);

                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node];
                if (actionInfo.createdAtLayerNum < layerNum)
                {
                    proc.Requires = new List<Requires>();
                    proc.Ensures = new List<Ensures>();
                    Implementation impl;
                    AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
                    if (atomicActionInfo != null)
                    {
                        CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action);
                        List<Cmd> cmds = new List<Cmd>();
                        foreach (AssertCmd assertCmd in atomicActionInfo.gate)
                        {
                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr)));
                        }
                        Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
                            new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
                                                       new List<Block>(new Block[] { action.Blocks[0] })));
                        List<Block> newBlocks = new List<Block>();
                        newBlocks.Add(newInitBlock);
                        newBlocks.AddRange(action.Blocks);
                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);
                    }
                    else
                    {
                        Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));
                        List<Block> newBlocks = new List<Block>();
                        newBlocks.Add(newInitBlock);
                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks);
                    }
                    impl.Proc = proc;
                    impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
                    impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
                    impls.Add(impl);
                }
                else
                {
                    yieldingProcs.Add(proc);
                    proc.Requires = this.VisitRequiresSeq(node.Requires);
                    proc.Ensures = this.VisitEnsuresSeq(node.Ensures);
                }
                procMap[node] = proc;
                proc.Modifies = new List<IdentifierExpr>();
                civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
            }
            return procMap[node];
        }

        private List<Block> CreateAssertsWithAssumes(List<List<Tuple<Variable, Expr, Expr>>> eqVarsGroups, List<Cmd> asserts)
        {
            int n = eqVarsGroups.Count();
            if (n == 0)
            {
                var b = new Block { Label = SectionLabelPrefix + "_" + _labelCounter++ };
                b.Cmds.AddRange(asserts);
                return new List<Block>() { b };
            }

            var result = new List<Block>();
            EnumerateAssumes(new List<Tuple<int, int>>(), n, asserts, eqVarsGroups, result);
            return result;
        }

      public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, HashSet<Block> beingVisited) {
        Contract.Requires(beingVisited != null);
        Contract.Requires(b != null);
        Contract.Requires(cce.NonNullDictionaryAndValues(gd));
        Contract.Ensures(Contract.Result<GraphNode>() != null);
        GraphNode g;
        if (gd.TryGetValue(b, out g)) {
          Contract.Assume(from != null);
          Contract.Assert(g != null);
          if (beingVisited.Contains(b)) {
            // it's a cut point
            g.isCutPoint = true;
            from.BackEdges.Add(g);
            g.Predecessors.Add(from);
          } else {
            from.ForwardEdges.Add(g);
            g.Predecessors.Add(from);
          }

        } else {
          List<Cmd> body = GetOptimizedBody(b.Cmds);
          g = new GraphNode(b, body);
          gd.Add(b, g);
          if (from != null) {
            from.ForwardEdges.Add(g);
            g.Predecessors.Add(from);
          }

          if (body != b.Cmds) {
            // the body was optimized -- there is no way through this block
          } else {
            beingVisited.Add(b);

            GotoCmd gcmd = b.TransferCmd as GotoCmd;
            if (gcmd != null) {
              Contract.Assume(gcmd.labelTargets != null);
              foreach (Block/*!*/ succ in gcmd.labelTargets) {
                Contract.Assert(succ != null);
                ComputeGraphInfo(g, succ, gd, beingVisited);
              }
            }

            beingVisited.Remove(b);
          }
        }
        return g;
      }

 private bool IsYieldingHeader(Graph<Block> graph, Block header)
 {
     foreach (Block backEdgeNode in graph.BackEdgeNodes(header))
     {
         foreach (Block x in graph.NaturalLoops(header, backEdgeNode))
         {
             foreach (Cmd cmd in x.Cmds)
             {
                 if (cmd is YieldCmd)
                     return true;
                 if (cmd is ParCallCmd)
                     return true;
                 CallCmd callCmd = cmd as CallCmd;
                 if (callCmd == null) continue;
                 if (yieldingProcs.Contains(callCmd.Proc))
                     return true;
             }
         }
     }
     return false;
 }

 public override Block VisitBlock(Block node) {
   //Contract.Requires(node != null);
   Contract.Ensures(Contract.Result<Block>() != null);
   return base.VisitBlock((Block) node.Clone());
 }

 private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
   var headsSeen = new HashSet<Block>();
   while (i.MoveNext()) {
     var b = i.Current;
     if (b.Item1 == dest)
       yield break;
     else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
       headsSeen.Add(b.Item1);
     else if (b.Item2 && !headsSeen.Contains(b.Item1))
       yield return b.Item1;
   }
   Debug.Assert(false);
 }

 public PartInfo(Expr p, Block r) { pred = p; realDest = r; }

 IEnumerable<Block> LoopsExited(Block src, Block dest) {
   var i = sortedBlocks.GetEnumerator();
   while (i.MoveNext()) {
     var b = i.Current;
     if (b.Item1 == src) {
       return LoopsExitedForwardEdge(dest, i);
     } else if (b.Item1 == dest) {
       return LoopsExitedBackEdge(src, i);
     }
   }
   Debug.Assert(false);
   return null;
 }

 private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
   var headsSeen = new HashSet<Block>();
   while (i.MoveNext()) {
     var b = i.Current;
     if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
       headsSeen.Add(b.Item1);
     else if (b.Item2)
       headsSeen.Remove(b.Item1);
     if (b.Item1 == src)
       return headsSeen;
   }
   Debug.Assert(false);
   return null;
 }

  // hasPredicatedRegion is true iff the block or its targets are predicated
  // (i.e. we enter, stay within or exit a predicated region).
  void PredicateTransferCmd(Expr p, Block src, List<Cmd> cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
    hasPredicatedRegion = predMap.ContainsKey(src);

    if (cmd is GotoCmd) {
      var gCmd = (GotoCmd)cmd;

      hasPredicatedRegion = hasPredicatedRegion ||
        gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));

      if (gCmd.labelTargets.Count == 1) {
        if (defMap.ContainsKey(gCmd.labelTargets[0])) {
          PredicateCmd(p, Expr.True, cmdSeq,
                       Cmd.SimpleAssign(Token.NoToken,
                                        Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
        }
      } else {
        Debug.Assert(gCmd.labelTargets.Count > 1);
        Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
                                                              partInfo.ContainsKey(t)));
        foreach (Block target in gCmd.labelTargets) {
          if (!partInfo.ContainsKey(target))
            continue;

          // In this case we not only predicate with the current predicate p,
          // but also with the "part predicate"; this ensures that we do not
          // update a predicate twice when it occurs in both parts.
          var part = partInfo[target];
          if (defMap.ContainsKey(part.realDest)) {
            PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
                         Cmd.SimpleAssign(Token.NoToken,
                                          Expr.Ident(predMap[part.realDest]), part.pred));
          }
          var predsExitingLoop = new Dictionary<Block, List<Expr>>();
          foreach (Block exit in LoopsExited(src, target)) {
            List<Expr> predList;
            if (!predsExitingLoop.ContainsKey(exit))
              predList = predsExitingLoop[exit] = new List<Expr>();
            else
              predList = predsExitingLoop[exit];
            predList.Add(part.pred);
          }
          foreach (var pred in predsExitingLoop) {
            PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), Expr.True, cmdSeq,
                         Cmd.SimpleAssign(Token.NoToken,
                                          Expr.Ident(predMap[pred.Key]),
                                          Expr.Not(pred.Value.Aggregate(Expr.Or))));
          }
        }
      }
    } else if (cmd is ReturnCmd) {
      // Blocks which end in a return will never share a predicate with a block
      // which appears after it.  Furthermore, such a block cannot be part of a
      // loop.  So it is safe to do nothing here.
    } else {
      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
    }
  }

 GraphNode(Block b, List<Cmd> body) {
   Contract.Requires(body != null);
   Contract.Requires(b != null);
   this.Block = b;
   this.Body = body;
 }

    Block Visit(GraphNode node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Block>() != null);
      Block orig = node.Block;
      Block nw;
      if (newBlocks.TryGetValue(orig, out nw)) {
        Contract.Assert(nw != null);

      } else {
        List<Cmd> body;
        TransferCmd tcmd;
        Contract.Assert(orig.TransferCmd != null);

        if (next == null && node.IsCutPoint) {
          // as the body, use the assert/assume commands that make up the loop invariant
          body = new List<Cmd>();
          foreach (Cmd/*!*/ c in node.Body) {
            Contract.Assert(c != null);
            if (c is PredicateCmd || c is CommentCmd) {
              body.Add(c);
            } else {
              break;
            }
          }
          if (soundLoopUnrolling) {
            body.Add(new AssertCmd(orig.tok, Bpl.Expr.False));
          } else {
            body.Add(new AssumeCmd(orig.tok, Bpl.Expr.False));
          }
          tcmd = new ReturnCmd(orig.TransferCmd.tok);

        } else {
          body = node.Body;
          List<Block> newSuccs = new List<Block>();

          foreach (GraphNode succ in node.ForwardEdges) {
            Block s;
            if (containingSCC[node] == containingSCC[succ]) {
              s = Visit(succ);
            } else {
              Contract.Assert(head != null); // follows from object invariant
              s = head.Visit(succ);
            }
            newSuccs.Add(s);
          }

          Contract.Assert(next != null || node.BackEdges.Count == 0);  // follows from if-else test above and the GraphNode invariant
          foreach (GraphNode succ in node.BackEdges) {
            Contract.Assert(next != null);  // since if we get here, node.BackEdges.Count != 0
            Block s = next.Visit(succ);
            newSuccs.Add(s);
          }

          if (newSuccs.Count == 0) {
            tcmd = new ReturnCmd(orig.TransferCmd.tok);
          } else {
            tcmd = new GotoCmd(orig.TransferCmd.tok, newSuccs);
          }
        }

        nw = new Block(orig.tok, orig.Label + "#" + this.c, body, tcmd);
        newBlocks.Add(orig, nw);
        newBlockSeqGlobal.Add(nw);
      }

      return nw;
    }