More line ending fixups.

12 files changed, 87 insertions, 87 deletions

diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index b1d16225..946814ba 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       foreach (Implementation impl in implementations) 

       { 

         impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom);

-        this.implWorkItems.Enqueue(impl);
+        this.implWorkItems.Enqueue(impl);

       }

 

       while (this.implWorkItems.Count > 0) // until fixed point reached

@@ -554,7 +554,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
           //PM: The following assertion follows from a nontrivial invariant of ArrayAssignCmd,

           //PM: which we do not have yet. Therefore, we put in an assume fo now.

           assume assmt.Index1 != null;

-          assert assmt.Index1 != null;
+          assert assmt.Index1 != null;

           // heap succession predicate

           Expr heapsucc = Expr.HeapSucc(oldHeap, newHeap, assmt.Index0, assmt.Index1);

 

@@ -735,14 +735,14 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       lattice.ToPredicate(incomingValue).DoVisit(freeVarsVisitorForA);

       lattice.ToPredicate(block.PreInvariant).DoVisit(freeVarsVisitorForB);

       

-      List<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables;
-      List<AI.IVariable!>! freeVarsOfB = freeVarsVisitorForB.FreeVariables;
+      List<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables;

+      List<AI.IVariable!>! freeVarsOfB = freeVarsVisitorForB.FreeVariables;

 

       System.Console.WriteLine("@@ Compared for block {0}:", block.Label);

       System.Console.WriteLine("@@ Incoming: {0}", lattice.ToPredicate((!) incomingValue));

-      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA));
+      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA));

       System.Console.WriteLine("@@ Previous: {0}", lattice.ToPredicate(block.PreInvariant));

-      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB));
+      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB));

       System.Console.WriteLine("@@ result = False");

       System.Console.WriteLine("@@ end Compare");

       string operation = "";

@@ -762,7 +762,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 #endif

 

           // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision

-          //    block.PreInvariant =  WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);
+          //    block.PreInvariant =  WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);

           block.PreInvariant = (AI.Lattice.Element)lattice.Widen(block.PreInvariant, incomingValue);

         }

         block.iterations++;

diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index c4f226d9..a1e88656 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -72,7 +72,7 @@ namespace Microsoft.Boogie {
         Contract.Assume(g.labelTargets != null);

         cce.BeginExpose(g.labelTargets);

         foreach (Block succ in g.labelTargets)

-        //              invariant b.currentlyTraversed;
+        //              invariant b.currentlyTraversed;

         //PM: The following loop invariant will work once properties are axiomatized

         //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

               {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index cd026393..a0d0e583 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -120,7 +120,7 @@ void ObjectInvariant()
         } else if (m is CouplingInvariant) {

           wr.WriteLine();

           PrintCouplingInvariant((CouplingInvariant)m, indent);

-          state = 2;
+          state = 2;

         } else {

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

         }

@@ -215,7 +215,7 @@ void ObjectInvariant()
       }

       wr.Write(" by ");

       PrintExpression(inv.Expr);

-      wr.WriteLine(";");
+      wr.WriteLine(";");

     }

     

     public void PrintFunction(Function f, int indent) {

@@ -287,7 +287,7 @@ void ObjectInvariant()
       }

       wr.WriteLine(method.Body == null ? ";" : "");

 

-      int ind = indent + IndentAmount;
+      int ind = indent + IndentAmount;

       PrintSpec("requires", method.Req, ind);

       PrintFrameSpecLine("modifies", method.Mod, ind);

       PrintSpec("ensures", method.Ens, ind);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 64a23393..ff658378 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -64,7 +64,7 @@ void ObjectInvariant()
     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

