bunch of refactorings

- moved doomed and predication code into separate projects;
  for doomed there is a static dependency from BoogieDriver
  but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs

14 files changed, 3 insertions, 4549 deletions

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
deleted file mode 100644
index 9df1c086..00000000
--- a/Source/VCGeneration/BlockPredicator.cs
+++ /dev/null
@@ -1,373 +0,0 @@
-using Graphing;

-using System;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Diagnostics.Contracts;

-using System.Linq;

-

-namespace Microsoft.Boogie {

-

-public class BlockPredicator {

-

-  Program prog;

-  Implementation impl;

-  Graph<Block> blockGraph;

-

-  bool createCandidateInvariants = true;

-  bool useProcedurePredicates = true;

-

-  Expr returnBlockId;

-

-  LocalVariable curVar, pVar;

-  IdentifierExpr cur, p, fp;

-  Expr pExpr;

-  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, bool cci, bool upp) {

-    prog = p;

-    impl = i;

-    createCandidateInvariants = cci;

-    useProcedurePredicates = upp;

-  }

-

-  void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {

-    if (!useProcedurePredicates && cmd is CallCmd) {

-      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 BlockSeq(trueBlock, falseBlock));

-      trueBlock.TransferCmd = falseBlock.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));

-      nextBlock = contBlock;

-    } else {

-      PredicateCmd(block.Cmds, cmd);

-      nextBlock = block;

-    }

-  }

-

-  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {

-    if (cmd is AssignCmd) {

-      var aCmd = (AssignCmd)cmd;

-      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,

-                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>

-                     new NAryExpr(Token.NoToken,

-                       new IfThenElse(Token.NoToken),

-                       new ExprSeq(p, rhs, lhs.AsExpr))))));

-    } else if (cmd is AssertCmd) {

-      var aCmd = (AssertCmd)cmd;

-      if (cmdSeq.Last() is AssignCmd &&

-          cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {

-        // This may be a loop invariant.  Make sure it continues to appear as

-        // the first statement in the block.

-        var assign = cmdSeq.Last();

-        cmdSeq.Truncate(cmdSeq.Length-1);

-        Expr newExpr = new EnabledReplacementVisitor(pExpr).VisitExpr(aCmd.Expr);

-        aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(pExpr, newExpr);

-        cmdSeq.Add(aCmd);

-        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));

-        cmdSeq.Add(assign);

-      } else {

-        aCmd.Expr = Expr.Imp(p, aCmd.Expr);

-        cmdSeq.Add(aCmd);

-        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));

-      }

-    } else if (cmd is AssumeCmd) {

-      var aCmd = (AssumeCmd)cmd;

-      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));

-    } else if (cmd is HavocCmd) {

-      var hCmd = (HavocCmd)cmd;

-      foreach (IdentifierExpr v in hCmd.Vars) {

-        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;

-        Contract.Assert(type != null);

-

-        IdentifierExpr havocTempExpr;

-        if (havocVars.ContainsKey(type)) {

-          havocTempExpr = havocVars[type];

-        } else {

-          var havocVar = new LocalVariable(Token.NoToken,

-                             new TypedIdent(Token.NoToken,

-                                            "_HAVOC_" + type.ToString(), type));

-          impl.LocVars.Add(havocVar);

-          havocVars[type] = havocTempExpr =

-            new IdentifierExpr(Token.NoToken, havocVar);

-        }

-        cmdSeq.Add(new HavocCmd(Token.NoToken,

-                                new IdentifierExprSeq(havocTempExpr)));

-        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

-                                    new NAryExpr(Token.NoToken,

-                                      new IfThenElse(Token.NoToken),

-                                      new ExprSeq(p, havocTempExpr, v))));

-      }

-    } else if (cmd is CallCmd) {

-      Debug.Assert(useProcedurePredicates);

-      var cCmd = (CallCmd)cmd;

-      cCmd.Ins.Insert(0, p);

-      cmdSeq.Add(cCmd);

-    }

-    else if (cmd is CommentCmd) {

-      // skip

-    }

-    else if (cmd is StateCmd) {

-      var sCmd = (StateCmd)cmd;

-      var newCmdSeq = new CmdSeq();

-      foreach (Cmd c in sCmd.Cmds)

-        PredicateCmd(newCmdSeq, c);

-      sCmd.Cmds = newCmdSeq;

-      cmdSeq.Add(sCmd);

-    }

-    else {

-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

-    }

-  }

-

-  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {

-    if (cmd is GotoCmd) {

-      var gCmd = (GotoCmd)cmd;

-      var targets = new List<Expr>(

-        gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));

-      if (targets.Count == 1) {

-        PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));

-      } else {

-        PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,

-                                          new IdentifierExprSeq(cur)));

-        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 {

-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

-    }

-  }

-

-  void PredicateImplementation() {

-    blockGraph = prog.ProcessLoops(impl);

-    var sortedBlocks = blockGraph.LoopyTopSort();

-

-    int blockId = 0;

-    foreach (var block in impl.Blocks)

-      blockIds[block] = Expr.Literal(blockId++);

-    returnBlockId = Expr.Literal(blockId++);

-

-    curVar = new LocalVariable(Token.NoToken,

-                               new TypedIdent(Token.NoToken, "cur",

-                                              Microsoft.Boogie.Type.Int));

-    impl.LocVars.Add(curVar);

-    cur = Expr.Ident(curVar);

-

-    pVar = new LocalVariable(Token.NoToken,

-                             new TypedIdent(Token.NoToken, "p",

-                                            Microsoft.Boogie.Type.Bool));

-    impl.LocVars.Add(pVar);

-    p = Expr.Ident(pVar);

-

-    if (useProcedurePredicates)

-      fp = Expr.Ident(impl.InParams[0]);

-

-    var newBlocks = new List<Block>();

-

-    Block entryBlock = new Block();

-    entryBlock.Label = "entry";

-    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,

-                        CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],

-                                           returnBlockId)));

-    newBlocks.Add(entryBlock);

-

-    var prevBlock = entryBlock;

-    foreach (var n in sortedBlocks) {

-      if (n.Item2) {

-        var backedgeBlock = new Block();

-        newBlocks.Add(backedgeBlock);

-

-        backedgeBlock.Label = n.Item1.Label + ".backedge";

-        backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

-          Expr.Eq(cur, blockIds[n.Item1]),

-          new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));

-        backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                                new BlockSeq(n.Item1));

-

-        var tailBlock = new Block();

-        newBlocks.Add(tailBlock);

-

-        tailBlock.Label = n.Item1.Label + ".tail";

-        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

-                                             Expr.Neq(cur, blockIds[n.Item1])));

-

-        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                        new BlockSeq(backedgeBlock, tailBlock));

-        prevBlock = tailBlock;

-      } else {

-        var runBlock = n.Item1;

-        var oldCmdSeq = runBlock.Cmds;

-        runBlock.Cmds = new CmdSeq();

-        newBlocks.Add(runBlock);

-        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                            new BlockSeq(runBlock));

-

-        pExpr = Expr.Eq(cur, blockIds[runBlock]);

-        if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {

-          AddUniformCandidateInvariant(runBlock.Cmds, runBlock);

-          AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);

-        }

-        runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));

-        var transferCmd = runBlock.TransferCmd;

-        foreach (Cmd cmd in oldCmdSeq)

-          PredicateCmd(newBlocks, runBlock, cmd, out runBlock);

-        PredicateTransferCmd(runBlock.Cmds, transferCmd);

-

-        prevBlock = runBlock;

-        doneBlocks.Add(runBlock);

-      }

-    }

-

-    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);

-    impl.Blocks = newBlocks;

-  }

-

-  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {

-    if (useProcedurePredicates) {

-      return new NAryExpr(Token.NoToken,

-                 new IfThenElse(Token.NoToken),

-                 new ExprSeq(fp, then, eElse));

-    } else {

-      return then;

-    }

-  }

-

-  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {

-    cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,

-               CreateIfFPThenElse(blockIds[header], returnBlockId)),

-             "uniform loop"));

-  }

-

-  private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {

-    var loopNodes = new HashSet<Block>();

-    foreach (var b in blockGraph.BackEdgeNodes(header))

-      loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));

-    var exits = new HashSet<Expr>();

-    foreach (var ln in loopNodes) {

-      if (ln.TransferCmd is GotoCmd) {

-        var gCmd = (GotoCmd) ln.TransferCmd;

-        foreach (var exit in gCmd.labelTargets.Cast<Block>()

-                                 .Where(b => !loopNodes.Contains(b)))

-          exits.Add(blockIds[exit]);

-      }

-      if (ln.TransferCmd is ReturnCmd)

-        exits.Add(returnBlockId);

-    }

-    var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),

-                                            (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));

-    cs.Add(prog.CreateCandidateInvariant(

-             CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),

-             "non-uniform loop"));

-  }

-

-  public static void Predicate(Program p,

-                               bool createCandidateInvariants = true,

-                               bool useProcedurePredicates = true) {

-    foreach (var decl in p.TopLevelDeclarations.ToList()) {

-      if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {

-        var dwf = (DeclWithFormals)decl;

-        var fpVar = new Formal(Token.NoToken,

-                               new TypedIdent(Token.NoToken, "_P",

-                                              Microsoft.Boogie.Type.Bool),

-                               /*incoming=*/true);

-        dwf.InParams = new VariableSeq(

-          (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

-            .ToArray());

-

-        if (dwf is Procedure)

-        {

-            var proc = (Procedure)dwf;

-            var newRequires = new RequiresSeq();

-            foreach (Requires r in proc.Requires)

-            {

-                newRequires.Add(new Requires(r.Free,

-                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));

-            }

-            var newEnsures = new EnsuresSeq();

-            foreach (Ensures e in proc.Ensures)

-            {

-                newEnsures.Add(new Ensures(e.Free,

-                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));

-            }

-        }

-

-      }

-

-      try {

-        var impl = decl as Implementation;

-        if (impl != null)

-          new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();

-      }

-      catch (Program.IrreducibleLoopException) { }

-    }

-  }

-

-  public static void Predicate(Program p, Implementation impl) {

-    try {

-      new BlockPredicator(p, impl, false, false).PredicateImplementation();

-    }

-    catch (Program.IrreducibleLoopException) { }

-  }

-

-}

-

-

-class EnabledReplacementVisitor : StandardVisitor

-{

-    private Expr pExpr;

-

-    internal EnabledReplacementVisitor(Expr pExpr)

-    {

-        this.pExpr = pExpr;

-    }

-

-    public override Expr VisitExpr(Expr node)

-    {

-        if (node is IdentifierExpr)

-        {

-            IdentifierExpr iExpr = node as IdentifierExpr;

-            if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))

-            {

-                return pExpr;

-            }

-        }

-        return base.VisitExpr(node);

-    }

-}

-

-}

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ca0c0e59..795fc9ca 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -10,7 +10,7 @@ using System.Diagnostics;
 using System.Threading;

 using System.IO;

 using Microsoft.Boogie;

-using Graphing;

+using Microsoft.Boogie.GraphUtil;

 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
deleted file mode 100644
index d7e297cd..00000000
--- a/Source/VCGeneration/DoomCheck.cs
+++ /dev/null
@@ -1,401 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    internal class Evc {

-        

-        public DoomErrorHandler ErrorHandler {

-            set {

-                m_ErrorHandler = value;

-            }

-        }

-        

-      [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(m_Checker!=null);

-}

-

-        private Checker m_Checker;

-        private DoomErrorHandler m_ErrorHandler;

-        

-        [NotDelayed]

-        public Evc(Checker check) {

-          Contract.Requires(check != null);

-            m_Checker = check;

-                   

-        }

-        

-        public void Initialize(VCExpr evc) {

-          Contract.Requires(evc != null);

-            m_Checker.PushVCExpr(evc);

-        }

-        

-    

-        public bool CheckReachvar(List<Variable> lv,Dictionary<Expr, int> finalreachvars, 

-            int k, int l, bool usenew , out ProverInterface.Outcome outcome) {

-          Contract.Requires(lv != null);

-

-          VCExpr vc = VCExpressionGenerator.False;

-          if (usenew )

-          {

-              foreach (Variable v in lv)

-              {

-

-                  vc = m_Checker.VCExprGen.Or(

-                      m_Checker.VCExprGen.Neq(

-                          m_Checker.VCExprGen.Integer(BigNum.ZERO),

-                          m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)),

-                      vc);

-              }

-              //Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count);

-

-              VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO); // Ask: is the necessary or can we use the same instance term in two inequalities?

-              VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO);

-

-                  foreach (KeyValuePair<Expr, int> kvp in finalreachvars)

-                  {

-

-                      vc21 = m_Checker.VCExprGen.Add(vc21, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key));

-                      vc22 = m_Checker.VCExprGen.Add(vc22, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key));

-                  }                  

-

-              VCExpr post = m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21);

-

-              if (k != -1)

-              {

-                  post = m_Checker.VCExprGen.Or(

-                        post, m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k)))

-                        );

-              }

-              vc = (m_Checker.VCExprGen.Or(vc, (post) ));

-

-          }

-          else

-          {

-              

-              foreach (Variable v in lv)

-              {

-

-                  vc = m_Checker.VCExprGen.Or(

-                      m_Checker.VCExprGen.Eq(

-                          m_Checker.VCExprGen.Integer(BigNum.ONE),

-                          m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)),

-                      vc);

-              }

-              Contract.Assert(vc != null);

-

-              // Add the desired outcome of the reachability variables

-              foreach (KeyValuePair<Expr, int> kvp in finalreachvars)

-              {

-                  vc = m_Checker.VCExprGen.Or(

-                      m_Checker.VCExprGen.Neq(

-                          m_Checker.VCExprGen.Integer(BigNum.FromInt(kvp.Value)),

-                          m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)),

-                      vc);

-              }

-

-          }

-

-            // Todo: Check if vc is trivial true or false            

-            outcome = ProverInterface.Outcome.Undetermined;

-            Contract.Assert( m_ErrorHandler !=null);

-            m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);

-            m_Checker.ProverDone.WaitOne();

-            

-            try {

-              outcome = m_Checker.ReadOutcome();

-            } catch (UnexpectedProverOutputException e)

-            {

-              if (CommandLineOptions.Clo.TraceVerify) { 

-                Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);

-                Console.WriteLine(e.ToString());

-              }

-              return false;

-            }                        

-            return true;

-        }

-    }

-

-    internal class DoomCheck {

-        

-      [ContractInvariantMethod]

-        void ObjectInvariant() 

-        {

-            Contract.Invariant(Label2Absy!=null);

-            Contract.Invariant(m_Check != null);

-            Contract.Invariant(m_Evc != null);

-            Contract.Invariant(m_Order != null);

-        }

-

-        #region Attributes

-        public Hashtable Label2Absy;

-        public DoomErrorHandler ErrorHandler {

-            set {

-                m_ErrHandler = value;

-                m_Evc.ErrorHandler = value;

-            }

-            

-            get {

-                return m_ErrHandler;

-            }

-        }

-        

-        private DoomErrorHandler m_ErrHandler;

-        private Checker m_Check;

-        private DoomDetectionStrategy m_Order;

-        private Evc m_Evc;

-        #endregion

-        

-        public void __DEBUG_PrintStatistics()

-        {

-            Console.WriteLine("Checked/Total: Bl {0} / {1} EQ {2} / {3} {4} Tr {5} {6} / {7}", m_Order.__DEBUG_BlocksChecked, m_Order.__DEBUG_BlocksTotal, m_Order.__DEBUG_EQCChecked, m_Order.__DEBUG_EQCTotal, m_Order.__DEBUG_EQCLeaf,  m_Order.__DEBUG_TracesChecked, m_Order.__DEBUG_InfeasibleTraces, m_Order.__DEBUG_TracesTotal);

-        }

-

-        [NotDelayed]

-        public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable, out int assertionCount) {

-          Contract.Requires(passive_impl != null);

-          Contract.Requires(check != null);

-          Contract.Requires(uncheckable != null);

-            m_Check = check;            

-

-            int replaceThisByCmdLineOption = CommandLineOptions.Clo.DoomStrategy ;

-            if (CommandLineOptions.Clo.DoomStrategy!=-1) Console.Write("Running experiments using {0} /", replaceThisByCmdLineOption);

-            switch (replaceThisByCmdLineOption)

-            {

-                default:

-                    {

-                        if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover specialK Strategy");

-                        m_Order = new PathCoverStrategyK(passive_impl, unifiedExit, uncheckable);

-                        break;

-                    }

-                case 1:

-                    {

-                        if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover L Strategy");

-                        m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable);

-                        break;

-                    }

-                case 2:

-                    {

-                        if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse strategy");

-                        m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable);

-

-                        break;

-                    }

-                case 3:

-                    {

-                        if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse+ce strategy");

-                        m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable);

