Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

7 files changed, 3106 insertions, 3106 deletions

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 83de03ff..c1d6736f 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -1,407 +1,407 @@
-//-----------------------------------------------------------------------------

-//

-// 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 Microsoft.Boogie.GraphUtil;

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

-            try

-            {

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

-              m_Checker.ProverTask.Wait();

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

-            }

-            finally

-            {

-              m_Checker.GoBackToIdle();

-            }

-            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 Dictionary<int, Absy> 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 Dictionary<int, Absy>(); // This is only a dummy

-            m_Evc = new Evc(check);

-            Dictionary<int, Absy> 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 Dictionary<int, Absy>(); // This is only a dummy

-            m_Evc = new Evc(check);

-            Dictionary<int, Absy> 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 Dictionary<int, Absy> 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 Dictionary<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,

-                            Dictionary<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,

-                     Dictionary<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.Count);

-              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 

-                       

-    }

-

-}

+//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.Boogie.GraphUtil;
+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);
+            try
+            {
+              m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+              m_Checker.ProverTask.Wait();
+              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;
+            }
+            finally
+            {
+              m_Checker.GoBackToIdle();
+            }
+            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 Dictionary<int, Absy> 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 Dictionary<int, Absy>(); // This is only a dummy
+            m_Evc = new Evc(check);
+            Dictionary<int, Absy> 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 Dictionary<int, Absy>(); // This is only a dummy
+            m_Evc = new Evc(check);
+            Dictionary<int, Absy> 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 Dictionary<int, Absy> 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 Dictionary<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,
+                            Dictionary<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,
+                     Dictionary<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.Count);
+              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/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index 8d89bae3..ce14ff73 100644
--- a/Source/Doomed/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -1,86 +1,86 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Microsoft.Boogie.GraphUtil;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    internal class DoomErrorHandler : ProverInterface.ErrorHandler

-    {

-

-        protected Dictionary<int, Absy> 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(Dictionary<int, Absy> 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, ProverInterface.Outcome proverOutcome)

-        {

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

-        }

-

-    }