-      Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>();
+      Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>();

       foreach (ModuleDecl m in prog.Modules) {

         if (modules.ContainsKey(m.Name)) {

           Error(m, "Duplicate module name: {0}", m.Name);

@@ -116,12 +116,12 @@ void ObjectInvariant()
         foreach (TopLevelDecl decl in m.TopLevelDecls) 

           if (decl is ClassRefinementDecl) {

             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

-            ResolveTopLevelRefinement(rdecl);
+            ResolveTopLevelRefinement(rdecl);

             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

           }

       

       // attempt finding refinement cycles

-      List<TopLevelDecl> refinesCycle = refines.TryFindCycle();
+      List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

       if (refinesCycle != null) {

         string cy = "";

         string sep = "";

@@ -293,7 +293,7 @@ void ObjectInvariant()
         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

           if (currentClass is ClassRefinementDecl) {      

-            ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+            ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

               Contract.Assert( classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

@@ -302,13 +302,13 @@ void ObjectInvariant()
               List<Field> fields = new List<Field>();

               foreach (IToken tok in inv.Toks) {

                 if (!members.ContainsKey(tok.val))

-                  Error(tok, "Refined class does not declare a field: {0}", tok.val);
+                  Error(tok, "Refined class does not declare a field: {0}", tok.val);

                 else {

                   MemberDecl field = members[tok.val];

                   if (!(field is Field)) 

                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

                   else if (fields.Contains(cce.NonNull((Field)field)))

-                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
+                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

                   else

                     fields.Add(cce.NonNull((Field)field));

                 }                  

@@ -324,9 +324,9 @@ void ObjectInvariant()
         }

         

         if (currentClass is ClassRefinementDecl) {          

-          ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+          ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

           if (refined != null) {

-            Contract.Assert( classMembers.ContainsKey(refined));
+            Contract.Assert( classMembers.ContainsKey(refined));

           

             // there is a member with the same name in refined class if and only if the member is a refined method

             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

@@ -379,7 +379,7 @@ void ObjectInvariant()
                   if (mf.Ins.Count != mf.Refined.Ins.Count)

                     Error(mf, "Different number of input variables");

                   if (mf.Outs.Count != mf.Refined.Outs.Count)

-                    Error(mf, "Different number of output variables");
+                    Error(mf, "Different number of output variables");

                   if (mf.IsStatic || mf.Refined.IsStatic) 

                     Error(mf, "Refined methods cannot be static");

                 } else {

@@ -387,7 +387,7 @@ void ObjectInvariant()
                 }            

               }

             } else {

-              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
+              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

             }

           }

         

@@ -1783,7 +1783,7 @@ void ObjectInvariant()
           ResolveExpression(ee, twoState, specContext);

           Contract.Assert( ee.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(elementType, ee.Type)) {

-            Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
+            Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);

           }

         }

         if (expr is SetDisplayExpr) {

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index c7be5420..66541236 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -35,7 +35,7 @@ void ObjectInvariant()
       }

       public void AddSuccessor(Vertex v) {

         Contract.Requires(v != null);

-        Successors.Add(v);
+        Successors.Add(v);

       }

     }

 

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 51318640..29574966 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -227,7 +227,7 @@ void ObjectInvariant()
     public void PushVCExpr(VCExpr vc)

     {

       Contract.Requires(vc != null);

-      //thmProver.Context.AddAxiom(vc);
+      //thmProver.Context.AddAxiom(vc);

       thmProver.PushVCExpression(vc);

     }

 