-                        break;

-                    }

-                case 4:

-                    {

-                        if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("no strategy");

-                        m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable);

-                        break;

-                    }

-                    

-            }

-

-            Label2Absy = new Hashtable(); // This is only a dummy

-            m_Evc = new Evc(check);

-            Hashtable l2a = null;

-            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);

-            Contract.Assert(vce != null);

-            Contract.Assert( l2a!=null);

-            Label2Absy = l2a;

-          

-            m_Evc.Initialize(vce);

-        }

-

-

-        public void RespawnChecker(Implementation passive_impl, Checker check)

-        {

-            Contract.Requires(check != null);

-            m_Check = check;

-            Label2Absy = new Hashtable(); // This is only a dummy

-            m_Evc = new Evc(check);

-            Hashtable l2a = null;

-            int assertionCount;  // compute and then ignore

-            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);

-            Contract.Assert(vce != null);

-            Contract.Assert(l2a != null);

-            Label2Absy = l2a;

-

-            m_Evc.Initialize(vce);            

-        }

-

-        /* - Set b to the next block that needs to be checked.

-           - Returns false and set b to null if all blocks are checked.           

-           - Has to be alternated with CheckLabel; might crash otherwise

-        */

-        public bool GetNextBlock(out List<Block> lb)

-        {

-            return m_Order.GetNextBlock(out lb);

-        }

-

-        public Stopwatch DEBUG_ProverTime = new Stopwatch();

-

-        /*  - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds.            

-            - outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed.            

-            - returns false if the theorem prover throws an exception, otherwise true.            

-        */

-        public bool CheckLabel(List<Variable> lv,Dictionary<Expr, int> finalreachvars, out ProverInterface.Outcome outcome) {

-           Contract.Requires(lv != null);

-            outcome = ProverInterface.Outcome.Undetermined;

-            DEBUG_ProverTime.Reset();

-            DEBUG_ProverTime.Start();

-            if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck,  out outcome) ) {

-                DEBUG_ProverTime.Stop();

-                if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) {

-                    outcome = ProverInterface.Outcome.Undetermined;

-                }

-                return true;

-            } else {

-                DEBUG_ProverTime.Stop();

-                Console.WriteLine(outcome);

-                m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler);

-                return false;

-            }

-        }

-

-        public List<List<Block/*!>!>!*/>> DoomedSequences { 

-            get {

-              Contract.Ensures(Contract.ForAll(Contract.Result<List<List<Block>>>(), i=> cce.NonNullElements(i)));

-

-                return m_Order.DetectedBlock;

-            }

-        }

-

-

-        #region Error Verification Condition Generation

-       /*

-                   #region _TESTING_NEW_STUFF_

-            CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;

-            //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true

-            

-            CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;

-            #endregion

-

-       */

-

-        VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {

-          Contract.Requires(impl != null);

-          Contract.Requires(ch != null);

-          Contract.Ensures(Contract.Result<VCExpr>() != null);

-

-          TypecheckingContext tc = new TypecheckingContext(null);

-          impl.Typecheck(tc);

-          label2absy = new Hashtable/*<int, Absy!>*/();

-          VCExpr vc;

-          switch (CommandLineOptions.Clo.vcVariety) {

-            case CommandLineOptions.VCVariety.Doomed:

-              vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount);

-              break;

-

-            default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected enumeration value

-          }

-          return vc;

-        }

-

-        public VCExpr LetVC(Block startBlock,

-                            Hashtable/*<int, Absy!>*/ label2absy,

-                            ProverContext proverCtxt,

-                            out int assertionCount)

-        {

-          Contract.Requires(startBlock != null);

-          Contract.Requires(label2absy != null);

-          Contract.Requires(proverCtxt != null);

-          Contract.Ensures(Contract.Result<VCExpr>() != null);

-

-          Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

-          List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-          VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount);

-          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-            return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );

-          } else {

-            return proverCtxt.ExprGen.Let(bindings, startCorrect );

-          }

-        }

-

-        VCExpr LetVC(Block block,

-                     Hashtable/*<int, Absy!>*/ label2absy,

-                     Hashtable/*<Block, VCExprVar!>*/ blockVariables,

-                     List<VCExprLetBinding> bindings,

-                     ProverContext proverCtxt,

-                     out int assertionCount)

-        {

-          Contract.Requires(label2absy != null);

-          Contract.Requires(blockVariables != null);

-          Contract.Requires(proverCtxt != null);

-          Contract.Requires(cce.NonNullElements(bindings));

-          Contract.Ensures(Contract.Result<VCExpr>() != null);

-

-          assertionCount = 0;

-          VCExpressionGenerator gen = proverCtxt.ExprGen;

-          Contract.Assert(gen != null);

-          VCExprVar v = (VCExprVar)blockVariables[block];

-          if (v == null) {

-            /*

-             * For block A (= block), generate:

-             *   LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct))

-             * with the side effect of adding the let bindings to "bindings" for any

-             * successor not yet visited.

-             */

-            VCExpr SuccCorrect;

-            GotoCmd gotocmd = block.TransferCmd as GotoCmd;

-            if (gotocmd == null) {

-                if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-                    SuccCorrect = VCExpressionGenerator.False;

-                } else {

-                    SuccCorrect = VCExpressionGenerator.True;

-                }

-            } else {

-              Contract.Assert( gotocmd.labelTargets != null);

-              List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

-              foreach (Block successor in gotocmd.labelTargets) {

-                Contract.Assert(successor != null);

-                int ac;

-                VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac);

-                assertionCount += ac;

-                SuccCorrectVars.Add(s);

-              }

-              SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

-            }

-

-            VCContext context = new VCContext(label2absy, proverCtxt);

-            //        m_Context = context;

-

-            VCExpr vc = Wlp.Block(block, SuccCorrect, context);

-            assertionCount += context.AssertionCount;

-            v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);

-            

-            bindings.Add(gen.LetBinding(v, vc));

-            blockVariables.Add(block, v);

-          }

-          return v;

-        }

-

-        

-        #endregion 

-                       

-    }

-

-}

diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
deleted file mode 100644
index 5f00a3cf..00000000
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ /dev/null
@@ -1,86 +0,0 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    internal class DoomErrorHandler : ProverInterface.ErrorHandler

-    {

-

-        protected Hashtable label2Absy;

-        protected VerifierCallback callback;

-        private List<Block> m_CurrentTrace = new List<Block>();

-

-        [ContractInvariantMethod]

-        void ObjectInvariant()

-        {

-            Contract.Invariant(label2Absy != null);

-            Contract.Invariant(callback != null);

-            Contract.Invariant(cce.NonNullElements(m_CurrentTrace));

-        }

-

-

-        public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback)

-        {

-            Contract.Requires(label2Absy != null);

-            Contract.Requires(callback != null);

-            this.label2Absy = label2Absy;

-            this.callback = callback;

-        }

-

-        public override Absy Label2Absy(string label)

-        {

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

-            Contract.Ensures(Contract.Result<Absy>() != null);

-

-            int id = int.Parse(label);

-            return cce.NonNull((Absy)label2Absy[id]);

-        }

-

-        public override void OnProverWarning(string msg)

-        {

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

-            this.callback.OnWarning(msg);

-        }

-

-

-        public List<Block>/*!>!*/ TraceNodes

-        {

-            get

-            {

-                Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

-

-                return m_CurrentTrace;

-            }

-        }

-

-        public override void OnModel(IList<string>/*!>!*/ labels, Model model)

-        {

-            // TODO: it would be better to check which reachability variables are actually set to one!

-            List<Block> traceNodes = new List<Block>();

-            List<AssertCmd> assertNodes = new List<AssertCmd>();            

-            foreach (string s in labels)

-            {

-                Contract.Assert(s != null);

-                Absy node = Label2Absy(s);

-                if (node is Block)

-                {

-                    Block b = (Block)node;

-                    traceNodes.Add(b);

-                    //Console.Write("{0}, ", b.Label);

-                }

-            }

-            m_CurrentTrace.AddRange(traceNodes);

-        }

-

-    }

-

-}
\ No newline at end of file
diff --git a/Source/VCGeneration/DoomedLoopUnrolling.cs b/Source/VCGeneration/DoomedLoopUnrolling.cs
deleted file mode 100644
index 5469a1db..00000000
--- a/Source/VCGeneration/DoomedLoopUnrolling.cs
+++ /dev/null
@@ -1,650 +0,0 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    #region Loop handeling for doomed code detection

-

-    #region Loop Remover

-    internal class LoopRemover

-    {        

-        GraphAnalyzer m_GraphAnalyzer;

-

-        public LoopRemover(GraphAnalyzer ga)

-        {

-            m_GraphAnalyzer = ga;

-        }

-

-         private void m_RemoveBackEdge(Loop l)

-        {

-            // first remove the backedges of the nested loops

-            foreach (Loop c in l.NestedLoops) m_RemoveBackEdge(c);

-            //Debugger.Break();

-            GraphNode loopSkip = null;

-            foreach (GraphNode gn in l.Cutpoint.Suc)

-            {

-                if (l.LoopExitNodes.Contains(gn))

-                {

-                    loopSkip = gn; break;

-                }

-            }

-            if (loopSkip == null)

-            { // We didn't find a loop exit node. There must be a bug

-                Debugger.Break();

-            }

-            foreach (GraphNode gn in l.Cutpoint.LoopingPred)

-            {

-                List<GraphNode> newsuc = new List<GraphNode>();

-                foreach (GraphNode s in gn.Suc)

-                {

-                    if (s == l.Cutpoint) newsuc.Add(loopSkip);

-                    else newsuc.Add(s);

-                }

-                gn.Suc = newsuc;

-            }

-        }

-

-        private void m_AbstractLoop(Loop l)

-        {

-            foreach (Loop c in l.NestedLoops) m_AbstractLoop(c);

-            m_HavocLoopBody(l);

-            m_RemoveBackEdge(l);        

-        }

-

-        public void AbstractLoopUnrolling()

-        {

-            foreach (Loop l in m_GraphAnalyzer.Graphloops)

-            {

-                m_MarkLoopExitUncheckable(l);

-                m_AbstractLoopUnrolling(l,null, "",true);                

-            }

-        }

-

-        private void m_HavocLoopBody(Loop l)

-        {

-            List<Block> loopblocks = new List<Block>();

-            foreach (GraphNode g in l.LoopNodes) loopblocks.Add(g.Label);

-            HavocCmd hcmd = m_ComputHavocCmd(loopblocks, l.Cutpoint.Label.tok);

-

-            //Add Havoc before and after the loop body

-            foreach (GraphNode g in l.Cutpoint.Suc) // before

-            {

-                if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd);                

-            }

-            foreach (GraphNode g in l.Cutpoint.Pre) // and after

-            {

-                if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd);                

-            }        

-        }

-

-        private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd)

-        {

-            CmdSeq cs = new CmdSeq();

-            cs.Add(hcmd); cs.AddRange(b.Cmds);

-            b.Cmds = cs;

-        }

-

-        private HavocCmd m_ComputHavocCmd(List<Block> bl, IToken tok)

-        {

-            Contract.Requires(bl != null);

-            Contract.Requires(tok != null);

-            Contract.Ensures(Contract.Result<HavocCmd>() != null);

-

-            VariableSeq varsToHavoc = new VariableSeq();

-            foreach (Block b in bl)

-            {

-                Contract.Assert(b != null);

-                foreach (Cmd c in b.Cmds)

-                {

-                    Contract.Assert(c != null);

-                    c.AddAssignedVariables(varsToHavoc);

-                }

-            }

-            IdentifierExprSeq havocExprs = new IdentifierExprSeq();

-            foreach (Variable v in varsToHavoc)

-            {

-                Contract.Assert(v != null);

-                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                if (!havocExprs.Has(ie))

-                    havocExprs.Add(ie);

-            }

-            // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct

-            // the source location for this later on

-            return new HavocCmd(tok, havocExprs);

-        }

-

-        private void m_AbstractLoopUnrolling(Loop l, Loop parent, string prefix, bool unfold)

-        {            

-            //Debugger.Break();

-            if (unfold)

-            {

-

-                Loop first = new Loop(l, m_GraphAnalyzer,prefix+"FI_");

-                Loop last = new Loop(l, m_GraphAnalyzer,prefix+"LA_");

-                Loop abs = new Loop(l, m_GraphAnalyzer, prefix + "AB_");

-                foreach (Loop c in first.NestedLoops) m_AbstractLoopUnrolling(c, first, prefix + "FI_", false);

-                foreach (Loop c in last.NestedLoops)  m_AbstractLoopUnrolling(c, last, prefix + "LA_", false);

-                foreach (Loop c in abs.NestedLoops)   m_AbstractLoopUnrolling(c, abs, prefix + "AB_", true);

-

-                //Debugger.Break();

-

-                if (parent != null)

-                {

-                    foreach (GraphNode gn in l.LoopNodes)

-                    {

-                        if (parent.LoopNodes.Contains(gn)) parent.LoopNodes.Remove(gn);

-                    }

-                    foreach (GraphNode gn in abs.LoopNodes)

-                    {

-                        if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);

-                    }

-                    foreach (GraphNode gn in first.LoopNodes)

-                    {

-                        if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);

-                    }

-                    foreach (GraphNode gn in last.LoopNodes)

-                    {

-                        if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);

-                    }

-                }

-                

-                m_HavocLoopBody(abs);

-                List<GraphNode> backupPre = new List<GraphNode>();

-                backupPre.AddRange(l.Cutpoint.Pre);

-                foreach (GraphNode pre in backupPre)

-                {

-                    if (!l.Cutpoint.LoopingPred.Contains(pre))

-                    {

-                        pre.RemoveEdgeTo(l.Cutpoint);

-                        pre.RemoveEdgeTo(abs.Cutpoint);

-                        pre.AddEdgeTo(first.Cutpoint);

-                    }

-                }

-

-                m_RemoveRegularLoopExit(last);

-                m_RemoveRegularLoopExit(abs);

-

-                m_ReplaceBackEdge(first, abs.Cutpoint);

-                m_ReplaceBackEdge(abs, last.Cutpoint);

-                foreach (GraphNode gn in first.Cutpoint.Suc)

-                {

-                    if (!first.LoopNodes.Contains(gn))

-                    {

-                        m_ReplaceBackEdge(last, gn);

-                        break;

-                    }

-                }

-

-                // Remove all remaining connections to the original loop

-                foreach (GraphNode gn in l.LoopExitNodes)

-                {

-                    List<GraphNode> tmp = new List<GraphNode>();

-                    tmp.AddRange(gn.Pre);

-                    foreach (GraphNode g in tmp)

-                    {

-                        if (l.LoopNodes.Contains(g))

-                        {

-                            //Debugger.Break();

-                            g.RemoveEdgeTo(gn);

-                        }

-                    }

-                }

-                foreach (GraphNode gn in l.LoopNodes)

-                {

-                    m_GraphAnalyzer.DeleteGraphNode(gn);

-                }

-                foreach (GraphNode gn in first.LoopNodes)

-                {

-                    if (gn != first.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn) ) 

-                        m_GraphAnalyzer.UncheckableNodes.Add(gn);

-                }

-                foreach (GraphNode gn in last.LoopNodes)

-                {

-                    if (gn != last.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn))

-                        m_GraphAnalyzer.UncheckableNodes.Add(gn);

-                }

-                MakeLoopExitUncheckable(last.LoopExitNodes);

-            }

-            else

-            {

-                foreach (Loop c in l.NestedLoops) m_AbstractLoopUnrolling(c, l, prefix, false);

-                m_AbstractLoop(l);

-                //MakeLoopExitUncheckable(l.LoopExitNodes);                

-            }            

-        }

-

-        // the loop exit has to be marked uncheckable because otherwise

-        // while(true) would report unreachable code.

-        private void m_MarkLoopExitUncheckable(Loop l)

-        {

-            

-            foreach (GraphNode g in l.Cutpoint.Suc)

-            {

-                if (!l.LoopNodes.Contains(g))

-                {                    

-                    foreach (GraphNode g_ in m_MarkLoopExitUncheckable(g, l))

-                    {

-                        if (!m_GraphAnalyzer.UncheckableNodes.Contains(g_))

-                            m_GraphAnalyzer.UncheckableNodes.Add(g_);

-                    }

-                }

-            }

-        }

-

-        private List<GraphNode> m_MarkLoopExitUncheckable(GraphNode g, Loop l)

-        {

-            List<GraphNode> ret = new List<GraphNode>();

-

-            if (g.Pre.Count > 1) return ret;

-            ret.Add(g);

-            foreach (GraphNode gn in g.Suc)

-            {

-                ret.AddRange(m_MarkLoopExitUncheckable(gn, l));

-            }

-

-            return ret;

-        }

-