-

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+    internal class DoomErrorHandler : ProverInterface.ErrorHandler
+    {
+
+        protected Dictionary<int, Absy> 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(Dictionary<int, Absy> 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, ProverInterface.Outcome proverOutcome)
+        {
+            // 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/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj
index 77713080..c8fb83ad 100644
--- a/Source/Doomed/Doomed.csproj
+++ b/Source/Doomed/Doomed.csproj
@@ -1,190 +1,190 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

-  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

-  <PropertyGroup>

-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProjectGuid>{884386A3-58E9-40BB-A273-B24976775553}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>Doomed</RootNamespace>

-    <AssemblyName>Doomed</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>

-    <ProductVersion>12.0.0</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>True</CodeContractsEnumObligations>

-    <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>

-    <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>

-    <CodeContractsRedundantTests>True</CodeContractsRedundantTests>

-    <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>

-    <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>

-    <CodeContractsInferRequires>True</CodeContractsInferRequires>

-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

-    <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>

-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>

-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>

-    <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>

-    <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>

-    <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>

-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>

-    <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsSQLServerOption />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>

-    <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>

-    <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>

-    <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>

-    <CodeContractsInferRequires>True</CodeContractsInferRequires>

-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>

-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>

-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsSQLServerOption />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>

-    <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-  </PropertyGroup>

-  <PropertyGroup>

-    <SignAssembly>true</SignAssembly>

-  </PropertyGroup>

-  <PropertyGroup>

-    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\QED\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <ItemGroup>

-    <Reference Include="System" />

-    <Reference Include="System.Core" />

-    <Reference Include="System.Xml.Linq" />

-    <Reference Include="System.Data.DataSetExtensions" />

-    <Reference Include="Microsoft.CSharp" />

-    <Reference Include="System.Data" />

-    <Reference Include="System.Xml" />

-  </ItemGroup>

-  <ItemGroup>

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

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

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

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

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

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

-  </ItemGroup>

-  <ItemGroup>

-    <ProjectReference Include="..\Basetypes\Basetypes.csproj">

-      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

-      <Name>Basetypes</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

-      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

-      <Name>CodeContractsExtender</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\Core\Core.csproj">

-      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

-      <Name>Core</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\Graph\Graph.csproj">

-      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

-      <Name>Graph</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\Model\Model.csproj">

-      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

-      <Name>Model</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

-      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

-      <Name>ParserHelper</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\VCExpr\VCExpr.csproj">

-      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

-      <Name>VCExpr</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

-      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

-      <Name>VCGeneration</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

-    <Folder Include="Properties\" />

-  </ItemGroup>

-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

-       Other similar extension points exist, see Microsoft.Common.targets.

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <ProjectGuid>{884386A3-58E9-40BB-A273-B24976775553}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>Doomed</RootNamespace>
+    <AssemblyName>Doomed</AssemblyName>
+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
+    <ProductVersion>12.0.0</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>True</CodeContractsEnumObligations>
+    <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
+    <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
+    <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
+    <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+    <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
+    <CodeContractsInferRequires>True</CodeContractsInferRequires>
+    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+    <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
+    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+    <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
+    <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
+    <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
+    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+    <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsSQLServerOption />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+    <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
+    <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+    <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+    <CodeContractsInferRequires>True</CodeContractsInferRequires>
+    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsSQLServerOption />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+    <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+  </PropertyGroup>
+  <PropertyGroup>
+    <SignAssembly>true</SignAssembly>
+  </PropertyGroup>
+  <PropertyGroup>
+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+  </PropertyGroup>
+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\QED\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <ItemGroup>
+    <Reference Include="System" />
+    <Reference Include="System.Core" />
+    <Reference Include="System.Xml.Linq" />
+    <Reference Include="System.Data.DataSetExtensions" />
+    <Reference Include="Microsoft.CSharp" />
+    <Reference Include="System.Data" />
+    <Reference Include="System.Xml" />
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="DoomCheck.cs" />
+    <Compile Include="DoomedLoopUnrolling.cs" />
+    <Compile Include="DoomedStrategy.cs" />
+    <Compile Include="DoomErrorHandler.cs" />
+    <Compile Include="HasseDiagram.cs" />
+    <Compile Include="VCDoomed.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+      <Name>Basetypes</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+      <Name>CodeContractsExtender</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Core\Core.csproj">
+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+      <Name>Core</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Graph\Graph.csproj">
+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+      <Name>Graph</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Model\Model.csproj">
+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+      <Name>Model</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+      <Name>ParserHelper</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\VCExpr\VCExpr.csproj">
+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+      <Name>VCExpr</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+      <Name>VCGeneration</Name>
+    </ProjectReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Folder Include="Properties\" />
+  </ItemGroup>
+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
 </Project>
\ No newline at end of file
diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs
index 38fa99ac..0905deed 100644
--- a/Source/Doomed/DoomedLoopUnrolling.cs
+++ b/Source/Doomed/DoomedLoopUnrolling.cs
@@ -1,650 +1,650 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Microsoft.Boogie.GraphUtil;

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

-        {

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

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

-

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

-            foreach (Block b in bl)

-            {

-                Contract.Assert(b != null);

-                foreach (Cmd c in b.Cmds)

-                {

-                    Contract.Assert(c != null);

-                    c.AddAssignedVariables(varsToHavoc);

-                }

-            }

-            List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();

-            foreach (Variable v in varsToHavoc)

-            {

-                Contract.Assert(v != null);

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

-                if (!havocExprs.Contains(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 List<Block>();

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

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

-                {

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

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

-        {

-            List<Cmd> cmds = new List<Cmd>(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

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+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)
+        {
+            List<Cmd> cs = new List<Cmd>();
+            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);
+
+            List<Variable> varsToHavoc = new List<Variable>();
+            foreach (Block b in bl)
+            {
+                Contract.Assert(b != null);
+                foreach (Cmd c in b.Cmds)
+                {
+                    Contract.Assert(c != null);
+                    c.AddAssignedVariables(varsToHavoc);
+                }
+            }
+            List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();
+            foreach (Variable v in varsToHavoc)
+            {
+                Contract.Assert(v != null);
+                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+                if (!havocExprs.Contains(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 List<Block>();
+                foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);
+                if (kvp.Value.Suc.Count > 0)
+                {
+                    List<Block> bs = new List<Block>();                    
+                    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)
+        {
+            List<Cmd> cmds = new List<Cmd>(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/Doomed/DoomedStrategy.cs b/Source/Doomed/DoomedStrategy.cs
index 9e280873..76261827 100644
--- a/Source/Doomed/DoomedStrategy.cs
+++ b/Source/Doomed/DoomedStrategy.cs
@@ -1,528 +1,528 @@
-//-----------------------------------------------------------------------------

-//

-// 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 Microsoft.Boogie.GraphUtil;

-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.Count > 1) branchingdepth--;

-

-            GotoCmd gc = b.TransferCmd as GotoCmd;

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

-            plen++;

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

-            {

-                if (gc.labelTargets.Count > 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

-

+//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.Boogie.GraphUtil;
+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.Count > 1) branchingdepth--;
+
+            GotoCmd gc = b.TransferCmd as GotoCmd;
+            if (__DEBUG_minelements.Contains(b)) leavespp++;
+            plen++;
+            if (gc != null && gc.labelTargets.Count>0)
+            {
+                if (gc.labelTargets.Count > 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/Doomed/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs
index ad3d487e..c866662e 100644
--- a/Source/Doomed/HasseDiagram.cs
+++ b/Source/Doomed/HasseDiagram.cs
@@ -1,424 +1,424 @@
-//-----------------------------------------------------------------------------

-//

-// 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 Microsoft.Boogie.GraphUtil;

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

-                List<Block> 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);

-

-                List<Block> 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 List<Block> 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 List<Block> m_Succecessors(Block b, bool forward)

-        {

-            return m_Predecessors(b, !forward);

-        }

-

-

-    }

-

+//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.Boogie.GraphUtil;
+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);
+                List<Block> 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);
+
+                List<Block> 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 List<Block> 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 List<Block> m_Succecessors(Block b, bool forward)
+        {
+            return m_Predecessors(b, !forward);
+        }
+
+
+    }
+
 }
\ No newline at end of file
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index d4d4db21..822fb9c0 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -1,826 +1,826 @@
-//-----------------------------------------------------------------------------

-//

-// 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 Microsoft.Boogie.GraphUtil;

-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, List<Checker> checkers)

-      : base(program, checkers) {

-      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(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(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, List<Cmd>> cmdbackup = new Dictionary<Block, List<Cmd>>();

-

-      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, List<Cmd>> 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, List<Cmd>> 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;

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

-        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

-      List<Cmd> backup = b.Cmds;

-      Contract.Assert(backup != null);

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

-      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/*!*/, List<Cmd>/*!*/>/*!*/ cmdbackup,

-                                int startidx, int endidx) {

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

-      Contract.Requires(impl != null);

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

-        List<Cmd> 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);

-      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();

-      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

-      {

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

-        // where clauses of global variables

-        foreach (var gvar in program.GlobalVariables) {

-          if (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

-        InjectPostConditions(impl, exitBlock, gotoCmdOrigins);

-      }

-      #endregion     

-    }

-

-

-    private Dictionary<Variable, Expr> 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 List<Cmd> 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) );

-            

-

-            List<Cmd> cs = new List<Cmd> { new AssignCmd(Token.NoToken, lhsl, rhsl) };

-            cs.AddRange(b.Cmds);

-            b.Cmds = cs;

-

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

-        }

-

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

-        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 Dictionary<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>();       

-        List<Cmd> cs = GenerateReachabilityPredicates(impl);

-        

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

-        //{

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

-        //}

-        

-        ResetPredecessors(impl.Blocks);

-        //EmitImpl(impl,false);

-

-        Dictionary<Variable, Expr> var2Expr = 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 (var2Expr.ContainsKey(kvp.Value))

-            {

-                m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[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)

-        {

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

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

-            {

-                List<String> lseq = new List<String>();

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

-                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

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.Boogie.GraphUtil;
+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, List<Checker> checkers)
+      : base(program, checkers) {
+      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(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(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, List<Cmd>> cmdbackup = new Dictionary<Block, List<Cmd>>();
+
+      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, List<Cmd>> 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, List<Cmd>> 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;
+        List<Cmd> cs = new List<Cmd>();
+        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
+      List<Cmd> backup = b.Cmds;
+      Contract.Assert(backup != null);
+      List<Cmd> cs = new List<Cmd>();
+      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/*!*/, List<Cmd>/*!*/>/*!*/ cmdbackup,
+                                int startidx, int endidx) {
+      Contract.Requires(cce.NonNullElements(cmdbackup));
+      Contract.Requires(impl != null);
+      for (int i = startidx; i <= endidx; i++) {
+        List<Cmd> 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);
+      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
+      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
+      {
+        List<Cmd> cc = new List<Cmd>();
+        // where clauses of global variables
+        foreach (var gvar in program.GlobalVariables) {
+          if (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
+        InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
+      }
+      #endregion     
+    }
+
+
+    private Dictionary<Variable, Expr> 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 List<Cmd> 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) );
+            
+
+            List<Cmd> cs = new List<Cmd> { new AssignCmd(Token.NoToken, lhsl, rhsl) };
+            cs.AddRange(b.Cmds);
+            b.Cmds = cs;
+
+            //checkBlocks.Add(new CheckableBlock(v_,b));
+        }
+
+        List<Cmd> incReachVars = new List<Cmd>();
+        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 Dictionary<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>();       
+        List<Cmd> cs = GenerateReachabilityPredicates(impl);
+        
+        //foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
+        //{
+        //    test.Cmds.AddRange(cs);
+        //}
+        
+        ResetPredecessors(impl.Blocks);
+        //EmitImpl(impl,false);
+
+        Dictionary<Variable, Expr> var2Expr = 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 (var2Expr.ContainsKey(kvp.Value))
+            {
+                m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[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)
+        {
+            List<Block> newpreds = new List<Block>();
+            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)
+            {
+                List<String> lseq = new List<String>();
+                List<Block> bseq = new List<Block>();
+                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
+  }
+}