@@ -326,7 +326,7 @@ void ObjectInvariant()
   public class ErrorModel {

     public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;

     public List<List<string/*!>>!*/>> partitionToIdentifiers;

-    public List<Object>/*!*/ partitionToValue;
+    public List<Object>/*!*/ partitionToValue;

     public Dictionary<object, int>/*!*/ valueToPartition;

     public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;

 

@@ -436,7 +436,7 @@ void ObjectInvariant()
         {

           if (values[i] == tuple[j]) {

             // succeeded in matching tuple[j]

-            j++;
+            j++;

             if (j == tuple.Count-1) return tuple[tuple.Count - 1];

           }

         }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 28744b27..b5f35b1e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie {
         if (b.tok == null) {

           Console.WriteLine("    <intermediate block>");

         } else {

-          // for ErrorTrace == 1 restrict the output;
+          // for ErrorTrace == 1 restrict the output;

           // do not print tokens with -17:-4 as their location because they have been 

           // introduced in the translation and do not give any useful feedback to the user

           if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 81273319..da0bc5b0 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -252,7 +252,7 @@ void ObjectInvariant()
   public abstract class VCExprTranslator : ICloneable {

     public abstract string translate(VCExpr expr, int polarity);

     public abstract string Lookup(VCExprVar var);

-    public abstract Object Clone();
+    public abstract Object Clone();

   }

 

   [ContractClassFor(typeof(VCExprTranslator))]

diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
index d4ee1f35..2407fecf 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/VCGeneration/DoomCheck.cs
@@ -39,12 +39,12 @@ void ObjectInvariant()
 }

 

         private Checker m_Checker;

-        private DoomErrorHandler m_ErrorHandler;
+        private DoomErrorHandler m_ErrorHandler;

         

         [NotDelayed]

         public Evc(Checker check) {

           Contract.Requires(check != null);

-            m_Checker = check;
+            m_Checker = check;

                    

         }

         

@@ -61,11 +61,11 @@ void ObjectInvariant()
             // Todo: Check if vc is trivial true or false            

             outcome = ProverInterface.Outcome.Undetermined;

             Contract.Assert( m_ErrorHandler !=null);

-            m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
+            m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);

             m_Checker.ProverDone.WaitOne();

             

             try {

-              outcome = m_Checker.ReadOutcome();
+              outcome = m_Checker.ReadOutcome();

             } catch (UnexpectedProverOutputException e)

             {

               if (CommandLineOptions.Clo.TraceVerify) { 

@@ -102,17 +102,17 @@ void ObjectInvariant()
             }

         }

         

-        private DoomErrorHandler m_ErrHandler;
-        private Checker m_Check;
-        private InclusionOrder m_Order;
-        private Evc m_Evc;
+        private DoomErrorHandler m_ErrHandler;

+        private Checker m_Check;

+        private InclusionOrder m_Order;

+        private Evc m_Evc;

         #endregion

         

         [NotDelayed]

         public DoomCheck (Implementation passive_impl, Checker check) {

           Contract.Requires(passive_impl != null);

           Contract.Requires(check != null);

-            m_Check = check;
+            m_Check = check;

             if (!VC.DCGen.UseItAsDebugger ) {  

                 m_Order = new InclusionOrder(passive_impl.Blocks[0]);

             } else {

@@ -126,7 +126,7 @@ void ObjectInvariant()
             Contract.Assert( l2a!=null);

             Label2Absy = l2a;

 //            vce = check.VCExprGen.Implies(vce, vce);

-            m_Evc.Initialize(vce);
+            m_Evc.Initialize(vce);

         }

 

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

@@ -148,9 +148,9 @@ void ObjectInvariant()
                 if (!m_Order.SetCurrentResult(reachvar, outcome, m_ErrHandler)) {

                     outcome = ProverInterface.Outcome.Undetermined;

                 }

-                return true;
+                return true;

             } else {

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

                 return false;

             }

         }

@@ -215,8 +215,8 @@ void ObjectInvariant()
                             ConsoleColor col = Console.ForegroundColor;

                             Console.ForegroundColor = ConsoleColor.Green; 					    

 					        Console.WriteLine(vc.ToString());

-                            Console.ForegroundColor = col;
-                            Console.WriteLine(" ... was asked.");
+                            Console.ForegroundColor = col;

+                            Console.WriteLine(" ... was asked.");

                         */

                                                                  

 					    }

@@ -227,7 +227,7 @@ void ObjectInvariant()
 				    default:

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

 			    }