-        // to avoid problems with unreachable code after while(true) {}, try to make the loopexit nodes uncheckable.

-        private void MakeLoopExitUncheckable(List<GraphNode> le)

-        { 

-            foreach (GraphNode gn in le) 

-            {

-                if (gn.Suc.Count==1)  m_GraphAnalyzer.UncheckableNodes.Add(gn);

-            }

-        }

-

-        private void m_RemoveRegularLoopExit(Loop l)

-        {

-            List<GraphNode> lg = new List<GraphNode>();

-            lg.AddRange( l.Cutpoint.Suc );

-            foreach (GraphNode gn in lg)

-            {

-                if (l.LoopExitNodes.Contains(gn))

-                {

-                    l.Cutpoint.RemoveEdgeTo(gn);

-                    l.LoopExitNodes.Remove(gn);

-                }

-            }

-        }

-

-        private void m_ReplaceBackEdge(Loop l, GraphNode loopSkip)

-        {

-

-            foreach (GraphNode gn in l.Cutpoint.LoopingPred)

-            {

-                List<GraphNode> newsuc = new List<GraphNode>();

-                foreach (GraphNode s in gn.Suc)

-                {

-                    if (s == l.Cutpoint) newsuc.Add(loopSkip);

-                    else newsuc.Add(s);

-                }

-                gn.Suc = newsuc;

-            }

-        }

-

-

-    }

-    #endregion

-

-    #region Graph Analyzer

-    internal class GraphAnalyzer

-    {

-        public List<GraphNode> UncheckableNodes = new List<GraphNode>();

-

-        public Dictionary<Block, GraphNode> GraphMap = new Dictionary<Block, GraphNode>();

-

-        public List<Loop> Graphloops = null;

-

-        public GraphAnalyzer(List<Block> blocks)

-        {

-            //ExitBlock = dedicatedExitBlock;

-            if (blocks.Count < 1) return;

-            foreach (Block b in blocks) GraphMap[b] = new GraphNode(b);

-            foreach (Block b in blocks)

-            {

-                foreach (Block pre in b.Predecessors) GraphMap[b].Pre.Add(GraphMap[pre]);

-                GotoCmd gc = b.TransferCmd as GotoCmd;

-                if (gc != null)

-                {

-                    foreach (Block suc in gc.labelTargets) GraphMap[b].Suc.Add(GraphMap[suc]);

-                }

-            }

-

-            

-            m_DetectCutPoints(GraphMap[blocks[0]]);

-            

-            //m_DetectCutPoints(GraphMap[blocks[0]], null, new List<GraphNode>());  

-            Graphloops = m_CollectLoops(GraphMap[blocks[0]], null);

-            

-        }

-

-        public List<Block> ToImplementation(out List<Block> uncheckables)

-        {

-            List<Block> blocks = new List<Block>();

-            uncheckables = new List<Block>();

-

-            foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap)

-            {

-                Block b = kvp.Key;

-                if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b);

-                blocks.Add(b);

-                b.Predecessors = new BlockSeq();

-                foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);

-                if (kvp.Value.Suc.Count > 0)

-                {

-                    BlockSeq bs = new BlockSeq();                    

-                    foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label);                    

-                    b.TransferCmd = new GotoCmd(b.tok, bs);

-                }

-                else

-                {

-                    b.TransferCmd = new ReturnCmd(b.tok);

-                }

-            }

-

-            return blocks;

-        }

-

-        public GraphNode CloneGraphNode(GraphNode gn, string prefix)

-        {

-            CmdSeq cmds = new CmdSeq(gn.Label.Cmds);

-

-            Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd);

-            GraphNode clone = new GraphNode(b);

-            clone.IsCutpoint = gn.IsCutpoint;

-            clone.Suc.AddRange(gn.Suc);

-            clone.Pre.AddRange(gn.Pre);

-            clone.LoopingPred.AddRange(gn.LoopingPred);

-            GraphMap[b] = clone;

-            //if (gn.Label == ExitBlock) ExitBlock = b;

-            return clone;

-        }

-

-        public void DeleteGraphNode(GraphNode gn)

-        {

-            List<Block> affected = new List<Block>();

-                        

-            foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap)

-            {

-                if (kvp.Value == gn && !affected.Contains(kvp.Key)) affected.Add(kvp.Key);

-            }

-            foreach (Block b in affected)

-            {

-                GraphMap.Remove(b);

-            }

-        }

-/*

-        private void m_DetectCutPoints(GraphNode gn, GraphNode pred, List<GraphNode> visited )

-        {

-            if (visited.Contains(gn) )

-            {

-                if (pred != null && !gn.LoopingPred.Contains(pred)) gn.LoopingPred.Add(pred);

-                gn.IsCutpoint = true;

-                Console.WriteLine("Normal RootNode {0}", gn.Label.Label);

-                return;

-            }

-            else

-            {

-                List<GraphNode> visited_ = new List<GraphNode>();

-                visited_.AddRange(visited);

-                visited_.Add(gn);

-                foreach (GraphNode next in gn.Suc)

-                {

-                    m_DetectCutPoints(next,gn,visited_);

-                }

-            }

-

-        }

-*/

-

-

-        private void m_DetectCutPoints(GraphNode gn)

-        {

-            List<GraphNode> todo = new List<GraphNode>();

-            List<GraphNode> done = new List<GraphNode>();

-            todo.Add(gn);

-

-            GraphNode current = null;

-            todo[0].Index = 0;

-

-            while (todo.Count > 0)

-            {

-                current = todo[0];

-                todo.Remove(current);

-

-                bool ready = true;

-                foreach (GraphNode p in current.Pre)

-                {                    

-                    if (!done.Contains(p) )

-                    {

-                        _loopbacktracking.Clear();

-                        if (!m_isLoop(current, p, todo, done))

-                        {

-                            todo.Add(current);

-                            ready = false;

-                            break;

-                        }

-                        else

-                        {

-                            if (!current.LoopingPred.Contains(p)) current.LoopingPred.Add(p);

-                            current.IsCutpoint = true;

-                        }

-                    } 

-                }

-                if (!ready) continue;

-                done.Add(current);

-                foreach (GraphNode s in current.Suc)

-                {

-                    if (!todo.Contains(s) && !done.Contains(s)) todo.Add(s);

-                }

-            }

-

-        }

-

-        List<GraphNode> _loopbacktracking = new List<GraphNode>();

-        private bool m_isLoop(GraphNode loophead, GraphNode gn, List<GraphNode> l1, List<GraphNode> l2)

-        {

-            if (loophead == gn) return true;

-            if (l1.Contains(gn) || l2.Contains(gn) || _loopbacktracking.Contains(gn)) return false;

-            _loopbacktracking.Add(gn);

-            foreach (GraphNode p in gn.Pre)

-            {

-                if (m_isLoop(loophead, p, l1, l2)) return true;

-            }

-            return false;

-        }

-

-        private List<Loop> m_CollectLoops(GraphNode gn, Loop lastLoop)

-        {

-            List<Loop> ret = new List<Loop>();

-            if (gn.Visited) return ret;

-            gn.Visited = true;

-            List<GraphNode> loopingSucs = new List<GraphNode>();

-            if (gn.IsCutpoint)

-            {                

-                Loop l = new Loop(gn);

-                if (lastLoop != null)

-                {

-                    lastLoop.SucLoops.Add(l);

-                    l.PreLoops.Add(lastLoop);

-                }

-                loopingSucs = l.LoopNodes;

-                lastLoop = l;

-                ret.Add(lastLoop);

-            }

-            foreach (GraphNode suc in gn.Suc)

-            {

-                if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop));                

-            }

-            //Debugger.Break();

-            return ret;

-        }

-    }

-    #endregion

-

-    #region GraphNodeStructure

-    internal class GraphNode

-    {

-        public int Index = -1; // Used for scc detection

-        public int LowLink = -1;  // Used for scc detection

-

-        public GraphNode(Block b)

-        {

-            Label = b; IsCutpoint = false;

-        }

-        public Block Label;

-        public List<GraphNode> Pre = new List<GraphNode>();

-        public List<GraphNode> Suc = new List<GraphNode>();

-        public bool IsCutpoint;

-        public bool Visited = false;

-        public List<GraphNode> LoopingPred = new List<GraphNode>();

-

-        public void AddEdgeTo(GraphNode other)

-        {

-            if (!this.Suc.Contains(other)) this.Suc.Add(other);

-            if (!other.Pre.Contains(this)) other.Pre.Add(this);

-        }

-

-        public void RemoveEdgeTo(GraphNode other)

-        {

-            if (this.Suc.Contains(other)) this.Suc.Remove(other);

-            if (other.Pre.Contains(this)) other.Pre.Remove(this);         

-        }

-

-    }

-    #endregion

-

-    #region LoopStructure

-    internal class Loop

-    {

-        public Loop(GraphNode cutpoint)

-        {

-            if (!cutpoint.IsCutpoint)

-            {

-                Debugger.Break();

-            }

-            Cutpoint = cutpoint;

-            LoopNodes.Add(Cutpoint);

-            foreach (GraphNode gn in Cutpoint.LoopingPred)

-            {

-                CollectLoopBody(gn);

-            }

-            CollectLoopExitNodes();

-        }

-

-        // Copy Constructor

-        public Loop(Loop l, GraphAnalyzer ga, string prefix)

-        {

-            

-            Dictionary<GraphNode, GraphNode> clonemap = new Dictionary<GraphNode, GraphNode>();

-            GraphNode clonecutpoint = null;

-            foreach (GraphNode gn in l.LoopNodes)

-            {

-                clonemap[gn] = ga.CloneGraphNode(gn, prefix);

-                if (gn == l.Cutpoint) clonecutpoint = clonemap[gn];

-            }

-

-            if (clonecutpoint == null)

-            {

-                Debugger.Break();

-                return;

-            }

-            // Replace the pre and post nodes by the corresponding clone

-            foreach (GraphNode gn in l.LoopNodes)

-            {

-                List<GraphNode> newl = new List<GraphNode>();

-                foreach (GraphNode g in clonemap[gn].Pre)

-                {

-                    if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);

-                    else newl.Add(g);

-                }

-                clonemap[gn].Pre = newl;

-                newl = new List<GraphNode>();

-                foreach (GraphNode g in clonemap[gn].Suc)

-                {

-                    if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);

-                    else newl.Add(g);

-                }

-                clonemap[gn].Suc = newl;

-                newl = new List<GraphNode>();

-                foreach (GraphNode g in clonemap[gn].LoopingPred)

-                {

-                    if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);

-                    else newl.Add(g);

-                }

-                clonemap[gn].LoopingPred = newl;

-            }

-

-            foreach (GraphNode gn in l.Cutpoint.LoopingPred)

-            {

-                clonecutpoint.LoopingPred.Remove(gn);

-                clonecutpoint.LoopingPred.Add(clonemap[gn]);

-            }

-

-            

-

-            SucLoops.AddRange(l.SucLoops);

-            PreLoops.AddRange(l.PreLoops);

-            Cutpoint = clonecutpoint;

-            LoopNodes.Add(Cutpoint);

-            foreach (GraphNode gn in Cutpoint.LoopingPred)

-            {

-                CollectLoopBody(gn);

-            }

-            CollectLoopExitNodes();

-        }

-

-        private void CollectLoopBody(GraphNode gn)

-        {

-            if (gn == Cutpoint) return;

-            if (!LoopNodes.Contains(gn))

-            {

-                if (gn.IsCutpoint) // nested loop found

-                {

-                    Loop lo = new Loop(gn);

-                    foreach (GraphNode lgn in lo.LoopNodes)

-                    {

-                        if (!LoopNodes.Contains(lgn)) LoopNodes.Add(lgn);

-                    }

-                    NestedLoops.Add(lo);

-                }

-                else

-                {

-                    LoopNodes.Add(gn);

-                }

-                foreach (GraphNode pre in gn.Pre) if (!gn.LoopingPred.Contains(pre)) CollectLoopBody(pre);

-            }

-        }

-

-        private void CollectLoopExitNodes()

-        {

-            foreach (GraphNode gn in LoopNodes)

-            {

-                foreach (GraphNode gn_ in gn.Suc)

-                {

-                    if (!LoopNodes.Contains(gn_) && !LoopExitNodes.Contains(gn_)) LoopExitNodes.Add(gn_);

-                }

-            }

-        }

-

-        public GraphNode Cutpoint;

-        public List<GraphNode> LoopExitNodes = new List<GraphNode>();

-        public List<Loop> NestedLoops = new List<Loop>();

-        public List<Loop> SucLoops = new List<Loop>();

-        public List<Loop> PreLoops = new List<Loop>();

-        public List<GraphNode> LoopNodes = new List<GraphNode>();

-    }

-    #endregion

-

-    #endregion

-}
\ No newline at end of file
diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/VCGeneration/DoomedStrategy.cs
deleted file mode 100644
index c08662b1..00000000
--- a/Source/VCGeneration/DoomedStrategy.cs
+++ /dev/null
@@ -1,528 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    #region SuperClass for different doomed code detection strategies

-    abstract internal class DoomDetectionStrategy

-    {

-        public int __DEBUG_BlocksChecked = 0;

-        public int __DEBUG_BlocksTotal = 0;

-        public int __DEBUG_InfeasibleTraces = 0;

-        public int __DEBUG_TracesChecked = 0;

-        public int __DEBUG_TracesTotal = 0;

-        public int __DEBUG_EQCTotal = 0;

-        public int __DEBUG_EQCLeaf = 0;

-        public int __DEBUG_EQCChecked = 0;

-

-        //Please use this one to toggle your Debug output

-        protected bool __DEBUGOUT = CommandLineOptions.Clo.DoomStrategy != -1;

-

-        protected Implementation impl;

-        protected BlockHierachy m_BlockH = null;

-

-        protected int m_MaxBranchingDepth = 0;

-        protected int m_MaxK = 0;

-

-        protected Stopwatch sw = new Stopwatch();

-

-

-        // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to 

-        // create an error message

-        public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();

-

-        private List<Block> __DEBUG_minelements = new List<Block>();

-

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

-        }

-

-        public int MaxBlocks, MinBlocks;

-        public bool HACK_NewCheck;

-

-        // This method is called by the prover while it returns true. The prover checks for each 

-        // List lb if 

-        //      |= !lb_1 /\ ... /\ !lb_n => wlp(Program, false) 

-        // and passes the result to SetCurrentResult

-        abstract public bool GetNextBlock(out  List<Block> passBlock);

-

-        // This method is called to inform about the prover outcome for the previous GetNextBlock call.

-        abstract public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb);

-

-        protected List<Block> m_GetErrorTraceFromCE(DoomErrorHandler cb)

-        {

-            BlockHierachyNode tn=null;

-            List<Block> errortrace = new List<Block>();

-            foreach (Block b in cb.TraceNodes)

-            {

-                if (errortrace.Contains(b)) continue;

-                if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out tn))

-                {

-                    foreach (Block b_ in tn.Unavoidable)

-                    {

-                        if (!errortrace.Contains(b_)) errortrace.Add(b_);

-                    }

-                    foreach (Block b_ in tn.Content)

-                    {

-                        if (!errortrace.Contains(b_)) errortrace.Add(b_);

-                    }

-                }

-            }

-            return errortrace;

-        }

-

-        private List<int> __pathLength = new List<int>();

-        private List<int> __leavespp = new List<int>();

-        protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen)

-        {

-            if (b.Predecessors.Length > 1) branchingdepth--;

-

-            GotoCmd gc = b.TransferCmd as GotoCmd;

-            if (__DEBUG_minelements.Contains(b)) leavespp++;

-            plen++;

-            if (gc != null && gc.labelTargets.Length>0)

-            {

-                if (gc.labelTargets.Length > 1) branchingdepth++;

-                m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth;

-                foreach (Block s in gc.labelTargets)

-                {

-                    m_GatherInfo(s, branchingdepth, leavespp,plen);

-                }

-            }

-            else

-            {

-                __pathLength.Add(plen);

-                __leavespp.Add(leavespp);

-                m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp;

-            }

-        }

-

-

-

-    }

-    #endregion

-

-    #region BruteForce Strategy

-    internal class NoStrategy : DoomDetectionStrategy

-    {

-        private List<Block> m_Blocks = new List<Block>();

-        private int m_Current = 0;

-

-        public NoStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)

-            : base(imp, unifiedexit, unreach)

-        {

-            m_Blocks = imp.Blocks;

-        }

-

-        override public bool GetNextBlock(out  List<Block> lb)

-        {

-            if (m_Current < m_Blocks.Count)

-            {

-                lb = new List<Block>();

-                lb.Add(m_Blocks[m_Current]);

-                m_Current++;

-                return true;

-            }

-            lb = null;

-            return false;

-        }

-

-        // This method is called to inform about the prover outcome for the previous GetNextBlock call.

-        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

-        {

-            this.__DEBUG_BlocksChecked++;

-            // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)

-            if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count)

-            {

-                List<Block> lb = new List<Block>();

-                lb.Add(m_Blocks[m_Current - 1]);

-                DetectedBlock.Add(lb);

-            }

-            return true;

-        }

-    }

-    #endregion

-

-    #region Only check the minimal elements of the Hasse diagram

-    internal class HierachyStrategy : DoomDetectionStrategy

-    {

-        private List<Block> m_Blocks = new List<Block>();

-        private List<Block> m_doomedBlocks = new List<Block>();

-        private int m_Current = 0;

-

-        public HierachyStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)

-            : base(imp, unifiedexit, unreach)

-        {            

-            foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

-            {

-                if (bhn.Content.Count > 0)

-                {

-                    m_Blocks.Add(bhn.Content[0]);

-                }

-            }

-        }

-

-        override public bool GetNextBlock(out  List<Block> lb)

-        {

-            sw.Start();

-            if (m_Current < m_Blocks.Count)

-            {

-                lb = new List<Block>();

-                lb.Add(m_Blocks[m_Current]);

-                m_Current++;

-                return true;

-            }

-            else

-            {

-                DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks));

-            }

-            lb = null;

-            return false;

-        }

-

-        // This method is called to inform about the prover outcome for the previous GetNextBlock call.

-        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

-        {

-            this.__DEBUG_BlocksChecked++;

-            // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)

-            if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count)

-            {

-                m_doomedBlocks.Add(m_Blocks[m_Current - 1]);

-            }

-            if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks);

-            sw.Stop();

-            sw.Reset();

-

-            return true;

-        }

-    }

-    #endregion

-

-    #region Only check the minimal elements of the Hasse diagram and use CEs

-    internal class HierachyCEStrategy : DoomDetectionStrategy

-    {

-        private List<Block> m_Blocks = new List<Block>();

-        private List<Block> m_doomedBlocks = new List<Block>();

-        private Block m_Current = null;

-

-        public HierachyCEStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)

-            : base(imp, unifiedexit, unreach)

-        {            

-            foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

-            {

-                if (bhn.Content.Count > 0)

-                {

-                    m_Blocks.Add(bhn.Content[0]);

-                }

-            }

-        }

-

-        override public bool GetNextBlock(out  List<Block> lb)

-        {

-            m_Current = null;

-            if (m_Blocks.Count > 0)

-            {

-                m_Current = m_Blocks[0];

-                m_Blocks.Remove(m_Current);

-                lb = new List<Block>();

-                lb.Add(m_Current);

-                return true;

-            }

-            else

-            {

-                DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks));

-            }

-            lb = null;

-            return false;

-        }

-

-        // This method is called to inform about the prover outcome for the previous GetNextBlock call.

-        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

-        {

-            this.__DEBUG_BlocksChecked++;

-            // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)

-            if (outcome == ProverInterface.Outcome.Valid && m_Current != null)

-            {

-                m_doomedBlocks.Add(m_Current);

-            }

-            else if (outcome == ProverInterface.Outcome.Invalid)

-            {

-                List<Block> errortrace = m_GetErrorTraceFromCE(cb);

-                foreach (Block b in errortrace)

-                {

-                    if (m_Blocks.Contains(b))

-                    {

-                        m_Blocks.Remove(b);

-                    }

-                }

-                cb.TraceNodes.Clear();

-            }

-            return true;

-        }

-    }

-    #endregion

-

-    #region Path Cover Optimization with L

-    internal class PathCoverStrategy : DoomDetectionStrategy

-    {

-        List<Block> m_Uncheckedlocks = new List<Block>();

-        List<Block> m_Ignore = new List<Block>();

-

-        Random m_Random = new Random();

-        bool m_NoMoreMoves = false;

-

-        private List<Block> m_foundBlock = new List<Block>();

-

-        public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)

-            : base(imp, unifiedexit, unreach)

-        {            

-            m_Ignore = unreach;

-            HACK_NewCheck = true;

-            impl = imp;

-            foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

-            {

-                if (bhn.Content.Count > 0)

-                {

-                    m_Uncheckedlocks.Add(bhn.Content[0]);

-                }

-

-            }

-            m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

-            MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);

-            MaxBlocks = -1;

-        }

-

-        override public bool GetNextBlock(out  List<Block> lb)

-        {

-            sw.Start();

-

-            lb = new List<Block>();

-

-            if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)

-            {

-                if (m_Uncheckedlocks.Count > 0)

-                {

-                    DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks));

-                }

-

-                return false;

-            }

-

-            lb.AddRange(m_Uncheckedlocks);

-

-            return true;

-        }

-

-        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

-        {

-            this.__DEBUG_BlocksChecked++;            

-            // Valid means infeasible...            

-            int oldl = MinBlocks;

-            int oldsize = m_Uncheckedlocks.Count;

-

-

-            if (outcome == ProverInterface.Outcome.Valid)

-            {

-                this.__DEBUG_InfeasibleTraces++;

-                if (MinBlocks == 1)

-                {

-                    m_NoMoreMoves = true;

-                }

-                else

-                {

-                    MinBlocks = 1;

-                }

-            }

-            else if (outcome == ProverInterface.Outcome.Invalid)

-            {

-                this.__DEBUG_TracesChecked++;

-                

-                List<Block> errortrace = m_GetErrorTraceFromCE(cb);

-                foreach (Block b in errortrace)

-                {

-                    if (m_Uncheckedlocks.Contains(b))

-                    {

-                        m_Uncheckedlocks.Remove(b);

-                    }

-                }

-                cb.TraceNodes.Clear();

-                m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

-                if (m_MaxK < 1)

-                {

-                    m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

-                }

-                MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);

-                //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK;

-                

-            }

-            else

-            {

-                m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

-            }

-            if (__DEBUGOUT) 

-                Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);

-            sw.Stop();

-            sw.Reset();

-            return true;

-        }

-

-

-    }

-    #endregion

-

-    #region Path Cover Optimization with K

-    internal class PathCoverStrategyK : DoomDetectionStrategy

-    {

-        List<Block> m_Uncheckedlocks = new List<Block>();

-        List<Block> m_Ignore = new List<Block>();

-

-        Random m_Random = new Random();

-        bool m_NoMoreMoves = false;

-

-        private List<Block> m_foundBlock = new List<Block>();

-

-        public PathCoverStrategyK(Implementation imp, Block unifiedexit, List<Block> unreach)

-            : base(imp, unifiedexit, unreach)

-        {

-            m_Ignore = unreach;

-            HACK_NewCheck = true;

-            impl = imp;

-            foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

-            {

-                if (bhn.Content.Count > 0)

-                {

-                    m_Uncheckedlocks.Add(bhn.Content[0]);

-                }

-

-            }

-

-            m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

-

-            MaxBlocks = m_Uncheckedlocks.Count;

-                if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0)

-                {

-                    MaxBlocks = m_MaxK;

-                }

-                else if (m_MaxK >= m_Uncheckedlocks.Count)

-                {

-                    MaxBlocks = m_Uncheckedlocks.Count;

-                }

-                else

-                {

-                    MaxBlocks = 1;

-                }

-                //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks);

-        }

-

-        override public bool GetNextBlock(out  List<Block> lb)

-        {

-            sw.Start();

-

-            lb = new List<Block>();

-

-            if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)

-            {

-                if (m_Uncheckedlocks.Count > 0)

-                {

-                    DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks));

-                }

-

-                return false;

-            }

-

-            lb.AddRange(m_Uncheckedlocks);

-

-            MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks;

-            MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0);

-            return true;

-        }

-

-        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

-        {

-            this.__DEBUG_BlocksChecked++;

-            // Valid means infeasible...

-            int oldk = MaxBlocks;

-            int oldl = MinBlocks;

-            int oldsize = m_Uncheckedlocks.Count;

-

-            if (outcome == ProverInterface.Outcome.Valid)

-            {

-                this.__DEBUG_InfeasibleTraces++;

-                if (MaxBlocks == 1)

-                {

-                    m_NoMoreMoves = true;

-                }

-                else

-                {

-                    MaxBlocks /= 2;

-                }

-            }

-            else if (outcome == ProverInterface.Outcome.Invalid)

-            {

-                this.__DEBUG_TracesChecked++;

-

-                List<Block> errortrace = m_GetErrorTraceFromCE(cb);

-                foreach (Block b in errortrace)

-                {

-                    if (m_Uncheckedlocks.Contains(b))

-                    {

-                        m_Uncheckedlocks.Remove(b);

-                    }

-                }

-                cb.TraceNodes.Clear();

-

-                int k = m_BlockH.GetMaxK(m_Uncheckedlocks);

-                MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k;

-            }

-            else

-            {

-                m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

-            }

-            if (__DEBUGOUT) 

-                Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);

-            sw.Stop();

-            sw.Reset();

-            return true;

-        }

-

-

-    }

-    #endregion

-

-}
\ No newline at end of file
diff --git a/Source/VCGeneration/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs
deleted file mode 100644
index 006a923f..00000000
--- a/Source/VCGeneration/GraphAlgorithms.cs
+++ /dev/null
@@ -1,127 +0,0 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public static class GraphAlgorithms {
-
-  public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource) {
-    var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
-    if (exits.Count == 0)
-      return null;
-    var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
-    if (exits.Count == 1)
-      dual.AddSource(exits[0]);
-    else {
-      dual.AddSource(dummySource);
-      foreach (var exit in exits)
-        dual.AddEdge(dummySource, exit);
-    }
-    return dual;
-  }
-
-  public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
-    Contract.Assert(g.Reducible);
-
-    int n = g.Nodes.Count;
-    var nodeToNumber = new Dictionary<Node, int>(n);
-    var numberToNode = new Node[n];
-    var allNodes = new List<int>();
-    int counter = 0;
-    foreach (Node node in g.Nodes) {
-      numberToNode[counter] = node;
-      nodeToNumber[node] = counter;
-      allNodes.Add(counter);
-      counter++;
-    }
-
-    var loops = new List<int>[n];
-    foreach (var h in g.Headers) {
-      var loopNodes = new HashSet<Node>();
-      foreach (var b in g.BackEdgeNodes(h))
-        loopNodes.UnionWith(g.NaturalLoops(h, b));
-      loops[nodeToNumber[h]] =
-        new List<int>(loopNodes.Select(node => nodeToNumber[node]));
-    }
-
-    var successors = new List<int>[n];
-    int[] incomingEdges = new int[n];
-
-    foreach (var e in g.Edges) {
-      Contract.Assert(e.Item1 != null);
-      Contract.Assert(e.Item2 != null);
-      int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
-      if (loops[target] == null || !loops[target].Contains(source)) {
-        if (successors[source] == null)
-          successors[source] = new List<int>();
-        successors[source].Add(target);
-        incomingEdges[target]++;
-      }
-    }
-
-    var sortedNodes = new List<Tuple<Node, bool>>();
-
-    var regionStack = new Stack<Tuple<Node, List<int>>>();
-    regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
-
-    while (regionStack.Count != 0) {
-      int rootIndex = -1;
-      foreach (var i in regionStack.Peek().Item2) {
-        if (incomingEdges[i] == 0) {
-          rootIndex = i;
-          break;
-        }
-      }
-      if (rootIndex == -1) {
-        var region = regionStack.Pop();
-        if (regionStack.Count != 0)
-          sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
-        continue;
-      }
-      incomingEdges[rootIndex] = -1;
-      sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
-      if (successors[rootIndex] != null)
-        foreach (int s in successors[rootIndex])
-          incomingEdges[s]--;
-      if (loops[rootIndex] != null)
-        regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
-                                                    loops[rootIndex]));
-    }
-
-    return sortedNodes;
-  }
-  
-  // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
-  // "The Program Dependence Graph and Its Use in Optimization"
-  public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new() {
-    Graph<Node> dual = g.Dual(new Node());
-    DomRelation<Node> pdom = dual.DominatorMap;
-    var result = new Dictionary<Node, HashSet<Node>>();
-
-    var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
-    foreach (var edge in S) {
-      var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
-      var deps = new List<Node>();
-      if (L == edge.Item1) {
-        pdom.DominatedBy(edge.Item2, edge.Item1, deps);
-        deps.Add(edge.Item2);
-        deps.Add(edge.Item1);
-      } else {
-        pdom.DominatedBy(edge.Item2, L, deps);
-        deps.Add(edge.Item2);
-      }
-      if (result.ContainsKey(edge.Item1)) {
-        result[edge.Item1].UnionWith(deps);
-      } else {
-        result[edge.Item1] = new HashSet<Node>(deps);
-      }
-    }
-    return result;
-  }
-
-}
-
-}
diff --git a/Source/VCGeneration/HasseDiagram.cs b/Source/VCGeneration/HasseDiagram.cs
deleted file mode 100644
index d5fdfb66..00000000
--- a/Source/VCGeneration/HasseDiagram.cs
+++ /dev/null
@@ -1,424 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    internal class BlockHierachyNode

-    {

-        public List<Block> Unavoidable;

-        public List<Block> Content = new List<Block>();

-        public List<BlockHierachyNode> Parents = new List<BlockHierachyNode>();

-        public List<BlockHierachyNode> Children = new List<BlockHierachyNode>();

-

-        public bool Checked, Doomed, DoubleChecked;

-

-        public BlockHierachyNode(Block current, List<Block> unavoidable)

-        {

-            Checked = false; Doomed = false; DoubleChecked = false;

-            Unavoidable = unavoidable;

-            Content.Add(current);

-        }

-

-        public static bool operator <(BlockHierachyNode left, BlockHierachyNode right)

-        {

-            return Compare(left,right)>0;

-        }

-

-        public static bool operator >(BlockHierachyNode left, BlockHierachyNode right)

-        {

-            return Compare(left, right) < 0;

-        }

-

-        // Compare the unavoidable blocks of two BlockHierachyNodes. 

-        // returns 0 if sets have the same size, -1 if l2 has an element 

-        // that is not in l1, otherwise the size of the intersection.

-        public static int Compare(BlockHierachyNode l1, BlockHierachyNode l2)

-        {

-            List<Block> tmp = new List<Block>();

-            tmp.AddRange(l2.Unavoidable);

-            foreach (Block b in l1.Unavoidable)

-            {

-                if (tmp.Contains(b)) tmp.Remove(b);

-                else return -1;

-            }

-            return tmp.Count;

-        }

-    }

-

-    internal class HasseDiagram

-    {

-        public readonly List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();

-        public readonly List<BlockHierachyNode> Roots = new List<BlockHierachyNode>();

-

-        public HasseDiagram(List<BlockHierachyNode> nodes)

-        {

-            Dictionary<BlockHierachyNode, List<BlockHierachyNode>> largerElements = new Dictionary<BlockHierachyNode, List<BlockHierachyNode>>();

-            foreach (BlockHierachyNode left in nodes)

-            {

-                largerElements[left] = new List<BlockHierachyNode>();

-                foreach (BlockHierachyNode right in nodes)

-                {

-                    if (left != right)

-                    {

-                        if (left < right)

-                        {

-                            largerElements[left].Add(right);

-                        }

-                    }

-                }

-                if (largerElements[left].Count == 0) Leaves.Add(left);

-            }

-

-            List<BlockHierachyNode> done = new List<BlockHierachyNode>();

-            List<BlockHierachyNode> lastround = null;

-

-            //Debugger.Break();

-

-            // Now that we have the leaves, build the Hasse diagram

-            while (done.Count < nodes.Count)

-            {

-                List<BlockHierachyNode> maxelements = new List<BlockHierachyNode>();

-                maxelements.AddRange(nodes);

-                foreach (BlockHierachyNode bhn in nodes)

-                {

-                    if (!done.Contains(bhn))

-                    {

-                        foreach (BlockHierachyNode tmp in largerElements[bhn])

-                        {

-                            if (maxelements.Contains(tmp)) maxelements.Remove(tmp);

-                        }

-                    }

-                    else

-                    {

-                        maxelements.Remove(bhn);

-                    }

-                }

-

-                done.AddRange(maxelements);

-

-                if (lastround != null)

-                {

-                    foreach (BlockHierachyNode tmp in lastround)

-                    {

-                        foreach (BlockHierachyNode tmp2 in maxelements)

-                        {

-                            if (largerElements[tmp].Contains(tmp2))

-                            {

-                                if (!tmp.Children.Contains(tmp2)) tmp.Children.Add(tmp2);

-                                if (!tmp2.Parents.Contains(tmp)) tmp2.Parents.Add(tmp);

-                            }

-                        }

-                    }

-                }

-                else

-                {

-                    Roots.AddRange(maxelements);

-                }

-                lastround = maxelements;

-            }

-        }

-

-

-    }