-			    return vc;
+			    return vc;

         }

 

         public VCExpr LetVC(Block startBlock,

@@ -294,7 +294,7 @@ void ObjectInvariant()
 

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

 

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

             

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

             blockVariables.Add(block, v);

@@ -314,7 +314,7 @@ void ObjectInvariant()
             public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();

  

             

-            InclusionTree RootNode = new InclusionTree(null);
+            InclusionTree RootNode = new InclusionTree(null);

             InclusionTree currentNode = null;

             [ContractInvariantMethod]

 void ObjectInvariant() 

@@ -340,7 +340,7 @@ void ObjectInvariant()
                 Dictionary<Block, List<Block>> unavoidablemap = new Dictionary<Block, List<Block>>();

 

                 Block exitblock = BreadthFirst(rootblock, map2);Contract.Assert(exitblock != null);

-                BreadthFirstBwd(exitblock, map);
+                BreadthFirstBwd(exitblock, map);

 

                 foreach (KeyValuePair<Block, TraceNode> kvp in map) {

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

@@ -371,7 +371,7 @@ void ObjectInvariant()
                     Insert2Tree(RootNode,kvp);

                 }

                 InitCurrentNode(RootNode);

-                //printtree(RootNode, "",0);
+                //printtree(RootNode, "",0);

             }

                                   

             void InitCurrentNode(InclusionTree n) {Contract.Requires(n != null);

@@ -424,12 +424,12 @@ void ObjectInvariant()
                     if (currentNode != null) {

                         currentNode.IsDoomed = false;

                         currentNode.HasBeenChecked = true;

-                        MarkUndoomedParents(currentNode);
+                        MarkUndoomedParents(currentNode);

                         if (cb != null) {

                             //Console.WriteLine("CE contains: ");

                             foreach (Block b in cb.TraceNodes)

                             {Contract.Assert(b != null);

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

                                 MarkUndoomedFromCE(b, RootNode);

                             }

                             //Console.WriteLine();

@@ -447,14 +447,14 @@ void ObjectInvariant()
 //                        if (ECContainsAssertFalse(currentNode.EquivBlock)) {  

 //                        

 //                            ConsoleColor col = Console.ForegroundColor;

-//                            Console.ForegroundColor = ConsoleColor.Blue;
+//                            Console.ForegroundColor = ConsoleColor.Blue;

 //                            Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");

-//                            Console.ForegroundColor = col;
+//                            Console.ForegroundColor = col;

 //

-//                            currentNode.HasBeenChecked = true;
-//                            currentNode.IsDoomed = false;
-//                            currentNode = currentNode.Parent;
-//                            return false;
+//                            currentNode.HasBeenChecked = true;

+//                            currentNode.IsDoomed = false;

+//                            currentNode = currentNode.Parent;

+//                            return false;

 //                        }

                         

                         List<Block> traceblocks = new List<Block>();

@@ -464,7 +464,7 @@ void ObjectInvariant()
                         

 //                        cb.OnWarning("Doomed program points found!");

                         if (cb != null) {

-                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
+                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);

                         }

                                                 

                         if (currentNode.EquivBlock.Count>0) {

@@ -596,7 +596,7 @@ void ObjectInvariant()
                                     

             InclusionTree FindNextNode(InclusionTree n) {Contract.Requires(n != null);

                 Contract.Assert( n!=n.Parent);

-                InclusionTree next = n.Parent;
+                InclusionTree next = n.Parent;

                 if (next!=null) {

                   foreach (InclusionTree n0 in next.Children) {

                     Contract.Assert(n0 != null);

@@ -604,7 +604,7 @@ void ObjectInvariant()
                             return n0;

                         }

                     }

-                    return FindNextNode(next);
+                    return FindNextNode(next);

                 }                

                 return next;

             }

@@ -662,7 +662,7 @@ void ObjectInvariant()
             bool IsSubset(List<Block> sub, List<Block> super ) {Contract.Requires(sub!=null);Contract.Requires(cce.NonNullElements(super));

                 foreach (Block b in sub) {

                   Contract.Assert(b != null);

-                    if (!super.Contains(b) ) return false;
+                    if (!super.Contains(b) ) return false;

                 }

                 return true;

             }

@@ -683,7 +683,7 @@ void ObjectInvariant()
             private class InclusionTree {

                 public InclusionTree(InclusionTree p) {

                     Parent = p;

-                    HasBeenChecked=false;
+                    HasBeenChecked=false;

                     IsDoomed = false;

                 }

                 

@@ -731,7 +731,7 @@ void ObjectInvariant()
                         Contract.Assert( firstpred!=null);

                         if (blockmap.TryGetValue(firstpred, out t0)) {

                             Contract.Assert( t0 !=null);

-                            tn.Unavoidables.AddRange(t0.Unavoidables);
+                            tn.Unavoidables.AddRange(t0.Unavoidables);

                         }

                     }   

                                          

@@ -739,8 +739,8 @@ void ObjectInvariant()
                         TraceNode t = null;

                         if (blockmap.TryGetValue(b0, out t)) {

                             Contract.Assert( t!=null);

-                            tn.Predecessors.Add(t);
-                            IntersectUnavoidables(t,tn);
+                            tn.Predecessors.Add(t);

+                            IntersectUnavoidables(t,tn);

                             if (!t.Successors.Contains(tn)) t.Successors.Add(tn);

                             blockmap[b0]=t;

                         }

@@ -807,7 +807,7 @@ void ObjectInvariant()
                         Contract.Assert( firstpred!=null);

                         if (blockmap.TryGetValue(firstpred, out t0)) {

                             Contract.Assert( t0 !=null);

-                            tn.Unavoidables.AddRange(t0.Unavoidables);
+                            tn.Unavoidables.AddRange(t0.Unavoidables);

                         }

                       

                                          

@@ -815,8 +815,8 @@ void ObjectInvariant()
                             TraceNode t = null;

                             if (blockmap.TryGetValue(b0, out t)) {

                                 Contract.Assert( t!=null);

-                                tn.Successors.Add(t);
-                                IntersectUnavoidables(t,tn);
+                                tn.Successors.Add(t);

+                                IntersectUnavoidables(t,tn);

                                 if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);

                                 blockmap[b0]=t;

                             }

@@ -880,7 +880,7 @@ void ObjectInvariant()
 

                 public TraceNode(Block b) {

                   Contract.Requires(b != null);

-                    block=b;
+                    block=b;

                 }

                 

             }

diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
index f31b597e..0bcf15f8 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/VCGeneration/DoomErrorHandler.cs
@@ -59,7 +59,7 @@ void ObjectInvariant()
           Contract.Requires(cce.NonNullElements(traceblocks));

             m_Reachvar = reachvar;

             m_DoomedBlocks = doomedblocks;

-            m_TraceBlocks = traceblocks;
+            m_TraceBlocks = traceblocks;

         }

         

         

@@ -90,7 +90,7 @@ void ObjectInvariant()
             //Console.Write("{0}, ", b.Label);

           } else {

             AssertCmd a = (AssertCmd)node;

-            assertNodes.Add(a);
+            assertNodes.Add(a);

           }

         }

         m_CurrentTrace.AddRange(traceNodes);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index cf386e77..287d3a27 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1706,7 +1706,7 @@ namespace VC {
       CheckIntAttributeOnImpl(impl, "vcs_max_splits", ref max_splits);

       CheckIntAttributeOnImpl(impl, "vcs_max_keep_going_splits", ref max_kg_splits);

       if (tmp_max_vc_cost >= 0) { 

-        max_vc_cost = tmp_max_vc_cost;
+        max_vc_cost = tmp_max_vc_cost;

       }

 

       Outcome outcome = Outcome.Correct;

@@ -1721,7 +1721,7 @@ namespace VC {
       int total = 0;

       int no = max_splits == 1 && !keep_going ? -1 : 0;

       bool first_round = true;

-      bool do_splitting = keep_going || max_splits > 1;
+      bool do_splitting = keep_going || max_splits > 1;

       double remaining_cost = 0.0, proven_cost = 0.0;

 

       if (do_splitting) {

@@ -1952,7 +1952,7 @@ namespace VC {
 		   reporter.underapproximationMode = false;

 	       

 		   //Console.Write("Checking with preds == true: "); Console.Out.Flush();

-		   ret = CheckVC(vc, reporter, checker, impl.Name);
+		   ret = CheckVC(vc, reporter, checker, impl.Name);

 		   //Console.WriteLine(ret.ToString());

 	       

 		   if(ret == Outcome.Correct) {

@@ -2220,7 +2220,7 @@ namespace VC {
         VCExprNAry vnary = node as VCExprNAry;

         if(vnary == null) return true;

         VCExprBoogieFunctionOp bop = vnary.Op as VCExprBoogieFunctionOp;

-        if(bop == null) return true;
+        if(bop == null) return true;

         if(implName2StratifiedInliningInfo.ContainsKey(bop.Func.Name)) {

            fcalls.Add(vnary);

         }

@@ -3236,7 +3236,7 @@ namespace VC {
         {

           Block entryBlock = cce.NonNull( impl.Blocks[0]);

           RemoveEmptyBlocks(entryBlock);

-          impl.PruneUnreachableBlocks();
+          impl.PruneUnreachableBlocks();

         }

         #endregion Get rid of empty blocks

         

@@ -3318,7 +3318,7 @@ namespace VC {
         for (int i = 0; i < cmds.Length; i++)

         {

           Cmd cmd = cce.NonNull( cmds[i]);

-          AssertCmd assertCmd = cmd as AssertCmd;
+          AssertCmd assertCmd = cmd as AssertCmd;

           if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)

           {

             Counterexample newCounterexample;

@@ -3468,7 +3468,7 @@ namespace VC {
         string calleeName = naryExpr.Fun.FunctionName;

         if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

         VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);

-        Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
+        Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

         Contract.Assert(boogieExprTranslator != null);

         List<int> args = new List<int>();

         foreach (Expr expr in naryExpr.Args)

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 55b1131f..d44547a8 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -182,7 +182,7 @@ namespace VC {
         Dictionary<Block, Block> tmpdict = new Dictionary<Block, Block>();

         CopyImplBlocks(impl.Blocks[0], ref blist, impl.Blocks[0], ref tmpdict);

         blist.Reverse();

-        //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);
+        //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);

 

         #endregion ////////////////////////////////////

 

@@ -291,7 +291,7 @@ namespace VC {
       UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;

       Stopwatch watch = new Stopwatch();

 

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

 

       if (CommandLineOptions.Clo.TraceVerify) {

         Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);

@@ -333,10 +333,10 @@ namespace VC {
 

 

       #endregion

-      //EmitImpl(impl,false);
+      //EmitImpl(impl,false);

 

 

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

 

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

       if (UseItAsDebugger) {

@@ -350,9 +350,9 @@ namespace VC {
       }

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

 

-      // EmitImpl(impl,false);
+      // EmitImpl(impl,false);

 

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

 

       bool __debug = false;

 

@@ -419,7 +419,7 @@ namespace VC {
       #region Try to produce a counter example (brute force)

       if (dc.DoomedSequences.Count > 0) {

         ConsoleColor col = Console.ForegroundColor;

-        //        Console.ForegroundColor = ConsoleColor.Red;
+        //        Console.ForegroundColor = ConsoleColor.Red;

         //        Console.WriteLine("  {0} is DOOMED!", impl.Name);

         //        foreach (List<Block!> bl in dc.DoomedSequences) {

         //            Console.Write("Doomed Blocks: ");

@@ -715,12 +715,12 @@ namespace VC {
             //                    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 = ConsoleColor.White;

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

             //                    Console.ForegroundColor = col;

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

             //                    Console.ForegroundColor = ConsoleColor.Yellow;

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

             //                    Console.ForegroundColor = col;

 

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