-

-    internal class BlockHierachy

-    {

-        public BlockHierachyNode RootNode = null;

-        readonly public Dictionary<Block, BlockHierachyNode> BlockToHierachyMap = new Dictionary<Block, BlockHierachyNode>();

-        readonly public Dictionary<Block, List<Block>> Dominators = new Dictionary<Block, List<Block>>();

-        readonly public Dictionary<Block, List<Block>> PostDominators = new Dictionary<Block, List<Block>>();

-        readonly public List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();

-

-        private Implementation m_Impl;

-

-        public BlockHierachy(Implementation impl, Block unifiedExit)

-        {

-            m_Impl = impl;

-            List<Block> blocks = impl.Blocks;

-            List<BlockHierachyNode> tmp_hnodes = new List<BlockHierachyNode>();

-            Dictionary<Block, List<Block>> unavoidable = new Dictionary<Block, List<Block>>();

-

-            BfsTraverser(blocks[0], true, Dominators);

-            BfsTraverser(unifiedExit, false, PostDominators);

-

-            foreach (Block b in blocks)

-            {

-                List<Block> l1 = Dominators[b];

-                List<Block> l2 = PostDominators[b];

-                unavoidable[b] = m_MergeLists(l1, l2);

-

-                BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]);

-                bool found = false;

-                foreach (KeyValuePair<Block, BlockHierachyNode> kvp in BlockToHierachyMap)

-                {

-                    if (BlockHierachyNode.Compare(kvp.Value, bhn) == 0) // using the overloaded compare operator

-                    {

-                        kvp.Value.Content.AddRange(bhn.Content);

-                        BlockToHierachyMap[b] = kvp.Value;

-                        found = true;

-                        break;

-                    }

-                }

-                if (!found)

-                {

-                    BlockToHierachyMap[b] = bhn;

-                    tmp_hnodes.Add(bhn);

-                }

-            }

-

-            HasseDiagram hd = new HasseDiagram(tmp_hnodes);

-            Leaves = hd.Leaves;            

-        }

-

-        public int GetMaxK(List<Block> blocks)

-        {

-            m_GetMaxK(blocks);

-            return (m_MaxK>0) ? m_MaxK : 1;

-        }

-

-        private int m_MaxK = 0;

-        private void m_GetMaxK(List<Block> blocks)

-        {

-            m_MaxK = 0;

-            Dictionary<Block, int> kstore = new Dictionary<Block, int>();

-            List<Block> todo = new List<Block>();

-            List<Block> done = new List<Block>();

-            todo.Add(m_Impl.Blocks[0]);

-            kstore[m_Impl.Blocks[0]] = 0;

-            int localmax;

-            Block current = null;

-            while (todo.Count > 0)

-            {

-                current = todo[0];

-                todo.Remove(current);

-                bool ready = true;

-                localmax = 0;

-                if (current.Predecessors!=null) {

-                    foreach (Block p in current.Predecessors)

-                    {

-                        if (!done.Contains(p))

-                        {

-                            ready = false; break;

-                        }

-                        else localmax = (localmax > kstore[p]) ? localmax : kstore[p];

-                    }

-                }

-                if (!ready)

-                {

-                    todo.Add(current); continue;

-                }

-                done.Add(current);

-                kstore[current] =  (blocks.Contains(current)) ? localmax +1 : localmax;

-

-                m_MaxK = (kstore[current] > m_MaxK) ? kstore[current] : m_MaxK;

-

-                GotoCmd gc = current.TransferCmd as GotoCmd;

-                if (gc != null)

-                {

-                    foreach (Block s in gc.labelTargets)

-                    {

-                        if (!todo.Contains(s)) todo.Add(s);

-                    }

-                }

-            }

-

-        }

-

-        public List<Block> GetOtherDoomedBlocks(List<Block> doomedblocks)

-        {

-            List<Block> alsoDoomed = new List<Block>();

-            List<BlockHierachyNode> todo = new List<BlockHierachyNode>();

-            foreach (Block b in doomedblocks)

-            {

-                BlockToHierachyMap[b].Doomed = true;                

-                todo.Add(BlockToHierachyMap[b]);

-            }

-

-            while (todo.Count > 0)

-            {

-                BlockHierachyNode current = todo[0];

-                todo.Remove(current);

-                if (!current.Doomed && current.Children.Count > 0)

-                {

-                    bool childrenDoomed = true;

-                    foreach (BlockHierachyNode c in current.Children)

-                    {

-                        if (!c.Doomed) { childrenDoomed = false; break; }

-                    }

-                    if (childrenDoomed) current.Doomed = true;

-                }

-

-                if (current.Doomed)

-                {

-                    foreach (BlockHierachyNode p in current.Parents)

-                    {

-                        if (!todo.Contains(p)) todo.Add(p);

-                    }

-                    foreach (Block b in current.Content)

-                    {

-                        if (!alsoDoomed.Contains(b)) alsoDoomed.Add(b);

-                    }

-                }

-            }

-

-            return alsoDoomed;

-        }

-

-        public void Impl2Dot(string filename)

-        {

-

-            Contract.Requires(filename != null);

-            List<string> nodes = new List<string>();

-            List<string> edges = new List<string>();

-

-            string nodestyle = "[shape=box];";

-

-            List<BlockHierachyNode> nl = new List<BlockHierachyNode>();

-            foreach (BlockHierachyNode h in BlockToHierachyMap.Values) if (!nl.Contains(h)) nl.Add(h);

-

-

-            foreach (BlockHierachyNode b in nl)

-            {

-                String l1 = "";

-                foreach (Block bl in b.Content) l1 = String.Format("{0}_{1}", l1, bl.Label);

-

-                Contract.Assert(b != null);

-                nodes.Add(string.Format("\"{0}\" {1}", l1, nodestyle));

-                foreach (BlockHierachyNode b_ in b.Children)

-                {

-

-                    String l2 = "";

-                    foreach (Block bl in b_.Content) l2 = String.Format("{0}_{1}", l2, bl.Label);

-                    edges.Add(String.Format("\"{0}\" -> \"{1}\";", l1, l2));

-                }

-

-            }

-

-            using (StreamWriter sw = new StreamWriter(filename))

-            {

-                sw.WriteLine(String.Format("digraph {0} {{", "DISCO"));

-                //            foreach (string! s in nodes) {

-                //                sw.WriteLine(s);

-                //            }

-                foreach (string s in edges)

-                {

-                    Contract.Assert(s != null);

-                    sw.WriteLine(s);

-                }

-                sw.WriteLine("}}");

-                sw.Close();

-            }

-        }

-        

-        private void BfsTraverser(Block current, bool forward, Dictionary<Block, List<Block>> unavoidableBlocks)

-        {

-            List<Block> todo = new List<Block>();

-            List<Block> done = new List<Block>();

-            unavoidableBlocks[current] = new List<Block>();

-            //Debugger.Break();

-            todo.Add(current);

-            while (todo.Count > 0)

-            {

-                current = todo[0];

-                todo.Remove(current);

-                BlockSeq pre = m_Predecessors(current, forward);

-                bool ready = true;

-                if (pre != null)

-                {

-                    foreach (Block bpre in pre)

-                    {

-                        if (!done.Contains(bpre))

-                        {

-                            ready = false;

-                            break;

-                        }

-                    }

-                }

-                if (!ready)

-                {

-                    todo.Add(current);

-                    continue;

-                }

-                done.Add(current);

-                unavoidableBlocks[current].Add(current);

-

-                BlockSeq suc = m_Succecessors(current, forward);

-                if (suc == null) continue;

-                foreach (Block bsuc in suc)

-                {

-                    if (unavoidableBlocks.ContainsKey(bsuc))

-                    {

-                        unavoidableBlocks[bsuc] = m_IntersectLists(unavoidableBlocks[bsuc], unavoidableBlocks[current]);

-                    }

-                    else

-                    {

-                        todo.Add(bsuc);

-                        unavoidableBlocks[bsuc] = new List<Block>();

-                        unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]);

-                    }

-

-                }

-            }

-

-        }

-

-        private List<Block> m_MergeLists(List<Block> lb1, List<Block> lb2)

-        {

-            List<Block> ret = new List<Block>();

-            ret.AddRange(lb1);

-            foreach (Block b in lb2)

-            {

-                if (!ret.Contains(b)) ret.Add(b);

-            }

-            return ret;

-        }

-

-        private List<Block> m_IntersectLists(List<Block> lb1, List<Block> lb2)

-        {

-            List<Block> ret = new List<Block>();

-            ret.AddRange(lb1);

-            foreach (Block b in lb2)

-            {

-                if (!lb1.Contains(b)) ret.Remove(b);

-            }

-            foreach (Block b in lb1)

-            {

-                if (ret.Contains(b) && !lb2.Contains(b)) ret.Remove(b);

-            }

-            return ret;

-        }

-

-        private BlockSeq m_Predecessors(Block b, bool forward)

-        {

-            if (forward) return b.Predecessors;

-            GotoCmd gc = b.TransferCmd as GotoCmd;

-            if (gc != null)

-            {

-                return gc.labelTargets;

-            }

-            return null;

-        }

-

-        private BlockSeq m_Succecessors(Block b, bool forward)

-        {

-            return m_Predecessors(b, !forward);

-        }

-

-

-    }

-

-}
\ No newline at end of file
diff --git a/Source/VCGeneration/SmartBlockPredicator.cs b/Source/VCGeneration/SmartBlockPredicator.cs
deleted file mode 100644
index b4f5a3df..00000000
--- a/Source/VCGeneration/SmartBlockPredicator.cs
+++ /dev/null
@@ -1,528 +0,0 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public class SmartBlockPredicator {
-
-  Program prog;
-  Implementation impl;
-  Graph<Block> blockGraph;
-  List<Tuple<Block, bool>> sortedBlocks;
-
-  Func<Procedure, bool> useProcedurePredicates;
-
-  Dictionary<Block, Variable> predMap, defMap;
-  Dictionary<Block, HashSet<Variable>> ownedMap;
-  Dictionary<Block, Block> parentMap;
-  Dictionary<Block, PartInfo> partInfo;
-
-  IdentifierExpr fp;
-  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>();
-  bool myUseProcedurePredicates;
-  UniformityAnalyser uni;
-
-  SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
-    prog = p;
-    impl = i;
-    useProcedurePredicates = upp;
-    myUseProcedurePredicates = useProcedurePredicates(i.Proc);
-    uni = u;
-  }
-
-  void PredicateCmd(Expr p, 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 BlockSeq(trueBlock, falseBlock));
-      trueBlock.TransferCmd = falseBlock.TransferCmd =
-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
-      nextBlock = contBlock;
-    } else {
-      PredicateCmd(p, block.Cmds, cmd);
-      nextBlock = block;
-    }
-  }
-
-  void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {
-    if (cmd is CallCmd) {
-      var cCmd = (CallCmd)cmd;
-      Debug.Assert(useProcedurePredicates(cCmd.Proc));
-      cCmd.Ins.Insert(0, p != null ? p : Expr.True);
-      cmdSeq.Add(cCmd);
-    } else if (p == null) {
-      cmdSeq.Add(cmd);
-    } else if (cmd is AssignCmd) {
-      var aCmd = (AssignCmd)cmd;
-      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
-                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
-                     new NAryExpr(Token.NoToken,
-                       new IfThenElse(Token.NoToken),
-                       new ExprSeq(p, rhs, lhs.AsExpr))))));
-    } else if (cmd is AssertCmd) {
-      var aCmd = (AssertCmd)cmd;
-      Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
-      aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
-      cmdSeq.Add(aCmd);
-    } else if (cmd is AssumeCmd) {
-      var aCmd = (AssumeCmd)cmd;
-      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
-    } else if (cmd is HavocCmd) {
-      var hCmd = (HavocCmd)cmd;
-      foreach (IdentifierExpr v in hCmd.Vars) {
-        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
-        Contract.Assert(type != null);
-
-        IdentifierExpr havocTempExpr;
-        if (havocVars.ContainsKey(type)) {
-          havocTempExpr = havocVars[type];
-        } else {
-          var havocVar = new LocalVariable(Token.NoToken,
-                             new TypedIdent(Token.NoToken,
-                                            "_HAVOC_" + type.ToString(), type));
-          impl.LocVars.Add(havocVar);
-          havocVars[type] = havocTempExpr =
-            new IdentifierExpr(Token.NoToken, havocVar);
-        }
-        cmdSeq.Add(new HavocCmd(Token.NoToken,
-                                new IdentifierExprSeq(havocTempExpr)));
-        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
-                                    new NAryExpr(Token.NoToken,
-                                      new IfThenElse(Token.NoToken),
-                                      new ExprSeq(p, havocTempExpr, v))));
-      }
-    } else if (cmd is CommentCmd) {
-      // skip
-    } else if (cmd is StateCmd) {
-      var sCmd = (StateCmd)cmd;
-      var newCmdSeq = new CmdSeq();
-      foreach (Cmd c in sCmd.Cmds)
-        PredicateCmd(p, newCmdSeq, c);
-      sCmd.Cmds = newCmdSeq;
-      cmdSeq.Add(sCmd);
-    } else {
-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
-    }
-  }
-
-  // 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, CmdSeq 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.Length == 1) {
-        if (defMap.ContainsKey(gCmd.labelTargets[0]))
-          PredicateCmd(p, cmdSeq,
-                       Cmd.SimpleAssign(Token.NoToken,
-                                        Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
-      } else {
-        Debug.Assert(gCmd.labelTargets.Length > 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;
-
-          var part = partInfo[target];
-          if (defMap.ContainsKey(part.realDest))
-            PredicateCmd(p, 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, 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());
-    }
-  }
-
-  Variable FreshPredicate(ref int predCount) {
-    var pVar = new LocalVariable(Token.NoToken,
-                                 new TypedIdent(Token.NoToken,
-                                                "p" + predCount++,
-                                                Microsoft.Boogie.Type.Bool));
-    impl.LocVars.Add(pVar);
-    return pVar;
-  }
-
-  void AssignPredicates(Graph<Block> blockGraph,
-                        DomRelation<Block> dom,
-                        DomRelation<Block> pdom,
-                        IEnumerator<Tuple<Block, bool>> i,
-                        Variable headPredicate,
-                        ref int predCount) {
-    var header = i.Current.Item1;
-    var regionPreds = new List<Tuple<Block, Variable>>();
-    var ownedPreds = new HashSet<Variable>();
-    ownedMap[header] = ownedPreds;
-
-    if (headPredicate != null) {
-      predMap[header] = headPredicate;
-      defMap[header] = headPredicate;
-      regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
-    }
-
-    while (i.MoveNext()) {
-      var block = i.Current;
-      if (uni != null && uni.IsUniform(impl.Name, block.Item1))
-        continue;
-      if (block.Item2) {
-        if (block.Item1 == header)
-          return;
-      } else {
-        if (blockGraph.Headers.Contains(block.Item1)) {
-          parentMap[block.Item1] = header;
-          var loopPred = FreshPredicate(ref predCount);
-          ownedPreds.Add(loopPred);
-          AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);
-        } else {
-          bool foundExisting = false;
-          foreach (var regionPred in regionPreds) {
-            if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
-                pdom.DominatedBy(regionPred.Item1, block.Item1)) {
-              predMap[block.Item1] = regionPred.Item2;
-              foundExisting = true;
-              break;
-            }
-          }
-          if (!foundExisting) {
-            var condPred = FreshPredicate(ref predCount);
-            predMap[block.Item1] = condPred;
-            defMap[block.Item1] = condPred;
-            ownedPreds.Add(condPred);
-            regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
-          }
-        }
-      }
-    }
-  }
-
-  void AssignPredicates() {
-    DomRelation<Block> dom = blockGraph.DominatorMap;
-
-    Graph<Block> dualGraph = blockGraph.Dual(new Block());
-    DomRelation<Block> pdom = dualGraph.DominatorMap;
-
-    var iter = sortedBlocks.GetEnumerator();
-    if (!iter.MoveNext()) {
-      predMap = defMap = null;
-      ownedMap = null;
-      return;
-    }
-
-    int predCount = 0;
-    predMap = new Dictionary<Block, Variable>();
-    defMap = new Dictionary<Block, Variable>();
-    ownedMap = new Dictionary<Block, HashSet<Variable>>();
-    parentMap = new Dictionary<Block, Block>();
-    AssignPredicates(blockGraph, dom, pdom, iter,
-                     myUseProcedurePredicates ? impl.InParams[0] : null,
-                     ref predCount);
-  }
-
-  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;
-  }
-
-  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);
-  }
-
-  class PartInfo {
-    public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
-    public Expr pred;
-    public Block realDest;
-  }
-
-  Dictionary<Block, PartInfo> BuildPartitionInfo() {
-    var partInfo = new Dictionary<Block, PartInfo>();
-    foreach (var block in blockGraph.Nodes) {
-      if (uni.IsUniform(impl.Name, block))
-        continue;
-
-      var parts = block.Cmds.Cast<Cmd>().TakeWhile(
-          c => c is AssumeCmd &&
-          QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
-
-      Expr pred = null;
-      if (parts.Count() > 0) {
-        pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
-        block.Cmds =
-          new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
-      } else {
-        continue;
-      }
-
-      Block realDest = block;
-      if (block.Cmds.Length == 0) {
-        var gc = block.TransferCmd as GotoCmd;
-        if (gc != null && gc.labelTargets.Length == 1)
-          realDest = gc.labelTargets[0];
-      }
-      partInfo[block] = new PartInfo(pred, realDest);
-    }
-
-    return partInfo;
-  }
-
-  void PredicateImplementation() {
-    blockGraph = prog.ProcessLoops(impl);
-    sortedBlocks = blockGraph.LoopyTopSort();
-
-    AssignPredicates();
-    partInfo = BuildPartitionInfo();
-
-    if (myUseProcedurePredicates)
-      fp = Expr.Ident(impl.InParams[0]);
-
-    var newBlocks = new List<Block>();
-    Block prevBlock = null;
-    foreach (var n in sortedBlocks) {
-      if (predMap.ContainsKey(n.Item1)) {
-        var p = predMap[n.Item1];
-        var pExpr = Expr.Ident(p);
-
-        if (n.Item2) {
-          var backedgeBlock = new Block();
-          newBlocks.Add(backedgeBlock);

-
-          backedgeBlock.Label = n.Item1.Label + ".backedge";
-          backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
-            new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
-          backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                                  new BlockSeq(n.Item1));
-
-          var tailBlock = new Block();
-          newBlocks.Add(tailBlock);
-
-          tailBlock.Label = n.Item1.Label + ".tail";
-          tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
-                                               Expr.Not(pExpr)));

-

-          if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {

-            uni.AddNonUniform(impl.Name, backedgeBlock);

-            uni.AddNonUniform(impl.Name, tailBlock);

-          }
-
-          if (prevBlock != null)
-            prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                          new BlockSeq(backedgeBlock, tailBlock));
-          prevBlock = tailBlock;
-        } else {
-          PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
-        }
-      } else {
-        if (!n.Item2) {
-          PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
-        }
-      }
-    }
-
-    if (prevBlock != null)
-      prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
-
-    impl.Blocks = newBlocks;
-  }
-
-  private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
-    var firstBlock = block;
-
-    var oldCmdSeq = block.Cmds;
-    block.Cmds = new CmdSeq();
-    newBlocks.Add(block);
-    if (prevBlock != null) {
-      prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
-    }
-
-    if (parentMap.ContainsKey(block)) {
-      var parent = parentMap[block];
-      if (predMap.ContainsKey(parent)) {
-        var parentPred = predMap[parent];
-        if (parentPred != null) {
-          block.Cmds.Add(new AssertCmd(Token.NoToken,
-                                          pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))
-                                                        : Expr.Ident(parentPred)));
-        }
-      }
-    }
-
-    var transferCmd = block.TransferCmd;
-    foreach (Cmd cmd in oldCmdSeq)
-      PredicateCmd(pExpr, newBlocks, block, cmd, out block);
-
-    if (ownedMap.ContainsKey(firstBlock)) {
-      var owned = ownedMap[firstBlock];
-      foreach (var v in owned)
-        block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
-    }
-
-    bool hasPredicatedRegion;
-    PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
-
-    if (hasPredicatedRegion)
-      prevBlock = block;
-    else
-      prevBlock = null;
-
-    doneBlocks.Add(block);
-  }
-
-  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
-    if (myUseProcedurePredicates) {
-      return new NAryExpr(Token.NoToken,
-                 new IfThenElse(Token.NoToken),
-                 new ExprSeq(fp, then, eElse));
-    } else {
-      return then;
-    }
-  }
-
-  public static void Predicate(Program p,
-                               Func<Procedure, bool> useProcedurePredicates = null,
-                               UniformityAnalyser uni = null) {
-    useProcedurePredicates = useProcedurePredicates ?? (proc => false);
-    if (uni != null) {
-      var oldUPP = useProcedurePredicates;
-      useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
-    }
-
-    foreach (var decl in p.TopLevelDeclarations.ToList()) {
-      if (decl is Procedure || decl is Implementation) {
-        var proc = decl as Procedure;
-        Implementation impl = null;
-        if (proc == null) {
-          impl = (Implementation)decl;
-          proc = impl.Proc;
-        }
-
-        bool upp = useProcedurePredicates(proc);
-        if (upp) {
-          var dwf = (DeclWithFormals)decl;
-          var fpVar = new Formal(Token.NoToken,
-                                 new TypedIdent(Token.NoToken, "_P",
-                                                Microsoft.Boogie.Type.Bool),
-                                 /*incoming=*/true);
-          dwf.InParams = new VariableSeq(
-            (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
-              .ToArray());
-
-          if (impl == null) {
-            var newRequires = new RequiresSeq();
-            foreach (Requires r in proc.Requires) {
-              newRequires.Add(new Requires(r.Free,
-                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
-            }
-            var newEnsures = new EnsuresSeq();
-            foreach (Ensures e in proc.Ensures) {
-              newEnsures.Add(new Ensures(e.Free,
-                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
-            }
-          }
-        }
-
-        if (impl != null) {
-          try {
-            new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
-          } catch (Program.IrreducibleLoopException) { }
-        }
-      }
-    }
-  }
-
-  public static void Predicate(Program p, Implementation impl) {
-    try {
-      new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
-    }
-    catch (Program.IrreducibleLoopException) { }
-  }
-
-}
-
-}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 5c6a5f68..6ad97141 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -7,7 +7,7 @@ using System.Linq;
 using System.Text;

 using System.IO;

 using Microsoft.Boogie;

-using Graphing;

+using Microsoft.Boogie.GraphUtil;

 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/VCGeneration/UniformityAnalyser.cs
deleted file mode 100644
index 802ee2d2..00000000
--- a/Source/VCGeneration/UniformityAnalyser.cs
+++ /dev/null
@@ -1,556 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics;
-using Graphing;
-
-namespace Microsoft.Boogie
-{
-
-    public class UniformityAnalyser
-    {
-        private Program prog;
-
-        private bool doAnalysis, unstructured;
-
-        private ISet<Implementation> entryPoints;
-
-        private IEnumerable<Variable> nonUniformVars;
-
-        private bool ProcedureChanged;
-
-        private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
-
-        private Dictionary<string, HashSet<int>> nonUniformLoops;
-
-        private Dictionary<string, HashSet<Block>> nonUniformBlocks;
-
-        private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
-
-        private Dictionary<string, List<string>> inParameters;
-
-        private Dictionary<string, List<string>> outParameters;
-
-        private List<WhileCmd> loopStack;
-
-        private bool hitNonuniformReturn;
-
-        public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
-        {
-            this.prog = prog;
-            this.doAnalysis = doAnalysis;
-            this.unstructured = unstructured;
-            this.entryPoints = entryPoints;
-            this.nonUniformVars = nonUniformVars;
-            uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
-            nonUniformLoops = new Dictionary<string, HashSet<int>>();
-            nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
-            loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
-            inParameters = new Dictionary<string, List<string>>();
-            outParameters = new Dictionary<string, List<string>>();
-            loopStack = new List<WhileCmd>();
-        }
-
-        public void Analyse()
-        {
-            var impls = prog.TopLevelDeclarations.OfType<Implementation>();
-
-            foreach (var Impl in impls)
-            {
-                bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
-
-                uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
-                    (uniformProcedure, new Dictionary<string, bool> ()));
-
-                nonUniformLoops.Add(Impl.Name, new HashSet<int>());
-                loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
-
-                foreach (var v in nonUniformVars)
-                    SetNonUniform(Impl.Name, v.Name);
-
-                foreach (Variable v in Impl.LocVars)
-                {
-                    if (doAnalysis)
-                    {
-                        SetUniform(Impl.Name, v.Name);
-                    }
-                    else
-                    {
-                        SetNonUniform(Impl.Name, v.Name);
-                    }
-                }
-
-                inParameters[Impl.Name] = new List<string>();
-
-                foreach (Variable v in Impl.InParams)
-                {
-                    inParameters[Impl.Name].Add(v.Name);
-                    if (doAnalysis)
-                    {
-                        SetUniform(Impl.Name, v.Name);
-                    }
-                    else
-                    {
-                        SetNonUniform(Impl.Name, v.Name);
-                    }
-                }
-
-                outParameters[Impl.Name] = new List<string>();
-                foreach (Variable v in Impl.OutParams)
-                {
-                    outParameters[Impl.Name].Add(v.Name);
-                    if (doAnalysis)
-                    {
-                        SetUniform(Impl.Name, v.Name);
-                    }
-                    else
-                    {
-                        SetNonUniform(Impl.Name, v.Name);
-                    }
-                }
-
-                ProcedureChanged = true;
-            }
-
-            if (doAnalysis)
-            {
-                while (ProcedureChanged)
-                {

-                    ProcedureChanged = false;
-
-                    foreach (var Impl in impls)
-                    {
-                        hitNonuniformReturn = false;
-                        Analyse(Impl, uniformityInfo[Impl.Name].Key);
-                    }
-                }
-            }
-
-            foreach (var Impl in impls)
-            {
-                if (!IsUniform (Impl.Name))
-                {
-                    List<string> newIns = new List<String>();
-                    newIns.Add("_P");
-                    foreach (string s in inParameters[Impl.Name])
-                    {
-                        newIns.Add(s);
-                    }
-                    inParameters[Impl.Name] = newIns;
-                }
-            }
-        }
-
-        private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
-        {
-            if (unstructured)
-            {

-                if (!ControlFlowIsUniform)
-                {
-                    nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
-
-                    foreach (Variable v in Impl.LocVars) {
-                        if (IsUniform(Impl.Name, v.Name)) {
-                            SetNonUniform(Impl.Name, v.Name);
-                        }
-                    }

-

-                    foreach (Variable v in Impl.InParams) {

-                        if (IsUniform(Impl.Name, v.Name)) {

-                            SetNonUniform(Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams) {

-                      if (IsUniform(Impl.Name, v.Name)) {

-                         SetNonUniform(Impl.Name, v.Name);

-                      }

-                    }

-                        
-                    return;
-                }
-
-                Graph<Block> blockGraph = prog.ProcessLoops(Impl);
-                var ctrlDep = blockGraph.ControlDependence();
-
-                // Compute transitive closure of control dependence info.
-                bool changed;
-                do
-                {
-                    changed = false;
-                    foreach (var depEntry in ctrlDep)
-                    {
-                        var newDepSet = new HashSet<Block>(depEntry.Value);
-                        foreach (var dep in depEntry.Value)
-                        {
-                            if (ctrlDep.ContainsKey(dep))
-                                newDepSet.UnionWith(ctrlDep[dep]);
-                        }
-                        if (newDepSet.Count != depEntry.Value.Count)
-                        {
-                            depEntry.Value.UnionWith(newDepSet);
-                            changed = true;
-                        }
-                    }
-                } while (changed);
-
-                var nonUniformBlockSet = new HashSet<Block>();
-                nonUniformBlocks[Impl.Name] = nonUniformBlockSet;

-

-                do {

-                  changed = false;

-                  foreach (var block in Impl.Blocks) {

-                    bool uniform = !nonUniformBlockSet.Contains(block);

-                    bool newUniform = Analyse(Impl, block.Cmds, uniform);

-                    if (uniform && !newUniform) {

-                      changed = true;

-                      nonUniformBlockSet.Add(block);

-                      Block pred = blockGraph.Predecessors(block).Single();

-                      if (ctrlDep.ContainsKey(pred))

-                        nonUniformBlockSet.UnionWith(ctrlDep[pred]);

-                    }

-                  }

-                } while (changed);

-            }
-            else
-            {
-                Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);
-            }
-        }
-
-
-        private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)
-        {
-            ControlFlowIsUniform &= !hitNonuniformReturn;
-            foreach (BigBlock bb in stmtList.BigBlocks)
-            {
-                Analyse(impl, bb, ControlFlowIsUniform);
-            }
-        }
-
-        private Implementation GetImplementation(string procedureName)
-        {
-            foreach (Declaration D in prog.TopLevelDeclarations)
-            {
-                if (D is Implementation && ((D as Implementation).Name == procedureName))
-                {
-                    return D as Implementation;
-                }
-            }
-            return null;
-        }
-
-        private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)
-        {
-            ControlFlowIsUniform &= !hitNonuniformReturn;
-            Analyse(impl, bb.simpleCmds, ControlFlowIsUniform);
-
-            if (bb.ec is WhileCmd)
-            {
-                WhileCmd wc = bb.ec as WhileCmd;
-                loopStack.Add(wc);
-                Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) && 
-                    !nonUniformLoops[impl.Name].Contains(GetLoopId(wc)));
-                loopStack.RemoveAt(loopStack.Count - 1);
-            }
-            else if (bb.ec is IfCmd)
-            {
-                IfCmd ifCmd = bb.ec as IfCmd;
-                Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
-                if (ifCmd.elseBlock != null)
-                {
-                    Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
-                }
-                Debug.Assert(ifCmd.elseIf == null);
-            }
-            else if (bb.ec is BreakCmd)
-            {
-                if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1])))
-                {
-                    SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]);
-                }
-            }
-
-            if (bb.tc is ReturnCmd && !ControlFlowIsUniform)
-            {
-                hitNonuniformReturn = true;
-                if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))
-                {
-                    SetNonUniform(impl.Name, loopStack[0]);
-                    loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));
-                }
-            }
-
-
-        }
-
-        private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)
-        {
-            foreach (Cmd c in cmdSeq)
-            {
-                if (c is AssignCmd)
-                {
-                    AssignCmd assignCmd = c as AssignCmd;
-                    foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
-                    {

-
-                        if (a.Item1 is SimpleAssignLhs)
-                        {
-                            SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs;

-                            Expr rhs = a.Item2;

-                            if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
-                                (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
-                            {

-                                SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
-                            }

-

-                        }
-                    }
-                }
-                else if (c is HavocCmd)
-                {
-                    HavocCmd havocCmd = c as HavocCmd;
-                    foreach(IdentifierExpr ie in havocCmd.Vars)
-                    {
-                        if(IsUniform(impl.Name, ie.Decl.Name)) {
-                            SetNonUniform(impl.Name, ie.Decl.Name);
-                        }
-                    }
-                }
-                else if (c is CallCmd)
-                {
-                    CallCmd callCmd = c as CallCmd;
-                    Implementation CalleeImplementation = GetImplementation(callCmd.callee);
-
-                    if (CalleeImplementation != null)
-                    {
-
-                        if (!ControlFlowIsUniform)
-                        {
-                            if (IsUniform(callCmd.callee))
-                            {
-                                SetNonUniform(callCmd.callee);
-                            }
-                        }
-                        for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
-                        {
-                            if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
-                                && !IsUniform(impl.Name, callCmd.Ins[i]))
-                            {
-                                SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
-                            }
-                        }
-
-                        for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
-                        {
-                            if (IsUniform(impl.Name, callCmd.Outs[i].Name)
-                                && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
-                            {
-                                SetNonUniform(impl.Name, callCmd.Outs[i].Name);
-                            }
-                        }
-
-                    }
-                }
-                else if (c is AssumeCmd)
-                {
-                    var ac = (AssumeCmd)c;
-                    if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
-                        !IsUniform(impl.Name, ac.Expr))
-                    {

-                      ControlFlowIsUniform = false;

-                    }
-                }
-            }
-
-            return ControlFlowIsUniform;
-        }
-
-        private int GetLoopId(WhileCmd wc)
-        {
-            AssertCmd inv = wc.Invariants[0] as AssertCmd;
-            Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
-            return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
-        }
-
-        private void SetNonUniform(string procedureName)
-        {
-            uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
-                (false, uniformityInfo[procedureName].Value);
-            RecordProcedureChanged();
-        }
-
-        private void SetNonUniform(string procedureName, WhileCmd wc)
-        {
-            nonUniformLoops[procedureName].Add(GetLoopId(wc));
-            RecordProcedureChanged();
-        }
-
-        public bool IsUniform(string procedureName)
-        {
-            if (!uniformityInfo.ContainsKey(procedureName))
-            {
-                return false;
-            }
-            return uniformityInfo[procedureName].Key;
-        }
-
-        public bool IsUniform(string procedureName, Block b)
-        {
-            if (!nonUniformBlocks.ContainsKey(procedureName))
-            {
-                return false;
-            }
-            return !nonUniformBlocks[procedureName].Contains(b);
-        }
-
-        class UniformExpressionAnalysisVisitor : StandardVisitor {
-
-          private bool isUniform = true;
-          private Dictionary<string, bool> uniformityInfo;
-
-          public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
-            this.uniformityInfo = uniformityInfo;
-          }
-
-          public override Variable VisitVariable(Variable v) {
-            if (!uniformityInfo.ContainsKey(v.Name)) {
-              isUniform = isUniform && (v is Constant);
-            } else if (!uniformityInfo[v.Name]) {
-              isUniform = false;
-            }
-
-            return v;
-          }
-
-          internal bool IsUniform() {
-            return isUniform;
-          }
-        }
-
-        public bool IsUniform(string procedureName, Expr expr)
-        {
-            UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
-            visitor.VisitExpr(expr);
-            return visitor.IsUniform();
-        }
-
-        public bool IsUniform(string procedureName, string v)
-        {
-            if (!uniformityInfo.ContainsKey(procedureName))
-            {
-                return false;
-            }
-
-            if (!uniformityInfo[procedureName].Value.ContainsKey(v))
-            {
-                return false;
-            }
-            return uniformityInfo[procedureName].Value[v];
-        }
-
-        private void SetUniform(string procedureName, string v)
-        {
-            uniformityInfo[procedureName].Value[v] = true;
-            RecordProcedureChanged();
-        }
-
-        private void RecordProcedureChanged()
-        {
-            ProcedureChanged = true;
-        }
-
-        private void SetNonUniform(string procedureName, string v)
-        {
-            uniformityInfo[procedureName].Value[v] = false;
-            RecordProcedureChanged();
-        }
-
-        public void dump()
-        {
-            foreach (string p in uniformityInfo.Keys)
-            {
-                Console.WriteLine("Procedure " + p + ": "
-                    + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
-                foreach (string v in uniformityInfo[p].Value.Keys)
-                {
-                    Console.WriteLine("  " + v + ": " +
-                        (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
-                }
-                Console.Write("Ins [");
-                for (int i = 0; i < inParameters[p].Count; i++)
-                {
-                    Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
-                }
-                Console.WriteLine("]");
-                Console.Write("Outs [");
-                for (int i = 0; i < outParameters[p].Count; i++)
-                {
-                    Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
-                }
-                Console.WriteLine("]");
-                Console.Write("Non-uniform loops:");
-                foreach (int l in nonUniformLoops[p])
-                {
-                    Console.Write(" " + l);
-                }
-                Console.WriteLine();
-                Console.Write("Non-uniform blocks:");
-                foreach (Block b in nonUniformBlocks[p])
-                {
-                    Console.Write(" " + b.Label);
-                }
-                Console.WriteLine();
-            }
-        }
-
-
-        public string GetInParameter(string procName, int i)
-        {
-            return inParameters[procName][i];
-        }
-
-        public string GetOutParameter(string procName, int i)
-        {
-            return outParameters[procName][i];
-        }
-
-
-        public bool knowsOf(string p)
-        {
-            return uniformityInfo.ContainsKey(p);
-        }
-
-        public void AddNonUniform(string proc, string v)
-        {
-            if (uniformityInfo.ContainsKey(proc))
-            {
-                Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
-                uniformityInfo[proc].Value[v] = false;
-            }
-        }

-

-        public void AddNonUniform(string proc, Block b) {

-          if (nonUniformBlocks.ContainsKey(proc)) {

-            Debug.Assert(!nonUniformBlocks[proc].Contains(b));

-            nonUniformBlocks[proc].Add(b);

-          }

-        }
-
-        public bool IsUniform(string proc, WhileCmd wc)
-        {
-            if (unstructured)
-                return false;
-
-            return !nonUniformLoops[proc].Contains(GetLoopId(wc));
-        }
-
-        public bool HasNonuniformReturn(string proc, WhileCmd whileCmd)
-        {
-            return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd));
-        }
-    }
-
-}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6efae58c..b13b7e35 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -11,7 +11,7 @@ using System.Linq;
 using System.Threading;

 using System.IO;

 using Microsoft.Boogie;

-using Graphing;

+using Microsoft.Boogie.GraphUtil;

 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

@@ -2058,12 +2058,6 @@ namespace VC {
       }

       #endregion

 

-      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining == 0) {

-        DesugarCalls(impl);

-        BlockPredicator.Predicate(program, impl);

-        impl.ComputePredecessorsForBlocks();

-      }

-

       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }

@@ -3038,36 +3032,6 @@ namespace VC {
       }

     }

 

-    /// <summary>

-    /// Simplifies the CFG of the given implementation impl by merging each

-    /// basic block with a single predecessor into that predecessor if the

-    /// predecessor has a single successor.  If a uniformity analyser is

-    /// being used then block will only be merged if they are both uniform

-    /// or both non-uniform

-    /// </summary>

-    public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni) {

-      var blockGraph = prog.ProcessLoops(impl);

-      var predMap = new Dictionary<Block, Block>();

-      foreach (var block in blockGraph.Nodes) {

-        try {

-          var pred = blockGraph.Predecessors(block).Single();

-          if (blockGraph.Successors(pred).Single() == block &&

-              (uni == null || 

-              (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||

-              (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block)))) {

-            Block predMapping;

-            while (predMap.TryGetValue(pred, out predMapping))

-              pred = predMapping;

-            pred.Cmds.AddRange(block.Cmds);

-            pred.TransferCmd = block.TransferCmd;

-            impl.Blocks.Remove(block);

-            predMap[block] = pred;

-          }

-        // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.

-        } catch (InvalidOperationException) {}

-      }

-    }

-

     static void DumpMap(Hashtable /*Variable->Expr*/ map) {

       Contract.Requires(map != null);

       foreach (DictionaryEntry de in map) {

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
deleted file mode 100644
index 962f9f26..00000000
--- a/Source/VCGeneration/VCDoomed.cs
+++ /dev/null
@@ -1,827 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Graphing;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC {

-  public partial class DCGen : ConditionGeneration {

-      private bool _print_time = CommandLineOptions.Clo.DoomStrategy!=-1;

-    #region Attributes

-    static private Dictionary<Block, Variable/*!*/>/*!*/ m_BlockReachabilityMap;

-    Dictionary<Block/*!*/, Block/*!*/>/*!*/ m_copiedBlocks = new Dictionary<Block/*!*/, Block/*!*/>();

-    const string reachvarsuffix = "__ivebeenthere";

-    List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>();

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-

-    }

-

-    #endregion

-

-

-    /// <summary>

-    /// Constructor.  Initializes the theorem prover.

-    /// </summary>

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

-      : base(program) {

-      Contract.Requires(program != null);

-

-      this.appendLogFile = appendLogFile;

-      this.logFilePath = logFilePath;

-      m_BlockReachabilityMap = new Dictionary<Block, Variable>();

-    }

-

-    /// <summary>

-    /// Debug method that prints a dot file of the 

-    /// current set of blocks in impl to filename. 

-    /// </summary>

-    private void Impl2Dot(Implementation impl, string filename) {

-      Contract.Requires(impl != null);

-      Contract.Requires(filename != null);

-      List<string> nodes = new List<string>();

-      List<string> edges = new List<string>();

-

-      string nodestyle = "[shape=box];";

-

-      foreach (Block b in impl.Blocks) {

-        Contract.Assert(b != null);

-        nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle));

-        GotoCmd gc = b.TransferCmd as GotoCmd;

-        if (gc != null)

-        {

-            Contract.Assert(gc.labelTargets != null);

-            foreach (Block b_ in gc.labelTargets)

-            {

-                Contract.Assert(b_ != null);

-                edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));

-            }

-        }

-

-        //foreach (Block b_ in b.Predecessors)

-        //{              

-        //    edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));

-        //}

-      }

-        

-      using (StreamWriter sw = new StreamWriter(filename)) {

-        sw.WriteLine(String.Format("digraph {0} {{", impl.Name));

-        //            foreach (string! s in nodes) {

-        //                sw.WriteLine(s);

-        //            }

-        foreach (string s in edges) {

-          Contract.Assert(s != null);

-          sw.WriteLine(s);

-        }

-        sw.WriteLine("}}");

-        sw.Close();

-      }

-    }

-    private const string _copyPrefix = "CPY__";

-

-    private List<Block> m_UncheckableBlocks = null;

-

-      /// <summary>

-    /// MSchaef: 

-    /// - remove loops and add reach variables

-    /// - make it a passive program

-    /// - compute the wlp for each block

-    /// - check if |= (reach=false) => wlp.S.false holds for each reach

-    ///

-    /// </summary>

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

-      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-      

-      Console.WriteLine();

-      Console.WriteLine("Checking function {0}", impl.Name);

-      callback.OnProgress("doomdetector", 0, 0, 0);

-

-      bool restartTP = CommandLineOptions.Clo.DoomRestartTP ;

-

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

-

-      Transform4DoomedCheck(impl);

-

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

-    

-      Checker checker = FindCheckerFor(impl, 1000);

-      Contract.Assert(checker != null);

-      int assertionCount;

-      DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);

-      CumulativeAssertionCount += assertionCount;

-

-      //EmitImpl(impl, false);

-      

-      int _totalchecks = 0;

-

-      ProverInterface.Outcome outcome;

-      dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);

-

-      System.TimeSpan ts = new TimeSpan();

-      

-      if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count);

-

-      List<Block> lb;

-      List<Variable> lv = new List<Variable>();

-      

-      while (dc.GetNextBlock(out lb))

-      {

-        Contract.Assert(lb != null);

-        outcome = ProverInterface.Outcome.Undetermined;

-        

-        Variable v = null;

-        lv.Clear();

-

-        foreach (Block b_ in lb)

-        {

-            if (!m_BlockReachabilityMap.TryGetValue(b_, out v))

-            {

-                // This should cause an error

-                continue;

-            }

-            //Console.Write("{0}, ",b_.Label);

-            lv.Add(v);

-        }

-        //Console.WriteLine();

-        Dictionary<Expr, int> finalreachvars = m_GetPostconditionVariables(impl.Blocks,lb);

-        if (lv.Count < 1)

-        {

-            

-            continue;

-        }

-

-        Contract.Assert(lv != null);

-        _totalchecks++;

-

-

-        if (!dc.CheckLabel(lv,finalreachvars, out outcome)) {

-          return Outcome.Inconclusive;

-        }

-        ts += dc.DEBUG_ProverTime.Elapsed;

-

-        if (restartTP)

-        {

-            checker.Close();

-            checker = FindCheckerFor(impl, 1000);

-            dc.RespawnChecker(impl, checker);

-            dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);

-        }

-

-      }

-      checker.Close();

-

-      if (_print_time)

-      {

-          Console.WriteLine("Number of Checkes / #Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count);

-          dc.__DEBUG_PrintStatistics();

-          Console.WriteLine("Total time for this method: {0}", ts.ToString());

-      }

-      #region Try to produce a counter example (brute force)

-      if (dc.DoomedSequences.Count > 0) {

-          int counter = 0;

-          List<Block> _all = new List<Block>();

-          foreach (List<Block> lb_ in dc.DoomedSequences)

-          {              

-              foreach (Block b_ in lb_)

-              {

-                  if (!_all.Contains(b_) && !m_UncheckableBlocks.Contains(b_)) 

-                  { 

-                      _all.Add(b_); counter++;

-                      if (!_print_time)  Console.WriteLine(b_.Label);

-                  }

-              }

-          }

-          if (_all.Count > 0)

-          {

-              Console.WriteLine("#Dead Blocks found: {0}:  ", counter);

-              return Outcome.Errors;

-          }

-      }

-      #endregion

-

-

-      return Outcome.Correct;

-    }

-

-    private Dictionary<Expr, int> m_GetPostconditionVariables(List<Block> allblock,  List<Block> passBlock)

-    {

-        Dictionary<Expr, int> r = new Dictionary<Expr, int>();        

-        foreach (Block b in allblock)

-        {            

-            Variable v;

-            if (m_BlockReachabilityMap.TryGetValue(b, out v))

-            {

-                if (passBlock.Contains(b))   r[m_LastReachVarIncarnation[v]] = 1;

-            }

-            else

-            {

-                Console.WriteLine("there is no reachability variable for {0}", b.Label);

-            }

-        }

-        return r;

-    }

-

-#if false

-    #region Error message construction

-    private void SearchCounterexample(Implementation impl, DoomErrorHandler errh, VerifierCallback callback) {

-      Contract.Requires(impl != null);

-      Contract.Requires(errh != null);

-      Contract.Requires(callback != null);

-      Contract.Requires(errh.m_Reachvar != null);

-      //if (errh.m_Reachvar==null) {

-      //    Contract.Assert(false);throw new cce.UnreachableException();

-      //}

-      m_doomedCmds.Clear();

-

-      Dictionary<Block, CmdSeq> cmdbackup = new Dictionary<Block, CmdSeq>();

-

-      BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count / 2 - 1);

-      BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count / 2, impl.Blocks.Count - 1);

-

-      List<Cmd> causals = CollectCausalStatements(impl.Blocks[0]);

-      foreach (Cmd c in causals) {

-        Contract.Assert(c != null);

-        GenerateErrorMessage(c, causals);

-      }

-

-      #region Undo all modifications

-      foreach (KeyValuePair<Block, CmdSeq> kvp in cmdbackup) {

-        Contract.Assert(kvp.Key != null);

-        Contract.Assert(kvp.Value != null);

-        kvp.Key.Cmds = kvp.Value;

-      }

-      #endregion

-    }

-

-    #region Causal Statement Tree

-

-    private void GenerateErrorMessage(Cmd causalStatement, List<Cmd> causals) {

-      Contract.Requires(causalStatement != null);

-      Contract.Requires(cce.NonNullElements(causals));

-      AssumeCmd uc = causalStatement as AssumeCmd;

-      AssertCmd ac = causalStatement as AssertCmd;

-      ConsoleColor col = Console.ForegroundColor;

-

-      // Trivial case. Must be either assume or assert false

-      if (m_doomedCmds.Count == 1) {

-        Console.WriteLine("Found a trivial error:");

-        if (uc != null) {

-          Console.Write("Trivial false assumption: ");

-          Console.Write("({0};{1}):", uc.tok.line, uc.tok.col);

-        }

-        if (ac != null) {

-          Console.Write("Trivial false assertion: ");

-          Console.Write("({0};{1}):", ac.tok.line, ac.tok.col);

-        }

-        causalStatement.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-      } else {

-        // Safety error

-        if (ac != null) {

-          Console.ForegroundColor = ConsoleColor.Red;

-          Console.WriteLine("Safety error:");

-          Console.ForegroundColor = col;

-          Console.Write("This assertion is violated: ");

-          Console.Write("({0};{1}):", ac.tok.line, ac.tok.col);

-          ac.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-        }

-        if (uc != null) {

-          bool containsAssert = false;

-          foreach (Cmd c in m_doomedCmds) {

-            Contract.Assert(c != null);

-            if (causals.Contains(c)) {

-              continue;

-            }

-            AssertCmd asrt = c as AssertCmd;

-            if (asrt != null) {

-              containsAssert = true;

-              break;

-            }

-          }

-          // Plausibility error

-          if (containsAssert) {

-            Console.ForegroundColor = ConsoleColor.Yellow;

-            Console.WriteLine("Plausibility error:");

-            Console.ForegroundColor = col;

-            Console.Write("There is no legal exeuction passing: ");

-            Console.Write("({0};{1})", uc.tok.line, uc.tok.col);

-            uc.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-          } else { // Reachability error

-            Console.ForegroundColor = ConsoleColor.DarkRed;

-            Console.WriteLine("Reachability error:");

-            Console.ForegroundColor = col;

-            Console.Write("No execution can reach: ");

-            Console.Write("({0};{1})", uc.tok.line, uc.tok.col);

-            uc.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-          }

-

-        }

-

-        Console.ForegroundColor = ConsoleColor.White;

-        Console.WriteLine("...on any execution passing through:");

-        foreach (Cmd c in m_doomedCmds) {

-          Contract.Assert(c != null);

-          if (causals.Contains(c)) {

-            continue;

-          }

-          Console.ForegroundColor = col;

-          Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col);

-          Console.ForegroundColor = ConsoleColor.DarkYellow;

-          c.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-        }

-        Console.ForegroundColor = col;

-        Console.WriteLine("--");

-

-      }

-    }

-

-    private List<Cmd> CollectCausalStatements(Block b) {

-      Contract.Requires(b != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Cmd>>()));

-

-      Cmd lastCausal = null;

-      foreach (Cmd c in b.Cmds) {

-        Contract.Assert(c != null);

-        AssertCmd ac = c as AssertCmd;

-        AssumeCmd uc = c as AssumeCmd;

-        if (ac != null && !ContainsReachVariable(ac)) {

-          if (ac.Expr != Expr.True) {

-            lastCausal = c;

-          }

-        } else if (uc != null && !ContainsReachVariable(uc)) {

-          lastCausal = c;

-        }

-      }

-

-      List<Cmd> causals = new List<Cmd>();

-      GotoCmd gc = b.TransferCmd as GotoCmd;

-      if (gc != null && gc.labelTargets != null) {

-        List<Cmd> tmp;

-        //bool allcausal = true;

-        foreach (Block b_ in gc.labelTargets) {

-          Contract.Assert(b_ != null);

-          tmp = CollectCausalStatements(b_);

-

-          foreach (Cmd cau in tmp) {

-            if (!causals.Contains(cau))

-              causals.Add(cau);

-          }

-        }

-        //if (allcausal) 

-        if (causals.Count > 0)

-          return causals;

-      }

-      if (lastCausal != null)

-        causals.Add(lastCausal);

-      return causals;

-    }

-

-    #endregion

-

-    bool BruteForceCESearch(Variable reachvar, Implementation impl, VerifierCallback callback,

-                        Dictionary<Block, CmdSeq> cmdbackup, int startidx, int endidx) {

-      Contract.Requires(reachvar != null);

-      Contract.Requires(impl != null);

-      Contract.Requires(callback != null);

-      Contract.Requires(cce.NonNullElements(cmdbackup));

-      #region Modify implementation

-      for (int i = startidx; i <= endidx; i++) {

-        if (_copiedBlock.Contains(impl.Blocks[i]))

-          continue;

-        CmdSeq cs = new CmdSeq();

-        cmdbackup.Add(impl.Blocks[i], impl.Blocks[i].Cmds);

-        foreach (Cmd c in impl.Blocks[i].Cmds) {

-          Contract.Assert(c != null);

-          if (ContainsReachVariable(c)) {

-            cs.Add(c);

-            continue;

-          }

-          AssertCmd ac = c as AssertCmd;

-          AssumeCmd uc = c as AssumeCmd;

-          if (ac != null) {

-            cs.Add(new AssertCmd(ac.tok, Expr.True));

-          } else if (uc != null) {

-            cs.Add(new AssertCmd(uc.tok, Expr.True));

-          } else {

-            cs.Add(c);

-          }

-        }

-        impl.Blocks[i].Cmds = cs;

-      }

-      #endregion

-

-      ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;

-      if (!ReCheckImpl(reachvar, impl, callback, out outcome)) {

-        UndoBlockModifications(impl, cmdbackup, startidx, endidx);

-        return false;

-      }

-      if (outcome == ProverInterface.Outcome.Valid) {

-        return true;

-      } else if (outcome == ProverInterface.Outcome.Invalid) {

-        UndoBlockModifications(impl, cmdbackup, startidx, endidx);

-        int mid = startidx + (endidx - startidx) / 2;

-        if (startidx >= endidx) {

-          // Now we found an interesting Block and we have to

-          // search for the interesting statements.

-          int cmdcount = impl.Blocks[endidx].Cmds.Length;

-          BruteForceCmd(impl.Blocks[endidx], 0, cmdcount / 2 - 1, reachvar, impl, callback);

-          BruteForceCmd(impl.Blocks[endidx], cmdcount / 2, cmdcount - 1, reachvar, impl, callback);

-          return true;

-        } else {

-          BruteForceCESearch(reachvar, impl, callback, cmdbackup, startidx, mid);

-          BruteForceCESearch(reachvar, impl, callback, cmdbackup, mid + 1, endidx);

-          return true;

-        }

-      } else {

-        UndoBlockModifications(impl, cmdbackup, startidx, endidx);

-        return false;

-      }

-    }

-

-    bool BruteForceCmd(Block b, int startidx, int endidx, Variable reachvar,

-                       Implementation impl, VerifierCallback callback) {

-      Contract.Requires(b != null);

-      Contract.Requires(reachvar != null);

-      Contract.Requires(impl != null);

-      Contract.Requires(callback != null);

-      #region Modify Cmds

-      CmdSeq backup = b.Cmds;

-      Contract.Assert(backup != null);

-      CmdSeq cs = new CmdSeq();

-      for (int i = 0; i < startidx; i++) {

-        cs.Add(b.Cmds[i]);

-      }

-      for (int i = startidx; i <= endidx; i++) {

-        Cmd c = b.Cmds[i];

-        if (ContainsReachVariable(c)) {

-          cs.Add(c);

-          continue;

-        }

-        cs.Add(new AssertCmd(c.tok, Expr.True));

-      }

-      for (int i = endidx + 1; i < b.Cmds.Length; i++) {

-        cs.Add(b.Cmds[i]);

-      }

-

-      b.Cmds = cs;

-      #endregion

-

-      #region Recheck

-      ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;

-      if (!ReCheckImpl(reachvar, impl, callback, out outcome)) {

-        b.Cmds = backup;

-        return false;

-      }

-      #endregion

-

-      if (outcome == ProverInterface.Outcome.Valid) {

-        return true;

-      } else if (outcome == ProverInterface.Outcome.Invalid) {

-        b.Cmds = backup;

-        if (startidx >= endidx) {

-          if (!ContainsReachVariable(b.Cmds[endidx])) {

-            //                    Console.Write("   Witness (");

-            //                    

-            //                    ConsoleColor col = Console.ForegroundColor;

-            //                    Console.ForegroundColor = ConsoleColor.White;

-            //                    Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );

-            //                    Console.ForegroundColor = col;

-            //                    Console.Write("):   ");

-            //                    Console.ForegroundColor = ConsoleColor.Yellow;

-            //                    b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-            //                    Console.ForegroundColor = col;

-

-            m_doomedCmds.Add(b.Cmds[endidx]);

-            return true;

-          } else {

-            return false;

-          }

-        } else {

-          int mid = startidx + (endidx - startidx) / 2;

-          BruteForceCmd(b, startidx, mid, reachvar, impl, callback);

-          BruteForceCmd(b, mid + 1, endidx, reachvar, impl, callback);

-          return false; // This is pure random

-        }

-      } else {

-        b.Cmds = backup;

-        return false;

-      }

-    }

-

-    void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,

-                                int startidx, int endidx) {

-      Contract.Requires(cce.NonNullElements(cmdbackup));

-      Contract.Requires(impl != null);

-      for (int i = startidx; i <= endidx; i++) {

-        CmdSeq cs = null;

-        if (cmdbackup.TryGetValue(impl.Blocks[i], out cs)) {

-          Contract.Assert(cs != null);

-          impl.Blocks[i].Cmds = cs;

-          cmdbackup.Remove(impl.Blocks[i]);

-        }

-      }

-    }

-

-    bool ReCheckImpl(Variable reachvar, Implementation impl, VerifierCallback callback,

-                     out ProverInterface.Outcome outcome) {

-      Contract.Requires(reachvar != null);

-      Contract.Requires(impl != null);

-      Contract.Requires(callback != null);

-      Checker checker = FindCheckerFor(impl, 1000);

-      Contract.Assert(checker != null);

-      DoomCheck dc = new DoomCheck(impl, this.exitBlock,  checker, m_UncheckableBlocks);

-      dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);

-      outcome = ProverInterface.Outcome.Undetermined;

-      List<Variable> rv = new List<Variable>();

-      rv.Add(reachvar);

-      if (!dc.CheckLabel(rv,null, out outcome)) {

-        checker.Close();

-        return false;

-      }

-      checker.Close();

-      return true;

-    }

-

-

-

-    bool ContainsReachVariable(Cmd c) {

-      Contract.Requires(c != null);

-      AssertCmd artc = c as AssertCmd;

-      AssumeCmd amec = c as AssumeCmd;

-      Expr e;

-      if (artc != null) {

-        e = artc.Expr;

-      } else if (amec != null) {

-        e = amec.Expr;

-      } else {

-        return false;

-      }

-      Set freevars = new Set();

-      e.ComputeFreeVariables(freevars);

-      foreach (Variable v in freevars) {

-        Contract.Assert(v != null);

-        if (v.Name.Contains(reachvarsuffix))

-          return true;

-      }

-      return false;

-    }

-#endregion

-#endif

-

-

-    Block exitBlock;

-

-    #region Program Passification

-    private void GenerateHelperBlocks(Implementation impl) {

-      Contract.Requires(impl != null);

-      Hashtable gotoCmdOrigins = new Hashtable();

-      exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

-      Contract.Assert(exitBlock != null);

-

-      AddBlocksBetween(impl.Blocks);

-

-      #region Insert pre- and post-conditions and where clauses as assume and assert statements

-      {

-        CmdSeq cc = new CmdSeq();

-        // where clauses of global variables

-        foreach (Declaration d in program.TopLevelDeclarations) {

-          GlobalVariable gvar = d as GlobalVariable;

-          if (gvar != null && gvar.TypedIdent.WhereExpr != null) {

-            Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

-            cc.Add(c);

-          }

-        }

-        // where clauses of in- and out-parameters

-        cc.AddRange(GetParamWhereClauses(impl));

-        // where clauses of local variables

-        foreach (Variable lvar in impl.LocVars) {

-          Contract.Assert(lvar != null);

-          if (lvar.TypedIdent.WhereExpr != null) {

-            Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);

-            cc.Add(c);

-          }

-        }

-

-        // add cc and the preconditions to new blocks preceding impl.Blocks[0]

-        InjectPreconditions(impl, cc);

-

-        // append postconditions, starting in exitBlock and continuing into other blocks, if needed

-        exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);

-      }

-      #endregion     

-    }

-

-

-    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {

-      Contract.Requires(impl != null);

-      Contract.Requires(mvInfo != null);

-      Contract.Requires(this.exitBlock != null);

-      Contract.Ensures(Contract.Result<Hashtable>() != null);

-      

-      CurrentLocalVariables = impl.LocVars;

-      return Convert2PassiveCmd(impl, mvInfo);

-      //return new Hashtable();

-    }

-

-    /// <summary>

-    /// Add additional variable to allow checking as described in the paper

-    /// "It's doomed; we can prove it"

-    /// </summary>

-    private CmdSeq GenerateReachabilityPredicates(Implementation impl)

-    {

-        Contract.Requires(impl != null);        

-        

-        foreach (Block b in impl.Blocks)

-        {

-            Contract.Assert(b != null);

-            //if (b.Predecessors.Length==0) continue;

-            //if (b.Cmds.Length == 0 ) continue;

-            

-            Variable v_ = new LocalVariable(Token.NoToken,

-                                    new TypedIdent(b.tok, b.Label + reachvarsuffix, new BasicType(SimpleType.Int )));

-

-            impl.LocVars.Add(v_);                      

-            

-            m_BlockReachabilityMap[b] = v_;

-

-            IdentifierExpr lhs = new IdentifierExpr(b.tok, v_);

-            Contract.Assert(lhs != null);

-

-            impl.Proc.Modifies.Add(lhs);

-          

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

-            lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs));

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

-            rhsl.Add(Expr.Literal(1) );

-            

-

-            CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));

-            cs.AddRange(b.Cmds);

-            b.Cmds = cs;

-

-            //checkBlocks.Add(new CheckableBlock(v_,b));

-        }

-

-        CmdSeq incReachVars = new CmdSeq();

-        foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)

-        {

-            IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value);

-            impl.Proc.Modifies.Add(lhs);

-            incReachVars.Add(new AssumeCmd(Token.NoToken, Expr.Le(lhs, Expr.Literal(1))));                        

-        }

-

-        return incReachVars;

-    }

- 

-    #endregion

-

-    #region Compute loop-free approximation

-

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

-    {

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

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

-        if (impl.Blocks.Count < 1) return;

-

-        impl.PruneUnreachableBlocks();

-        AddBlocksBetween(impl.Blocks);

-        ResetPredecessors(impl.Blocks);        

-

-        GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks);

-        LoopRemover lr = new LoopRemover(ga);

-        lr.AbstractLoopUnrolling();

-

-        impl.Blocks = ga.ToImplementation(out m_UncheckableBlocks);

-        ResetPredecessors(impl.Blocks);

-

-        // Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks

-        List<Block> oldblocks = new List<Block>();

-        oldblocks.AddRange(impl.Blocks);       

-        GenerateHelperBlocks(impl);

-        #region Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks

-        foreach (Block b in impl.Blocks)

-        {

-            if (oldblocks.Contains(b)) continue;

-            GotoCmd gc = b.TransferCmd as GotoCmd;

-            if (gc != null)

-            {

-                bool allsuccUncheckable = true;

-                foreach (Block _b in gc.labelTargets)

-                {

-                    if (!m_UncheckableBlocks.Contains(_b))

-                    {

-                        allsuccUncheckable = false; break;

-                    }

-                }

-                if (allsuccUncheckable && !m_UncheckableBlocks.Contains(b)) m_UncheckableBlocks.Add(b);

-            }

-        }

-        #endregion

-

-        impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks);

-

-        m_BlockReachabilityMap = new Dictionary<Block, Variable>();       

-        CmdSeq cs = GenerateReachabilityPredicates(impl);

-        

-        //foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))

-        //{

-        //    test.Cmds.AddRange(cs);

-        //}

-        

-        ResetPredecessors(impl.Blocks);

-        //EmitImpl(impl,false);

-

-        Hashtable/*Variable->Expr*/ htbl = PassifyProgram(impl, new ModelViewInfo(program, impl));

-

-        // Collect the last incarnation of each reachability variable in the passive program

-        foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)

-        {

-            if (htbl.ContainsKey(kvp.Value))

-            {

-                m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[kvp.Value];

-            }

-        }

-    }

-

-

-    List<Block> getTheFFinalBlock(Block b)

-    {

-        List<Block> lb = new List<Block>();

-        GotoCmd gc = b.TransferCmd as GotoCmd;

-        if (gc == null) lb.Add(b);

-        else

-        {

-            foreach (Block s in gc.labelTargets)

-            {

-                foreach (Block r in getTheFFinalBlock(s)) if (!lb.Contains(r)) lb.Add(r);

-            }

-        }

-        return lb;

-    }

-

-

-    private List<Block> DeepCopyBlocks(List<Block> lb, List<Block> uncheckables)

-    {

-        List<Block> clones = new List<Block>();

-        List<Block> uncheck_ = new List<Block>();

-        Dictionary<Block, Block> clonemap = new Dictionary<Block, Block>();

-

-        foreach (Block b in lb)

-        {

-            Block clone = CloneBlock(b);

-            clones.Add(clone);

-            clonemap[b] = clone;

-            if (uncheckables.Contains(b)) uncheck_.Add(clone);

-        }

-        uncheckables.Clear();

-        uncheckables.AddRange(uncheck_);

-        // update the successors and predecessors

-        foreach (Block b in lb)

-        {

-            BlockSeq newpreds = new BlockSeq();

-            foreach (Block b_ in b.Predecessors)

-            {

-                newpreds.Add(clonemap[b_]);

-            }

-            clonemap[b].Predecessors = newpreds;

-            GotoCmd gc = b.TransferCmd as GotoCmd;

-            ReturnCmd rc = b.TransferCmd as ReturnCmd;

-            if (gc != null)

-            {

-                StringSeq lseq = new StringSeq();

-                BlockSeq bseq = new BlockSeq();

-                foreach (string s in gc.labelNames) lseq.Add(s);

-                foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]);

-                GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq);

-                clonemap[b].TransferCmd = tcmd;

-            }

-            else if (rc != null)

-            {

-                clonemap[b].TransferCmd = new ReturnCmd(rc.tok);

-            }

-        }

-        return clones;

-    }

-

-    private Block CloneBlock(Block b)

-    {

-        Block clone = new Block(b.tok, b.Label, b.Cmds, b.TransferCmd);

-        if (this.exitBlock == b) this.exitBlock = clone;

-        return clone;

-    }

-    #endregion

-  }

-}

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 98958c66..0c98a891 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -144,22 +144,12 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

-    <Compile Include="BlockPredicator.cs" />

     <Compile Include="Check.cs" />

     <Compile Include="ConditionGeneration.cs" />

     <Compile Include="Context.cs" />

-    <Compile Include="DoomCheck.cs" />

-    <Compile Include="DoomedLoopUnrolling.cs" />

-    <Compile Include="DoomedStrategy.cs" />

-    <Compile Include="DoomErrorHandler.cs" />

-    <Compile Include="GraphAlgorithms.cs" />

-    <Compile Include="HasseDiagram.cs" />

     <Compile Include="OrderingAxioms.cs" />

-    <Compile Include="SmartBlockPredicator.cs" />

     <Compile Include="StratifiedVC.cs" />

-    <Compile Include="UniformityAnalyser.cs" />

     <Compile Include="VC.cs" />

-    <Compile Include="VCDoomed.cs" />

     <Compile Include="..\version.cs" />

     <Compile Include="Wlp.cs" />

   </ItemGroup>