Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln

28 files changed, 480 insertions, 750 deletions

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 4054951f..433195a6 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -100,14 +100,6 @@
   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

-    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Framework, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Framework.dll</HintPath>

-    </Reference>

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

     </Reference>

diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index 827bd070..e29a6d4a 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -11,7 +11,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
   using System.Diagnostics;

   using System.Diagnostics.Contracts;

   using Microsoft.Boogie;

-  using Cci = System.Compiler;

+  using System.Linq;

   using AI = Microsoft.AbstractInterpretationFramework;

 

 

@@ -22,7 +22,6 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     private AI.Lattice lattice;

     private Queue<ProcedureWorkItem> procWorkItems;  //PM: changed to generic queue

     private Queue/*<CallSite>*/ callReturnWorkItems;

-    private Cci.IRelation/*<Procedure,Implementation>*/ procedureImplementations;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -71,120 +70,20 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       this.callReturnWorkItems = new Queue();

     }

 

-    private Cci.IGraphNavigator ComputeCallGraph(Program program) {

+    private Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {

       Contract.Requires(program != null);

-      Contract.Ensures(this.procedureImplementations != null);

       // Since implementations call procedures (impl. signatures) 

       // rather than directly calling other implementations, we first

       // need to compute which implementations implement which

       // procedures and remember which implementations call which

       // procedures.

 

-      Cci.IMutableRelation/*<Implementation,Procedure>*/ callsProcedure = new Cci.Relation();

-      Cci.IMutableRelation/*<Procedure,Implementation>*/ implementsProcedure = new Cci.Relation();

-      this.procedureImplementations = implementsProcedure;

+      return program

+            .TopLevelDeclarations

+            .Where(d => d is Implementation).Select(i => (Implementation)i)

+            .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);

 

-      //      ArrayList publics = new ArrayList();

-      //      publicImpls = publics;

-

-      foreach (Declaration member in program.TopLevelDeclarations) {

-        Implementation impl = member as Implementation;

-        if (impl != null) {

-          implementsProcedure.Add(impl.Proc, impl);

-          //         if (impl.IsPublic) { publics.Add(impl); }          // PR: what does "IsPublic" stand for?

-

-          foreach (Block block in impl.Blocks) {

-            foreach (Cmd cmd in block.Cmds) {

-              CallCmd call = cmd as CallCmd;

-              if (call != null) {

-                callsProcedure.Add(impl, call.Proc);

-              }

-            }

-          }

-        }

-      }

-

-      // Now compute a graph from implementations to implementations.

-

-      Cci.GraphBuilder callGraph = new Cci.GraphBuilder();

-

-      IEnumerable callerImpls = callsProcedure.GetKeys();

-      Contract.Assume(callerImpls != null);  // because of non-generic collection

-      foreach (Implementation caller in callerImpls) {

-        IEnumerable callerProcs = callsProcedure.GetValues(caller);

-        Contract.Assume(callerProcs != null);  // because of non-generic collection

-        foreach (Procedure callee in callerProcs) {

-          IEnumerable calleeImpls = implementsProcedure.GetValues(callee);

-          Contract.Assume(calleeImpls != null);  // because of non-generic collection

-          foreach (Implementation calleeImpl in calleeImpls) {

-            callGraph.AddEdge(caller, calleeImpl);

-          }

-        }

-      }

-

-      return callGraph;

-    }

-

-#if OLDCODE

-    public void ComputeImplementationInvariants (Implementation impl)

-    {

-        // process each procedure implementation by recursively processing the first (entry) block...

-        ComputeBlockInvariants(impl.Blocks[0], lattice.Top);

-

-        // compute the procedure invariant by joining all terminal block invariants...

-        AI.Lattice.Element post = lattice.Bottom;

-        foreach (Block block in impl.Blocks) 

-        {

-            if (block.TransferCmd is ReturnCmd) 

-            {

-                AI.Lattice.Element postValue = block.PostInvariantBuckets[invariantIndex];

-                Debug.Assert(postValue != null);

-                post = post.Join(postValue);

-            }

-        }

-        impl.PostInvariant = post;

-

-        // Now update the procedure to reflect the new properties

-        // of this implementation.

-

-        if (impl.Proc.PreInvariant <= impl.PreInvariant)

-        {

-            // Strengthen the precondition

-            impl.Proc.PreInvariant = impl.PreInvariant;

-            foreach (Implementation otherImpl in this.procedureImplementations.GetValues(impl.Proc))

-            {

-                if (otherImpl == impl) { continue; }

-                if (otherImpl.PreInvariant <= impl.Proc.PreInvariant)

-                {

-                    // If another implementation of the same procedure has

-                    // a weaker precondition, re-do it with the stronger

-                    // precondition.

-                    otherImpl.PreInvariant = impl.Proc.PreInvariant;

-                    this.implWorkItems.Enqueue(otherImpl);

-                }

-            }

-        }

     }

-#endif

-

-

-#if NOTYET

-    public void ComputeSccInvariants (IEnumerable/*<Implementation>*/ implementations)

-    {

-      Debug.Assert(this.implWorkItems.Count == 0); // no work left over from last SCC

-

-      foreach (Implementation impl in implementations) 

-      { 

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

-        this.implWorkItems.Enqueue(impl);

-      }

-

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

-      {

-        Implementation impl = (Implementation)this.implWorkItems.Dequeue();

-      }

-    }

-#endif

 

     public AI.Lattice.Element ApplyProcedureSummary(CallCmd call, Implementation caller, AI.Lattice.Element knownAtCallSite, CallSite callSite) {

       Contract.Requires(call.Proc != null);

@@ -254,12 +153,14 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       return this.lattice.Meet(atReturn, knownAtCallSite);

     }

 

+      /*

     private Cci.IGraphNavigator callGraph;

     public Cci.IGraphNavigator CallGraph {

       get {

         return this.callGraph;

       }

     }

+      */

 

     /// <summary>

     /// Compute the invariants for the program using the underlying abstract domain

@@ -267,29 +168,10 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     public void ComputeProgramInvariants(Program program) {

       Contract.Requires(program != null);

 

-#if NOT_YET

-      Cci.IGraphNavigator callGraph = 

-#endif

-

-      callGraph = this.ComputeCallGraph(program);

-      Contract.Assert(this.procedureImplementations != null);

-      Cci.IRelation procedureImplementations = this.procedureImplementations;//Non-nullability was already asserted in

+      Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);

       //the line above, ergo there is no need for

       //an assert after this statement to maintain

       //the non-null type.

-#if NOT_YET

-      IEnumerable/*<IStronglyConnectedComponent>*/ sccs = 

-          StronglyConnectedComponent.ConstructSCCs(publicImpls, callGraph);

-

-      IList/*<IStronglyConnectedComponent>*/ sortedSccs = 

-          GraphUtil.TopologicallySortComponentGraph(sccs);

-

-      // Go bottom-up through the SCCs of the call graph

-      foreach (IStronglyConnectedComponent scc in sortedSccs)

-      {

-        this.ComputeSccInvariants(scc.Nodes);

-      }

-#endif

       AI.Lattice.Element initialElement = this.lattice.Top;

       Contract.Assert(initialElement != null);

       // Gather all the axioms to create the initial lattice element

@@ -316,8 +198,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
           ProcedureWorkItem workItem = this.procWorkItems.Dequeue();

 

           ProcedureSummaryEntry summaryEntry = cce.NonNull(workItem.Proc.Summary[workItem.Index]);

-

-          if (cce.NonNull(procedureImplementations.GetValues(workItem.Proc)).Count == 0) {

+          if (!procedureImplementations.ContainsKey(workItem.Proc)) {

             // This procedure has no given implementations.  We therefore treat the procedure

             // according to its specification only.

 

@@ -347,7 +228,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
             }

 

             // For each implementation in the procedure...

-            foreach (Implementation impl in cce.NonNull(procedureImplementations.GetValues(workItem.Proc))) {

+            foreach (Implementation impl in cce.NonNull(procedureImplementations[workItem.Proc])) {

               // process each procedure implementation by recursively processing the first (entry) block...

               cce.NonNull(impl.Blocks[0]).Lattice = lattice;

               ComputeBlockInvariants(impl, cce.NonNull(impl.Blocks[0]), summaryEntry.OnEntry, summaryEntry);

@@ -1040,16 +921,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       Contract.Requires(lattice != null);

       AbstractionEngine engine = new AbstractionEngine(lattice);

       engine.ComputeProgramInvariants(program);

-      callGraph = engine.CallGraph;

-    }

-    private static Cci.IGraphNavigator callGraph;

-    public static Cci.IGraphNavigator CallGraph {

-      get {

-        return callGraph;

-      }

     }

-

-

   }

 

 } // namespace
\ No newline at end of file
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8f70766f..64b15be7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -9,8 +9,8 @@
 namespace Microsoft.Boogie.AbstractInterpretation {

   using System.Diagnostics;

   using System.Diagnostics.Contracts;

-  using CCI = System.Compiler;

   using System.Collections;

+  using System.Collections.Generic;

   using AI = Microsoft.AbstractInterpretationFramework;

 

   public class CallSite {

@@ -45,7 +45,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     public AI.Lattice/*!*/ Lattice;

     public AI.Lattice.Element/*!*/ OnEntry;

     public AI.Lattice.Element/*!*/ OnExit;

-    public CCI.IMutableSet/*<CallSite>*//*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+    public HashSet<CallSite>/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Lattice != null);

@@ -61,7 +61,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       this.Lattice = lattice;

       this.OnEntry = onEntry;

       this.OnExit = lattice.Bottom;

-      this.ReturnPoints = new CCI.HashSet();

+      this.ReturnPoints = new HashSet<CallSite>();

       // base();

     }

 

@@ -407,7 +407,7 @@ namespace Microsoft.Boogie {
         Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr

 

         VariableSeq/*!*/ targets = new VariableSeq();

-        Set<Variable> footprint = new Set<Variable>();

+        HashSet<Variable> footprint = new HashSet<Variable>();

 

         foreach (Block/*!*/ b in g.BackEdgeNodes(header))

         {

@@ -422,7 +422,7 @@ namespace Microsoft.Boogie {
 

                     VariableCollector c = new VariableCollector();

                     c.Visit(cmd);

-                    footprint.AddRange(c.usedVars);

+                    footprint.UnionWith(c.usedVars);

                 }

             }

         }

@@ -531,7 +531,7 @@ namespace Microsoft.Boogie {
         Contract.Assert(header != null);

         LoopProcedure loopProc = loopHeaderToLoopProc[header];

         Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();

-        Set<string> dummyBlocks = new Set<string>();

+        HashSet<string> dummyBlocks = new HashSet<string>();

 

         CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]);  // fix me

         VariableSeq inputs = loopHeaderToInputs[header];

@@ -696,7 +696,7 @@ namespace Microsoft.Boogie {
     {

         // Do a BFS to find all reachable blocks

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

-        Set<string> visited = new Set<string>();

+        HashSet<string> visited = new HashSet<string>();

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

 

         visited.Add(impl.Blocks[0].Label);

@@ -2806,7 +2806,7 @@ namespace Microsoft.Boogie {
     public void PruneUnreachableBlocks() {

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

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

-      System.Compiler.IMutableSet /*Block!*/ reachable = new System.Compiler.HashSet /*Block!*/ ();  // the set of elements in "reachableBlocks"

+      HashSet<Block> reachable = new HashSet<Block>();  // the set of elements in "reachableBlocks"

 

       visitNext.Add(this.Blocks[0]);

       while (visitNext.Count != 0) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 35929311..afd171b9 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie {
     public readonly IToken/*!*/ EndCurly;

     public StmtList ParentContext;

     public BigBlock ParentBigBlock;

-    public Set<string/*!*/>/*!*/ Labels = new Set<string/*!*/>();

+    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(EndCurly != null);

@@ -233,7 +233,7 @@ namespace Microsoft.Boogie {
     List<Block/*!*/> blocks;

     string/*!*/ prefix = "anon";

     int anon = 0;

-    Set<string/*!*/> allLabels = new Set<string/*!*/>();

+    HashSet<string/*!*/> allLabels = new HashSet<string/*!*/>();

     Errors/*!*/ errorHandler;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -784,7 +784,7 @@ namespace Microsoft.Boogie {
     // VC generation and SCC computation

     public BlockSeq/*!*/ Predecessors;

 

-    public Set<Variable/*!*/> liveVarsBefore;

+    public HashSet<Variable/*!*/> liveVarsBefore;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Label != null);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index b63b82cc..42bd1406 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -10,7 +10,6 @@ using System.Collections.Specialized;
 using System.IO;

 using System.Diagnostics;

 using System.Diagnostics.Contracts;

-using Cci = System.Compiler;

 

 namespace Microsoft.Boogie {

   public class CommandLineOptions {

@@ -1543,6 +1542,7 @@ namespace Microsoft.Boogie {
       return Contract.Exists(procsToCheck, s => 0 <= methodFullname.IndexOf(s));

     }

 

+#if CCI

     public bool UserWantsToTranslateRoutine(Cci.Method method, string methodFullname) {

       Contract.Requires(methodFullname != null);

       Contract.Requires(method != null);

@@ -1674,6 +1674,7 @@ namespace Microsoft.Boogie {
       }

       return null;

     }

+#endif

 

     class CommandLineParseState {

       public string s;

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index ab4857dc..6cea383c 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -103,19 +103,7 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.SpecSharp.Runtime, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Framework, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Framework.dll</HintPath>

-    </Reference>

     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 694ddc00..40be3798 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -41,7 +41,7 @@ namespace Microsoft.Boogie {
 

   public class ModSetCollector : StandardVisitor {

     static Procedure proc;

-    static Dictionary<Procedure/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ modSets;

+    static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(modSets));

@@ -60,9 +60,9 @@ namespace Microsoft.Boogie {
       }

       Console.WriteLine("Number of procedures = {0}", procCount);

 

-      modSets = new Dictionary<Procedure/*!*/, Set<Variable/*!*/>/*!*/>();

+      modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

 

-      Set<Procedure/*!*/> implementedProcs = new Set<Procedure/*!*/>();

+      HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

         Contract.Assert(decl != null);

         if (decl is Implementation) {

@@ -155,7 +155,7 @@ namespace Microsoft.Boogie {
       if (var.Name == "alloc")

         return;

       if (!modSets.ContainsKey(localProc)) {

-        modSets[localProc] = new Set<Variable/*!*/>();

+        modSets[localProc] = new HashSet<Variable/*!*/>();

       }

       if (modSets[localProc].Contains(var))

         return;

@@ -165,8 +165,8 @@ namespace Microsoft.Boogie {
   }

 

   public class VariableCollector : StandardVisitor {

-    public System.Collections.Generic.Set<Variable/*!*/>/*!*/ usedVars;

-    public System.Collections.Generic.Set<Variable/*!*/>/*!*/ oldVarsUsed;

+    public HashSet<Variable/*!*/>/*!*/ usedVars;

+    public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(usedVars));

@@ -176,8 +176,8 @@ namespace Microsoft.Boogie {
     int insideOldExpr;

 

     public VariableCollector() {

-      usedVars = new System.Collections.Generic.Set<Variable/*!*/>();

-      oldVarsUsed = new System.Collections.Generic.Set<Variable/*!*/>();

+      usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();

+      oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();

       insideOldExpr = 0;

     }

 

@@ -210,11 +210,11 @@ namespace Microsoft.Boogie {
       blockCoalescer.Visit(program);

     }

 

-    private static Set<Block/*!*/>/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) {

+    private static HashSet<Block/*!*/>/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) {

       Contract.Requires(impl != null);

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

-      Set<Block/*!*/> visitedBlocks = new Set<Block/*!*/>();

-      Set<Block/*!*/> multiPredBlocks = new Set<Block/*!*/>();

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));

+      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();

+      HashSet<Block/*!*/> multiPredBlocks = new HashSet<Block/*!*/>();

       Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();

       dfsStack.Push(impl.Blocks[0]);

       while (dfsStack.Count > 0) {

@@ -247,10 +247,10 @@ namespace Microsoft.Boogie {
       //Console.WriteLine("Procedure {0}", impl.Name);

       //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);

 

-      Set<Block/*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

+      HashSet<Block/*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

       Contract.Assert(cce.NonNullElements(multiPredBlocks));

-      Set<Block/*!*/> visitedBlocks = new Set<Block/*!*/>();

-      Set<Block/*!*/> removedBlocks = new Set<Block/*!*/>();

+      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();

+      HashSet<Block/*!*/> removedBlocks = new HashSet<Block/*!*/>();

       Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();

       dfsStack.Push(impl.Blocks[0]);

       while (dfsStack.Count > 0) {

@@ -333,14 +333,14 @@ namespace Microsoft.Boogie {
       IEnumerable<Block> sortedNodes = dag.TopologicalSort();

       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

-        Set<Variable/*!*/>/*!*/ liveVarsAfter = new Set<Variable/*!*/>();

+        HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

         if (block.TransferCmd is GotoCmd) {

           GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;

           if (gotoCmd.labelTargets != null) {

             foreach (Block/*!*/ succ in gotoCmd.labelTargets) {

               Contract.Assert(succ != null);

               Contract.Assert(succ.liveVarsBefore != null);

-              liveVarsAfter.AddRange(succ.liveVarsBefore);

+              liveVarsAfter.UnionWith(succ.liveVarsBefore);

             }

           }

         }

@@ -365,7 +365,7 @@ namespace Microsoft.Boogie {
     }

 

     // perform in place update of liveSet

-    public static void Propagate(Cmd cmd, Set<Variable/*!*/>/*!*/ liveSet) {

+    public static void Propagate(Cmd cmd, HashSet<Variable/*!*/>/*!*/ liveSet) {

       Contract.Requires(cmd != null);

       Contract.Requires(cce.NonNullElements(liveSet));

       if (cmd is AssignCmd) {

@@ -373,7 +373,7 @@ namespace Microsoft.Boogie {
         // I must first iterate over all the targets and remove the live ones.

         // After the removals are done, I must add the variables referred on 

         // the right side of the removed targets

-        Set<int> indexSet = new Set<int>();

+        HashSet<int> indexSet = new HashSet<int>();

         int index = 0;

         foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) {

           Contract.Assert(lhs != null);

@@ -394,7 +394,7 @@ namespace Microsoft.Boogie {
           if (indexSet.Contains(index)) {

             VariableCollector/*!*/ collector = new VariableCollector();

             collector.Visit(expr);

-            liveSet.AddRange(collector.usedVars);

+            liveSet.UnionWith(collector.usedVars);

             AssignLhs lhs = assignCmd.Lhss[index];

             if (lhs is MapAssignLhs) {

               // If the target is a map, then all indices are also read

@@ -402,7 +402,7 @@ namespace Microsoft.Boogie {
               foreach (Expr e in malhs.Indexes) {

                 VariableCollector/*!*/ c = new VariableCollector();

                 c.Visit(e);

-                liveSet.AddRange(c.usedVars);

+                liveSet.UnionWith(c.usedVars);

               }

             }

           }

@@ -427,7 +427,7 @@ namespace Microsoft.Boogie {
         } else {

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(predicateCmd.Expr);

-          liveSet.AddRange(collector.usedVars);

+          liveSet.UnionWith(collector.usedVars);

         }

       } else if (cmd is CommentCmd) {

         // comments are just for debugging and don't affect verification

@@ -470,8 +470,8 @@ namespace Microsoft.Boogie {
 

   public class GenKillWeight {

     // lambda S. (S - kill) union gen

-    Set<Variable/*!*/>/*!*/ gen;

-    Set<Variable/*!*/>/*!*/ kill;

+    HashSet<Variable/*!*/>/*!*/ gen;

+    HashSet<Variable/*!*/>/*!*/ kill;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(gen));

@@ -482,17 +482,17 @@ namespace Microsoft.Boogie {
 

     bool isZero;

 

-    public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new Set<Variable/*!*/>(), new Set<Variable/*!*/>());

+    public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet<Variable/*!*/>(), new HashSet<Variable/*!*/>());

     public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight();

 

     // initializes to zero

     public GenKillWeight() {

       this.isZero = true;

-      this.gen = new Set<Variable/*!*/>();

-      this.kill = new Set<Variable/*!*/>();

+      this.gen = new HashSet<Variable/*!*/>();

+      this.kill = new HashSet<Variable/*!*/>();

     }

 

-    public GenKillWeight(Set<Variable/*!*/> gen, Set<Variable/*!*/> kill) {

+    public GenKillWeight(HashSet<Variable/*!*/> gen, HashSet<Variable/*!*/> kill) {

       Contract.Requires(cce.NonNullElements(gen));

       Contract.Requires(cce.NonNullElements(kill));

       Contract.Assert(gen != null);

@@ -519,7 +519,14 @@ namespace Microsoft.Boogie {
       if (w1.isZero || w2.isZero)

         return zero();

 

-      return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));

+      HashSet<Variable> t = new HashSet<Variable>(w2.gen);

+      t.ExceptWith(w1.kill);

+      HashSet<Variable> g = new HashSet<Variable>(w1.gen);

+      g.UnionWith(t);

+      HashSet<Variable> k = new HashSet<Variable>(w1.kill);

+      k.UnionWith(w2.kill);

+      return new GenKillWeight(g, k);

+      //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));

     }

 

     public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) {

@@ -531,16 +538,29 @@ namespace Microsoft.Boogie {
       if (w2.isZero)

         return w1;

 

-      return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));

+      HashSet<Variable> g = new HashSet<Variable>(w1.gen);

+      g.UnionWith(w2.gen);

+      HashSet<Variable> k = new HashSet<Variable>(w1.kill);

+      k.IntersectWith(w2.kill);

+      return new GenKillWeight(g, k);

+      //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));

     }

 

     public static GenKillWeight projectLocals(GenKillWeight w) {

       Contract.Requires(w != null);

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

-      Set<Variable/*!*/> gen = w.gen.FindAll(isGlobal);

-      Contract.Assert(cce.NonNullElements(gen));

-      Set<Variable/*!*/> kill = w.kill.FindAll(isGlobal);

-      Contract.Assert(cce.NonNullElements(kill));

+      HashSet<Variable/*!*/> gen = new HashSet<Variable>();

+      foreach (Variable v in w.gen)

+      {

+          if (isGlobal(v))

+              gen.Add(v);

+      }

+      HashSet<Variable/*!*/> kill = new HashSet<Variable>();

+      foreach (Variable v in w.kill)

+      {

+          if (isGlobal(v))

+              kill.Add(v);

+      }

 

       return new GenKillWeight(gen, kill);

     }

@@ -567,16 +587,18 @@ namespace Microsoft.Boogie {
       return string.Format("({0},{1})", gen.ToString(), kill.ToString());

     }

 

-    public Set<Variable/*!*/>/*!*/ getLiveVars() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+    public HashSet<Variable/*!*/>/*!*/ getLiveVars() {

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       return gen;

     }

 

-    public Set<Variable/*!*/>/*!*/ getLiveVars(Set<Variable/*!*/>/*!*/ lv) {

+    public HashSet<Variable/*!*/>/*!*/ getLiveVars(HashSet<Variable/*!*/>/*!*/ lv) {

       Contract.Requires(cce.NonNullElements(lv));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

-      Set<Variable/*!*/>/*!*/ temp = cce.NonNull(lv.Difference(kill));

-      return cce.NonNull(temp.Union(gen));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

+      HashSet<Variable> temp = new HashSet<Variable>(lv);

+      temp.ExceptWith(kill);

+      temp.UnionWith(gen);

+      return temp;

     }

 

   }

@@ -585,18 +607,18 @@ namespace Microsoft.Boogie {
     public Graph<Block/*!*/>/*!*/ graph;

     // Map from procedure to the list of blocks that call that procedure

     public Dictionary<string/*!*/, List<Block/*!*/>/*!*/>/*!*/ procsCalled;

-    public Set<Block/*!*/>/*!*/ nodes;

-    public Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>/*!*/ succEdges;

-    public Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>/*!*/ predEdges;

+    public HashSet<Block/*!*/>/*!*/ nodes;

+    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ succEdges;

+    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ predEdges;

     private Dictionary<Block/*!*/, int>/*!*/ priority;

 

-    public Set<Block/*!*/>/*!*/ srcNodes;

-    public Set<Block/*!*/>/*!*/ exitNodes;

+    public HashSet<Block/*!*/>/*!*/ srcNodes;

+    public HashSet<Block/*!*/>/*!*/ exitNodes;

 

     public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightBefore;

     public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightAfter;

-    public Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ liveVarsAfter;

-    public Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ liveVarsBefore;

+    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ liveVarsAfter;

+    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ liveVarsBefore;

 

     public GenKillWeight/*!*/ summary;

     public Implementation/*!*/ impl;

@@ -624,19 +646,19 @@ namespace Microsoft.Boogie {
       Contract.Requires(impl != null);

       this.graph = new Graph<Block/*!*/>();

       this.procsCalled = new Dictionary<string/*!*/, List<Block/*!*/>/*!*/>();

-      this.nodes = new Set<Block/*!*/>();

-      this.succEdges = new Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>();

-      this.predEdges = new Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>();

+      this.nodes = new HashSet<Block/*!*/>();

+      this.succEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();

+      this.predEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();

 

       this.priority = new Dictionary<Block/*!*/, int>();

 

-      this.srcNodes = new Set<Block/*!*/>();

-      this.exitNodes = new Set<Block/*!*/>();

+      this.srcNodes = new HashSet<Block/*!*/>();

+      this.exitNodes = new HashSet<Block/*!*/>();

 

       this.weightBefore = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();

       this.weightAfter = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();

-      this.liveVarsAfter = new Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>();

-      this.liveVarsBefore = new Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>();

+      this.liveVarsAfter = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();

+      this.liveVarsBefore = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();

 

       summary = GenKillWeight.zero();

       this.impl = impl;

@@ -725,11 +747,11 @@ namespace Microsoft.Boogie {
     private void registerNode(Block b) {

       Contract.Requires(b != null);

       if (!succEdges.ContainsKey(b)) {

-        succEdges.Add(b, new Set<Block/*!*/>());

+        succEdges.Add(b, new HashSet<Block/*!*/>());

       }

 

       if (!predEdges.ContainsKey(b)) {

-        predEdges.Add(b, new Set<Block/*!*/>());

+        predEdges.Add(b, new HashSet<Block/*!*/>());

       }

 

       nodes.Add(b);

@@ -762,8 +784,8 @@ namespace Microsoft.Boogie {
 

     Implementation/*!*/ mainImpl;

 

-    static Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ varsLiveAtExit = new Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>();

-    static Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ varsLiveAtEntry = new Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>();

+    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtExit = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();

+    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtEntry = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();

     static Dictionary<string/*!*/, GenKillWeight/*!*/>/*!*/ varsLiveSummary = new Dictionary<string/*!*/, GenKillWeight/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -875,15 +897,15 @@ namespace Microsoft.Boogie {
 

     }

 

-    public static Set<Variable/*!*/>/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) {

+    public static HashSet<Variable/*!*/>/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) {

       Contract.Requires(prog != null);

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       if (varsLiveAtExit.ContainsKey(impl.Name)) {

         return varsLiveAtExit[impl.Name];

       }

       // Return default: all globals and out params

-      Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

       foreach (Variable/*!*/ v in prog.GlobalVariables()) {

         Contract.Assert(v != null);

         lv.Add(v);

@@ -895,15 +917,15 @@ namespace Microsoft.Boogie {
       return lv;

     }

 

-    public static Set<Variable/*!*/>/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) {

+    public static HashSet<Variable/*!*/>/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) {

       Contract.Requires(prog != null);

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       if (varsLiveAtEntry.ContainsKey(impl.Name)) {

         return varsLiveAtEntry[impl.Name];

       }

       // Return default: all globals and in params

-      Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

       foreach (Variable/*!*/ v in prog.GlobalVariables()) {

         Contract.Assert(v != null);

         lv.Add(v);

@@ -920,10 +942,10 @@ namespace Microsoft.Boogie {
       return varsLiveSummary.ContainsKey(name);

     }

 

-    public static Set<Variable/*!*/>/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, Set<Variable/*!*/>/*!*/ lvAfter) {

+    public static HashSet<Variable/*!*/>/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet<Variable/*!*/>/*!*/ lvAfter) {

       Contract.Requires(cmd != null);

       Contract.Requires(cce.NonNullElements(lvAfter));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       Procedure/*!*/ proc = cce.NonNull(cmd.Proc);

       if (varsLiveSummary.ContainsKey(proc.Name)) {

         GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd);

@@ -936,8 +958,8 @@ namespace Microsoft.Boogie {
         Contract.Assert(w != null);

         return w.getLiveVars(lvAfter);

       }

-      Set<Variable/*!*/>/*!*/ ret = new Set<Variable/*!*/>();

-      ret.AddRange(lvAfter);

+      HashSet<Variable/*!*/>/*!*/ ret = new HashSet<Variable/*!*/>();

+      ret.UnionWith(lvAfter);

       LiveVariableAnalysis.Propagate(cmd, ret);

       return ret;

     }

@@ -1014,7 +1036,7 @@ namespace Microsoft.Boogie {
 

     class WorkList {

       SortedList<int, int>/*!*/ priorities;

-      Set<string/*!*/>/*!*/ labels;

+      HashSet<string/*!*/>/*!*/ labels;

 

       Dictionary<int, List<WorkItem/*!*/>/*!*/>/*!*/ workList;

       [ContractInvariantMethod]

@@ -1027,7 +1049,7 @@ namespace Microsoft.Boogie {
 

 

       public WorkList() {

-        labels = new Set<string/*!*/>();

+        labels = new HashSet<string/*!*/>();

         priorities = new SortedList<int, int>();

         workList = new Dictionary<int, List<WorkItem/*!*/>/*!*/>();

       }

@@ -1127,8 +1149,8 @@ namespace Microsoft.Boogie {
         Contract.Assert(cfg != null);

         foreach (Block/*!*/ b in cfg.nodes) {

           Contract.Assert(b != null);

-          cfg.liveVarsAfter.Add(b, new Set<Variable/*!*/>());

-          cfg.liveVarsBefore.Add(b, new Set<Variable/*!*/>());

+          cfg.liveVarsAfter.Add(b, new HashSet<Variable/*!*/>());

+          cfg.liveVarsBefore.Add(b, new HashSet<Variable/*!*/>());

         }

       }

 

@@ -1150,16 +1172,16 @@ namespace Microsoft.Boogie {
       // Set live variable info

       foreach (ICFG/*!*/ cfg in procICFG.Values) {

         Contract.Assert(cfg != null);

-        Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+        HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

         foreach (Block/*!*/ eb in cfg.exitNodes) {

           Contract.Assert(eb != null);

-          lv.AddRange(cfg.liveVarsAfter[eb]);

+          lv.UnionWith(cfg.liveVarsAfter[eb]);

         }

         varsLiveAtExit.Add(cfg.impl.Name, lv);

-        lv = new Set<Variable/*!*/>();

+        lv = new HashSet<Variable/*!*/>();

         foreach (Block/*!*/ eb in cfg.srcNodes) {

           Contract.Assert(eb != null);

-          lv.AddRange(cfg.liveVarsBefore[eb]);

+          lv.UnionWith(cfg.liveVarsBefore[eb]);

         }

         varsLiveAtEntry.Add(cfg.impl.Name, lv);

         varsLiveSummary.Add(cfg.impl.Name, cfg.summary);

@@ -1186,11 +1208,11 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       Contract.Assert(cfg != null);

       Block/*!*/ block = wi.block;

       Contract.Assert(block != null);

-      Set<Variable/*!*/>/*!*/ lv = cfg.liveVarsAfter[block];

+      HashSet<Variable/*!*/>/*!*/ lv = cfg.liveVarsAfter[block];

       Contract.Assert(cce.NonNullElements(lv));

       // Propagate backwards in the block

-      Set<Variable/*!*/>/*!*/ prop = new Set<Variable/*!*/>();

-      prop.AddRange(lv);

+      HashSet<Variable/*!*/>/*!*/ prop = new HashSet<Variable/*!*/>();

+      prop.UnionWith(lv);

       for (int i = block.Cmds.Length - 1; i >= 0; i--) {

         Cmd/*!*/ cmd = block.Cmds[i];

         Contract.Assert(cmd != null);

@@ -1202,7 +1224,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
             Contract.Assert(callee != null);

             // Inter propagation

             // Remove local variables; add return variables

-            Set<Variable/*!*/>/*!*/ elv = new Set<Variable/*!*/>();

+            HashSet<Variable/*!*/>/*!*/ elv = new HashSet<Variable/*!*/>();

             foreach (Variable/*!*/ v in prop) {

               Contract.Assert(v != null);

               if (v is GlobalVariable)

@@ -1215,7 +1237,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
 

             foreach (Block/*!*/ eb in callee.exitNodes) {

               Contract.Assert(eb != null);

-              callee.liveVarsAfter[eb].AddRange(elv);

+              callee.liveVarsAfter[eb].UnionWith(elv);

               // TODO: check if modified before inserting

               AddToWorkListReverse(new WorkItem(callee, eb));

             }

@@ -1231,13 +1253,14 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         }

       }

 

-      cfg.liveVarsBefore[block].AddRange(prop);

+      cfg.liveVarsBefore[block].UnionWith(prop);

 

       foreach (Block/*!*/ b in cfg.predEdges[block]) {

         Contract.Assert(b != null);

-        Set<Variable/*!*/>/*!*/ prev = cfg.liveVarsAfter[b];

+        HashSet<Variable/*!*/>/*!*/ prev = cfg.liveVarsAfter[b];

         Contract.Assert(cce.NonNullElements(prev));

-        Set<Variable/*!*/>/*!*/ curr = cce.NonNull(prev.Union(cfg.liveVarsBefore[block]));

+        HashSet<Variable/*!*/>/*!*/ curr = new HashSet<Variable>(prev);

+        curr.UnionWith(cfg.liveVarsBefore[block]);

         Contract.Assert(cce.NonNullElements(curr));

         if (curr.Count != prev.Count) {

           cfg.liveVarsAfter[b] = curr;

@@ -1323,8 +1346,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCache.ContainsKey(cmd))

         return weightCache[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

       GenKillWeight/*!*/ ret;

 

       if (cmd is AssignCmd) {

@@ -1349,7 +1372,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
           Contract.Assert(expr != null);

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(expr);

-          gen.AddRange(collector.usedVars);

+          gen.UnionWith(collector.usedVars);

           AssignLhs lhs = assignCmd.Lhss[index];

           if (lhs is MapAssignLhs) {

             // If the target is a map, then all indices are also read

@@ -1357,7 +1380,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
             foreach (Expr e in malhs.Indexes) {

               VariableCollector/*!*/ c = new VariableCollector();

               c.Visit(e);

-              gen.AddRange(c.usedVars);

+              gen.UnionWith(c.usedVars);

             }

           }

           index++;

@@ -1396,7 +1419,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         } else {

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(predicateCmd.Expr);

-          gen.AddRange(collector.usedVars);

+          gen.UnionWith(collector.usedVars);

         }

         ret = new GenKillWeight(gen, kill);

       } else if (cmd is CommentCmd) {

@@ -1444,8 +1467,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCacheAfterCall.ContainsKey(cmd))

         return weightCacheAfterCall[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

 

       Contract.Assert(cmd is CallCmd);

       CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd);

@@ -1482,15 +1505,15 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCacheBeforeCall.ContainsKey(cmd))

         return weightCacheBeforeCall[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

       CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd);

 

       foreach (Expr/*!*/ expr in ccmd.Ins) {

         Contract.Assert(expr != null);

         VariableCollector/*!*/ collector = new VariableCollector();

         collector.Visit(expr);

-        gen.AddRange(collector.usedVars);

+        gen.UnionWith(collector.usedVars);

       }

 

       Contract.Assert(ccmd.Proc != null);

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index cfadd2b2..6976e281 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -5,7 +5,6 @@
 //-----------------------------------------------------------------------------

 using System.Diagnostics.Contracts;

 using System.Collections.Generic;

-using Cci = System.Compiler;

 using Bpl = Microsoft.Boogie;

 

 namespace Microsoft.Boogie {

@@ -16,7 +15,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(0 <= unrollMaxDepth);

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

       Dictionary<Block, GraphNode/*!*/> gd = new Dictionary<Block, GraphNode/*!*/>();

-      Cci.HashSet/*Block*//*!*/ beingVisited = new Cci.HashSet/*Block*/();

+      HashSet<Block> beingVisited = new HashSet<Block>();

       GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);

 

       // Compute SCCs

@@ -106,7 +105,7 @@ namespace Microsoft.Boogie {
         return cmds;

       }

 

-      public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, Cci.HashSet/*Block*/ beingVisited) {

+      public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, HashSet<Block> beingVisited) {

         Contract.Requires(beingVisited != null);

         Contract.Requires(b != null);

         Contract.Requires(cce.NonNullElements(gd));

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 93018097..d4b353ef 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -7,7 +7,6 @@ namespace Microsoft.Boogie {
   using System.Collections;

   using System.Collections.Generic;

   using System;

-  using Microsoft.SpecSharp.Collections;

   using System.Diagnostics.Contracts;

 

   [ContractClass(typeof(IErrorSinkContracts))]

diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs
index 8fca82f8..e0b909fe 100644
--- a/Source/Core/Xml.cs
+++ b/Source/Core/Xml.cs
@@ -8,7 +8,6 @@ using System.IO;
 using System.Xml;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

-using Cci = System.Compiler;

 namespace Microsoft.Boogie {

 

   public class XmlSink {

@@ -143,6 +142,7 @@ namespace Microsoft.Boogie {
       cce.EndExpose();

     }

 

+#if CCI

     public void WriteError(string message, Cci.Node offendingNode, BlockSeq trace) {

       Contract.Requires(offendingNode != null);

       Contract.Requires(message != null);

@@ -177,6 +177,7 @@ namespace Microsoft.Boogie {
       }

       cce.EndExpose();

     }

+#endif

 

     [Inside]

     private void WriteTokenAttributes(IToken tok) {

@@ -189,6 +190,7 @@ namespace Microsoft.Boogie {
       }

     }

 

+#if CCI

     [Inside]

     private void WriteTokenAttributes(Cci.Node node) {

       Contract.Requires(node != null);

@@ -201,6 +203,7 @@ namespace Microsoft.Boogie {
         wr.WriteAttributeString("column", node.SourceContext.StartColumn.ToString());

       }

     }

+#endif

 

     public void WriteStartInference(string inferenceName) {

       Contract.Requires(inferenceName != null);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index bd87186b..fcf556f0 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -20,7 +20,6 @@ namespace Microsoft.Boogie
   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics;

   using VC;

-  using Cci = System.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

 

 /* 

@@ -69,17 +68,6 @@ namespace Microsoft.Boogie
         Console.WriteLine("--------------------");

       }

 

-      SelectPlatform(CommandLineOptions.Clo);

-

-      // Make sure the Spec# runtime is initialized.

-      // This happens when the static constructor for the Runtime type is executed.

-      // Otherwise, if a reference happens to get chased to it, it is loaded twice

-      // and then the types in it do not get unique representations.

-      if (System.Type.GetType("Mono.Runtime") == null) {  // MONO

-        Cci.AssemblyNode a = Microsoft.SpecSharp.Runtime.RuntimeAssembly;

-        Contract.Assert( a != null);

-      }

-

       foreach (string file in CommandLineOptions.Clo.Files) 

       {Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

@@ -146,78 +134,11 @@ namespace Microsoft.Boogie
       Console.ForegroundColor = col;

     }

 

-    public static void SelectPlatform(CommandLineOptions options)

-    {

-      Contract.Requires(options != null);

-      if (options.TargetPlatformLocation != null) {

-        // Make sure static constructor runs before we start setting locations, etc.

-        System.Compiler.SystemTypes.Clear();

-

-        switch (options.TargetPlatform){

-        case CommandLineOptions.PlatformType.v1: Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.v11: Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.v2: Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation); break;

-        case CommandLineOptions.PlatformType.cli1: Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation); break;

-        }

-        

-        if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0){

-          System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation;

-        }

-        System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll";

-                

-        System.Compiler.SystemTypes.Initialize(true, true);

-      }

-    }

-  

-    static string GetErrorLine(Cci.ErrorNode node)

-    {    Contract.Requires( node.SourceContext.Document == null || node.SourceContext.Document.Name != null);

-    

-    

-    Contract.Requires(node != null);

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

-

-      string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture);

-      string kind;

-      if (message.Contains("(trace position)")) {

-        kind = "Related information";

-      } else {

-        kind = "Error";

-      }

-      if (node.SourceContext.Document != null) {

-        return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(cce.NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message);

-      } else {

-        return string.Format("{0}: {1}", kind, message);

-      }

-    }

-

     enum FileType { Unknown, Cil, Bpl, Dafny };

 

-    class ErrorReporter

-    {

-        public Cci.ErrorNodeList errors = new Cci.ErrorNodeList();

-      [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(errors!=null);

-}

-

-        public int errorsReported;

-        

-        public void ReportErrors()

-        {

-            //sort the portion of the array that will be reported to make output more deterministic

-            errors.Sort(errorsReported,errors.Count-errorsReported);

-            for(;errorsReported < errors.Count; errorsReported++) {

-                Cci.ErrorNode error = errors[errorsReported];

-                if (error != null)

-                    ErrorWriteLine(GetErrorLine(error));

-            } 

-        }

-    }

-

     static void ProcessFiles (List<string/*!*/>/*!*/ fileNames)

     {

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

+      Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {

         Dafny.Program dafnyProgram;

         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";

@@ -242,7 +163,7 @@ void ObjectInvariant()
           }

 

           int errorCount, verified, inconclusives, timeOuts, outOfMemories;

-          PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+          PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

           switch (oc) {

             case PipelineOutcome.VerificationCompleted:

               if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {

@@ -420,7 +341,6 @@ void ObjectInvariant()
     /// their error code.

     /// </summary>

     static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,

-        ErrorReporter errorReporter,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

     Contract.Requires(cce.NonNullElements(bplFileName));

@@ -451,7 +371,7 @@ void ObjectInvariant()
           return oc;

 

         case PipelineOutcome.ResolvedAndTypeChecked:

-          return InferAndVerify(program, errorReporter, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+          return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

           

         default:

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

@@ -511,7 +431,6 @@ void ObjectInvariant()
     ///    parameters contain meaningful values

     /// </summary>

     static PipelineOutcome InferAndVerify (Program program,

-                                           ErrorReporter errorReporter,

                                            out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

       Contract.Ensures( 0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

@@ -569,169 +488,188 @@ void ObjectInvariant()
       foreach ( Declaration decl in program.TopLevelDeclarations )

       {Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

-        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

-          List<Counterexample>/*?*/ errors;

-

-          DateTime start = new DateTime();  // to please compiler's definite assignment rules

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            start = DateTime.Now;

-            if (CommandLineOptions.Clo.Trace) {

-              Console.WriteLine();

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

-            }

-            if (CommandLineOptions.Clo.XmlSink != null) {

-              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

-            }

-          }

+        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)

+        {

+            List<Counterexample>/*?*/ errors;

 

-          ConditionGeneration.Outcome outcome;

-          try

-          {

-            outcome = vcgen.VerifyImplementation(impl, program, out errors);

-          }

-          catch (VCGenException e)

-          {

-            ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          }

-          catch (UnexpectedProverOutputException upo)

-          {

-            AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          }

+            DateTime start = new DateTime();  // to please compiler's definite assignment rules

+            if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+            {

+                start = DateTime.Now;

+                if (CommandLineOptions.Clo.Trace)

+                {

+                    Console.WriteLine();

+                    Console.WriteLine("Verifying {0} ...", impl.Name);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null)

+                {

+                    CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

+                }

+            }

 

-          string timeIndication = "";

-          DateTime end = DateTime.Now;

-          TimeSpan elapsed = end - start;

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            if (CommandLineOptions.Clo.Trace) {

-              timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+            ConditionGeneration.Outcome outcome;

+            try

+            {

+                outcome = vcgen.VerifyImplementation(impl, program, out errors);

+            }

+            catch (VCGenException e)

+            {

+                ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true);

+                errors = null;

+                outcome = VCGen.Outcome.Inconclusive;

+            }

+            catch (UnexpectedProverOutputException upo)

+            {

+                AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+                errors = null;

+                outcome = VCGen.Outcome.Inconclusive;

             }

-          }

-          

 

-          switch (outcome) {

-            default:

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

-            case VCGen.Outcome.Correct:

-              Inform(String.Format("{0}verified", timeIndication));

-              verified++;

-              break;

-            case VCGen.Outcome.TimedOut:

-              timeOuts++;

-              Inform(String.Format("{0}timed out", timeIndication));

-              break;

-            case VCGen.Outcome.OutOfMemory:

-              outOfMemories++;

-              Inform(String.Format("{0}out of memory", timeIndication));

-              break;

-            case VCGen.Outcome.Inconclusive:

-              inconclusives++;

-              Inform(String.Format("{0}inconclusive", timeIndication));

-              break;

-            case VCGen.Outcome.Errors:

-              Contract.Assert( errors != null);  // guaranteed by postcondition of VerifyImplementation

-              if (errorReporter != null)

-              {

-//                assert translatedProgram != null;

-//                ErrorReporting h = new ErrorReporting();

-//                h.errorReportingWithTrace(translatedProgram, errors, impl);

-                

-                errorReporter.ReportErrors();

-              }

-              else

-              {

-                // BP1xxx: Parsing errors

-                // BP2xxx: Name resolution errors

-                // BP3xxx: Typechecking errors

-                // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-                // BP5xxx: Verification errors

-                

-                errors.Sort(new CounterexampleComparer());

-                foreach (Counterexample error in errors)

+            string timeIndication = "";

+            DateTime end = DateTime.Now;

+            TimeSpan elapsed = end - start;

+            if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+            {

+                if (CommandLineOptions.Clo.Trace)

                 {

-                  if (error is CallCounterexample)

-                  {

-                    CallCounterexample err = (CallCounterexample) error;

-                    ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true);

-                    ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false);

-                    if (CommandLineOptions.Clo.XmlSink != null) {

-                      CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

-                    }

-                  }

-                  else if (error is ReturnCounterexample)

-                  {

-                    ReturnCounterexample err = (ReturnCounterexample) error;

-                    ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true);

-                    ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);

-                    if (CommandLineOptions.Clo.XmlSink != null) {

-                      CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

-                    }

-                  }

-                  else // error is AssertCounterexample

-                  {

-                    AssertCounterexample err = (AssertCounterexample) error;

-                    if (err.FailingAssert is LoopInitAssertCmd) {

-                      ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true);

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    }

-                    else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

-                      // this assertion is a loop invariant which is not maintained

-                      ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true);

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    } else {

-                      string msg = err.FailingAssert.ErrorData as string;

-                      if (msg == null) {

-                        msg = "Error BP5001: This assertion might not hold.";

-                      }

-                      ReportBplError(err.FailingAssert, msg, true);

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    }

-                  }

-                  if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) { 

-                    foreach (string info in error.relatedInformation) {Contract.Assert(info != null);

-                      Console.WriteLine("       " + info);

-                    } 

-                  }

-                  if (CommandLineOptions.Clo.ErrorTrace > 0) {

-                    Console.WriteLine("Execution trace:");

-                    foreach (Block b in error.Trace) {

-                      Contract.Assert(b != null);

-                      if (b.tok == null) {

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

-                      } else {

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

-                          Console.WriteLine("    {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

+                    timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+                }

+            }

+

+            switch (outcome)

+            {

+                default:

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

+                case VCGen.Outcome.Correct:

+                    Inform(String.Format("{0}verified", timeIndication));

+                    verified++;

+                    break;

+                case VCGen.Outcome.TimedOut:

+                    timeOuts++;

+                    Inform(String.Format("{0}timed out", timeIndication));

+                    break;

+                case VCGen.Outcome.OutOfMemory:

+                    outOfMemories++;

+                    Inform(String.Format("{0}out of memory", timeIndication));

+                    break;

+                case VCGen.Outcome.Inconclusive:

+                    inconclusives++;

+                    Inform(String.Format("{0}inconclusive", timeIndication));

+                    break;

+                case VCGen.Outcome.Errors:

+                    Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+                    // BP1xxx: Parsing errors

+                    // BP2xxx: Name resolution errors

+                    // BP3xxx: Typechecking errors

+                    // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+                    // BP5xxx: Verification errors

+

+                    errors.Sort(new CounterexampleComparer());

+                    foreach (Counterexample error in errors)

+                    {

+                        if (error is CallCounterexample)

+                        {

+                            CallCounterexample err = (CallCounterexample)error;

+                            ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true);

+                            ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false);

+                            if (CommandLineOptions.Clo.XmlSink != null)

+                            {

+                                CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+                            }

+                        }

+                        else if (error is ReturnCounterexample)

+                        {

+                            ReturnCounterexample err = (ReturnCounterexample)error;

+                            ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true);

+                            ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);

+                            if (CommandLineOptions.Clo.XmlSink != null)

+                            {

+                                CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+                            }

+                        }

+                        else // error is AssertCounterexample

+                        {

+                            AssertCounterexample err = (AssertCounterexample)error;

+                            if (err.FailingAssert is LoopInitAssertCmd)

+                            {

+                                ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true);

+                                if (CommandLineOptions.Clo.XmlSink != null)

+                                {

+                                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

+                                }

+                            }

+                            else if (err.FailingAssert is LoopInvMaintainedAssertCmd)

+                            {

+                                // this assertion is a loop invariant which is not maintained

+                                ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true);

+                                if (CommandLineOptions.Clo.XmlSink != null)

+                                {

+                                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

+                                }

+                            }

+                            else

+                            {

+                                string msg = err.FailingAssert.ErrorData as string;

+                                if (msg == null)

+                                {

+                                    msg = "Error BP5001: This assertion might not hold.";

+                                }

+                                ReportBplError(err.FailingAssert, msg, true);

+                                if (CommandLineOptions.Clo.XmlSink != null)

+                                {

+                                    CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

+                                }

+                            }

+                        }

+                        if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)

+                        {

+                            foreach (string info in error.relatedInformation)

+                            {

+                                Contract.Assert(info != null);

+                                Console.WriteLine("       " + info);

+                            }

+                        }

+                        if (CommandLineOptions.Clo.ErrorTrace > 0)

+                        {

+                            Console.WriteLine("Execution trace:");

+                            foreach (Block b in error.Trace)

+                            {

+                                Contract.Assert(b != null);

+                                if (b.tok == null)

+                                {

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

+                                }

+                                else

+                                {

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

+                                    {

+                                        Console.WriteLine("    {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

+                                    }

+                                }

+                            }

                         }

-                      }

+                        if (CommandLineOptions.Clo.ModelViewFile != null)

+                        {

+                            error.PrintModel();

+                        }

+                        errorCount++;

                     }

-                  }

-                  if (CommandLineOptions.Clo.ModelViewFile != null) {

-                    error.PrintModel();

-                  }

-                  errorCount++;

-                }

-              }

-              Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

-              break;

-          }

-          if (CommandLineOptions.Clo.XmlSink != null) {

-            CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

-          }

-          if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {

-            Console.Out.Flush();

-          }

+

+                    Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

+                    break;

+            }

+

+            if (CommandLineOptions.Clo.XmlSink != null)

+            {

+                CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

+            }

+            if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+            {

+                Console.Out.Flush();

+            }

         }

       }

       vcgen.Close();

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index afd8f9b3..1ec5abb0 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -97,19 +97,7 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\Core\bin\Debug\Core.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.SpecSharp, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

     <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 6bfd5c34..bc256cd5 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -5,8 +5,6 @@
 //-----------------------------------------------------------------------------

 using System;

 using System.Collections.Generic;

-using Microsoft.SpecSharp.Collections;

-using Microsoft.Contracts;

 using System.Text; // for StringBuilder

 using System.Diagnostics.Contracts;

 namespace Graphing {

@@ -279,23 +277,24 @@ namespace Graphing {
       return;

     }

   }

+

   public class Graph<Node> {

-    private Set<Pair<Node/*!*/, Node/*!*/>> es;

-    private Set<Node> ns;

+    private HashSet<Tuple<Node/*!*/, Node/*!*/>> es;

+    private HashSet<Node> ns;

     private Node source;

     private bool reducible;

-    private Set<Node> headers;

-    private Map<Node, Set<Node>> backEdgeNodes;

-    private Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops;

+    private HashSet<Node> headers;

+    private Dictionary<Node, HashSet<Node>> backEdgeNodes;

+    private Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;

 

     private DomRelation<Node> dominatorMap = null;

-    private Dictionary<Node, Set<Node>> predCache = new Dictionary<Node, Set<Node>>();

-    private Dictionary<Node, Set<Node>> succCache = new Dictionary<Node, Set<Node>>();

+    private Dictionary<Node, HashSet<Node>> predCache = new Dictionary<Node, HashSet<Node>>();

+    private Dictionary<Node, HashSet<Node>> succCache = new Dictionary<Node, HashSet<Node>>();

     private bool predComputed;

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(es == null || Contract.ForAll(es, p => p.First != null && p.Second != null));

-      Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Second != null && p.First != null));

+      Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null));

+      Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));

     }

 

 

@@ -318,30 +317,30 @@ namespace Graphing {
       }

     }

 

-    public Graph(Set<Pair<Node/*!*/, Node/*!*/>> edges) {

+    public Graph(HashSet<Tuple<Node/*!*/, Node/*!*/>> edges) {

 

-      Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.First != null && p.Second != null));

+      Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null));

       es = edges;

 

       // original A#

       //ns = Set<Node>{ x : <x,y> in es } + Set<Node>{ y : <x,y> in es };

 

       // closest Spec#

-      //ns = new Set<Node>{ Pair<Node,Node> p in edges; p.First } + new Set<Node>{ Pair<Node,Node> p in edges; p.Second };

+      //ns = new Set<Node>{ Tuple<Node,Node> p in edges; p.Item1 } + new Set<Node>{ Tuple<Node,Node> p in edges; p.Item2 };

 

       // 

-      Set<Node> temp = new Set<Node>();

-      foreach (Pair<Node/*!*/, Node/*!*/> p in edges) {

-        Contract.Assert(p.First != null);

-        temp.Add(p.First);

-        Contract.Assert(p.Second != null);

-        temp.Add(p.Second);

+      HashSet<Node> temp = new HashSet<Node>();

+      foreach (Tuple<Node/*!*/, Node/*!*/> p in edges) {

+        Contract.Assert(p.Item1 != null);

+        temp.Add(p.Item1);

+        Contract.Assert(p.Item2 != null);

+        temp.Add(p.Item2);

       }

       ns = temp;

     }

     public Graph() {

-      es = new Set<Pair<Node/*!*/, Node/*!*/>>();

-      ns = new Set<Node>();

+      es = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();

+      ns = new HashSet<Node>();

     }

 

     // BUGBUG: Set<T>.ToString() should return a non-null string

@@ -363,22 +362,22 @@ namespace Graphing {
       Contract.Requires(dest != null);

       //es += Set<Edge>{<source,dest>};

       //ns += Set<Node>{source, dest};

-      es.Add(new Pair<Node/*!*/, Node/*!*/>(source, dest));

+      es.Add(new Tuple<Node/*!*/, Node/*!*/>(source, dest));

       ns.Add(source);

       ns.Add(dest);

       predComputed = false;

     }

 

-    public Set<Node> Nodes {

+    public HashSet<Node> Nodes {

       get {

         return ns;

       }

     }

-    public IEnumerable<Pair<Node/*!*/, Node/*!*/>> Edges {

+    public IEnumerable<Tuple<Node/*!*/, Node/*!*/>> Edges {

       get {

-        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Pair<Node, Node>>>())

-          && Contract.ForAll(Contract.Result<IEnumerable<Pair<Node, Node>>>(), n =>

-          n.First != null && n.Second != null));

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Tuple<Node, Node>>>())

+          && Contract.ForAll(Contract.Result<IEnumerable<Tuple<Node, Node>>>(), n =>

+          n.Item1 != null && n.Item2 != null));

         return es;

       }

     }

@@ -388,33 +387,33 @@ namespace Graphing {
       Contract.Requires(y != null);

       // original A#

       // return <x,y> in es;

-      return es.Contains(new Pair<Node/*!*/, Node/*!*/>(x, y));

+      return es.Contains(new Tuple<Node/*!*/, Node/*!*/>(x, y));

     }

 

     private void ComputePredSuccCaches() {

       if (predComputed)

         return;

       predComputed = true;

-      predCache = new Dictionary<Node, Set<Node>>();

-      succCache = new Dictionary<Node, Set<Node>>();

+      predCache = new Dictionary<Node, HashSet<Node>>();

+      succCache = new Dictionary<Node, HashSet<Node>>();

 

       foreach (Node n in Nodes) {

-        predCache[n] = new Set<Node>();

-        succCache[n] = new Set<Node>();

+        predCache[n] = new HashSet<Node>();

+        succCache[n] = new HashSet<Node>();

       }

 

-      foreach (Pair<Node/*!*/, Node/*!*/> p in Edges) {

-        Contract.Assert(p.First != null);

-        Contract.Assert(p.Second != null);

-        Set<Node> tmp;

+      foreach (Tuple<Node/*!*/, Node/*!*/> p in Edges) {

+        Contract.Assert(p.Item1 != null);

+        Contract.Assert(p.Item2 != null);

+        HashSet<Node> tmp;

 

-        tmp = predCache[p.Second];

-        tmp.Add(p.First);

-        predCache[p.Second] = tmp;

+        tmp = predCache[p.Item2];

+        tmp.Add(p.Item1);

+        predCache[p.Item2] = tmp;

 

-        tmp = succCache[p.First];

-        tmp.Add(p.Second);

-        succCache[p.First] = tmp;

+        tmp = succCache[p.Item1];

+        tmp.Add(p.Item2);

+        succCache[p.Item1] = tmp;

       }

     }

 

@@ -482,10 +481,10 @@ namespace Graphing {
         nodeToNumber[node] = counter;

         counter++;

       }

-      foreach (Pair<Node/*!*/, Node/*!*/> e in this.Edges) {

-        Contract.Assert(e.First != null);

-        Contract.Assert(e.Second != null);

-        Node/*!*/ target = e.Second;

+      foreach (Tuple<Node/*!*/, Node/*!*/> e in this.Edges) {

+        Contract.Assert(e.Item1 != null);

+        Contract.Assert(e.Item2 != null);

+        Node/*!*/ target = e.Item2;

         incomingEdges[nodeToNumber[target]]++;

       }

       List<Node> sorted = new List<Node>();

@@ -518,14 +517,15 @@ namespace Graphing {
       return;

     }

     private IEnumerable<Node> OldTopologicalSort() {

-      Pair<bool, Seq<Node>> result = this.TopSort();

-      return result.First ? result.Second : (IEnumerable<Node>)new Seq<Node>();

+      Tuple<bool, List<Node>> result = this.TopSort();

+      return result.Item1 ? result.Item2 : (IEnumerable<Node>)new List<Node>();

     }

     // From AsmL distribution example

-    private Pair<bool, Seq<Node>> TopSort() {

-      Seq<Node> S = new Seq<Node>();

-      Set<Node> V = this.Nodes;

-      Set<Node> X = new Set<Node>();

+    private Tuple<bool, List<Node>> TopSort()

+    {

+      List<Node> S = new List<Node>();

+      HashSet<Node> V = this.Nodes;

+      HashSet<Node> X = new HashSet<Node>();

       foreach (Node/*!*/ n in V) {

         Contract.Assert(n != null);

         X.Add(n);

@@ -556,11 +556,11 @@ namespace Graphing {
           }

           // Then we made it all the way through X without finding a source node

           if (!change) {

-            return new Pair<bool, Seq<Node>>(false, new Seq<Node>());

+            return new Tuple<bool, List<Node>>(false, new List<Node>());

           }

         }

       }

-      return new Pair<bool, Seq<Node>>(true, S);

+      return new Tuple<bool, List<Node>>(true, S);

     }

 

     public static bool Acyclic(Graph<Node> g, Node source) {

@@ -570,66 +570,29 @@ namespace Graphing {
       return acyclic;

     }

 

-    //

-    // [Dragon, pp. 670--671]

-    // returns map D s.t. d in D(n) iff d dom n

-    //

-    static private Map<Node, Set<Node>> OldComputeDominators(Graph<Node> g, Node/*!*/ source) {

-      Contract.Requires(source != null);

-      Contract.Assert(g.source != null);

-      Set<Node> N = g.Nodes;

-      Set<Node> nonSourceNodes = N - new Set<Node>(source);

-      Map<Node, Set<Node>> D = new Map<Node, Set<Node>>();

-      D[source] = new Set<Node>(source);

-      foreach (Node/*!*/ n in nonSourceNodes) {

-        Contract.Assert(n != null);

-        D[n] = N;

-      }

-      bool change = true;

-      while (change) {

-        change = false;

-        foreach (Node/*!*/ n in nonSourceNodes) {

-          Contract.Assert(n != null);

-

-          // original A#

-          //Set<Set<Node>> allPreds = new Set<Set<Node>>{ Node p in this.Predecessors(n) ; D[p] };

-

-          Set<Set<Node>> allPreds = new Set<Set<Node>>();

-          foreach (Node/*!*/ p in g.Predecessors(n)) {

-            Contract.Assert(p != null);

-            allPreds.Add(D[p]);

-          }

-          Set<Node> temp = new Set<Node>(n) + Set<Node>.BigIntersect(allPreds);

-          if (temp != D[n]) {

-            change = true;

-            D[n] = temp;

-          }

-        }

-      }

-      return D;

-    }

-

     // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.]

-    static Set<Node> NaturalLoop(Graph<Node> g, Pair<Node/*!*/, Node/*!*/> backEdge) {

-      Contract.Requires(backEdge.First != null && backEdge.Second != null);

-      Node/*!*/ n = backEdge.First;

-      Node/*!*/ d = backEdge.Second;

-      Seq<Node> stack = new Seq<Node>();

-      Set<Node> loop = new Set<Node>(d);

-      if (!n.Equals(d)) // then n is not in loop

+    static HashSet<Node> NaturalLoop(Graph<Node> g, Tuple<Node/*!*/, Node/*!*/> backEdge)

     {

+      Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null);

+      Node/*!*/ n = backEdge.Item1;

+      Node/*!*/ d = backEdge.Item2;

+      Stack<Node> stack = new Stack<Node>();

+      HashSet<Node> loop = new HashSet<Node>();

+      loop.Add(d);

+      if (!n.Equals(d)) // then n is not in loop

+      {

         loop.Add(n);

-        stack = new Seq<Node>(n) + stack; // push n onto stack

+        stack.Push(n); // push n onto stack

       }

       while (stack.Count > 0) // not empty

-    {

-        Node m = stack.Head;

-        stack = stack.Tail; // pop stack

+      {

+        Node m = stack.Peek();

+        stack.Pop(); // pop stack

         foreach (Node/*!*/ p in g.Predecessors(m)) {

           Contract.Assert(p != null);

           if (!(loop.Contains(p))) {

             loop.Add(p);

-            stack = new Seq<Node>(p) + stack; // push p onto stack

+            stack.Push(p); // push p onto stack

           }

         }

       }

@@ -638,16 +601,17 @@ namespace Graphing {
 

     internal struct ReducibleResult {

       internal bool reducible;

-      internal Set<Node> headers;

-      internal Map<Node, Set<Node>> backEdgeNodes;

-      internal Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops;

+      internal HashSet<Node> headers;

+      internal Dictionary<Node, HashSet<Node>> backEdgeNodes;

+      internal Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;

       [ContractInvariantMethod]

       void ObjectInvariant() {

-        Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.First != null && p.Second != null));

+        Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null));

       }

 

-      internal ReducibleResult(bool b, Set<Node> headers, Map<Node, Set<Node>> backEdgeNodes, Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops) {

-        Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.First != null && Key.Second != null));

+      internal ReducibleResult(bool b, HashSet<Node> headers, Dictionary<Node, HashSet<Node>> backEdgeNodes, Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops)

+      {

+        Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null));

         this.reducible = b;

         this.headers = headers;

         this.backEdgeNodes = backEdgeNodes;

@@ -670,15 +634,15 @@ namespace Graphing {
       Contract.Requires(DomRelation != null);

 

       //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible");

-      IEnumerable<Pair<Node/*!*/, Node/*!*/>> edges = g.Edges;

-      Contract.Assert(Contract.ForAll(edges, n => n.First != null && n.Second != null));

-      Set<Pair<Node/*!*/, Node/*!*/>> backEdges = new Set<Pair<Node/*!*/, Node/*!*/>>();

-      Set<Pair<Node/*!*/, Node/*!*/>> nonBackEdges = new Set<Pair<Node/*!*/, Node/*!*/>>();

-      foreach (Pair<Node/*!*/, Node/*!*/> e in edges) {

-        Contract.Assert(e.First != null);

-        Contract.Assert(e.Second != null);

-        Node x = e.First;

-        Node y = e.Second; // so there is an edge from x to y

+      IEnumerable<Tuple<Node/*!*/, Node/*!*/>> edges = g.Edges;

+      Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null));

+      HashSet<Tuple<Node/*!*/, Node/*!*/>> backEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();

+      HashSet<Tuple<Node/*!*/, Node/*!*/>> nonBackEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();

+      foreach (Tuple<Node/*!*/, Node/*!*/> e in edges) {

+        Contract.Assert(e.Item1 != null);

+        Contract.Assert(e.Item2 != null);

+        Node x = e.Item1;

+        Node y = e.Item2; // so there is an edge from x to y

         if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x

           backEdges.Add(e);

         } else {

@@ -687,40 +651,40 @@ namespace Graphing {
       }

       if (!Acyclic(new Graph<Node>(nonBackEdges), source)) {

         return new ReducibleResult(false,

-                                   new Set<Node>(),

-                                   new Map<Node, Set<Node>>(),

-                                   new Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>>());

+                                   new HashSet<Node>(),

+                                   new Dictionary<Node, HashSet<Node>>(),

+                                   new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>());

       } else {

         // original A#:

         //Set<Node> headers = Set{ d : <n,d> in backEdges };

-        Set<Node> headers = new Set<Node>();

-        foreach (Pair<Node/*!*/, Node/*!*/> e in backEdges) {

+        HashSet<Node> headers = new HashSet<Node>();

+        foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {

 

-          Contract.Assert(e.First != null);

-          Contract.Assert(e.Second != null);

-          headers.Add(e.Second);

+          Contract.Assert(e.Item1 != null);

+          Contract.Assert(e.Item2 != null);

+          headers.Add(e.Item2);

         }

         // original A#:

         //Map<Node,Set<Node>> backEdgeNodes = Map{ h -> bs  : h in headers, bs = Set<Node>{ b : <b,x> in backEdges, x == h } };

-        Map<Node, Set<Node>> backEdgeNodes = new Map<Node, Set<Node>>();

+        Dictionary<Node, HashSet<Node>> backEdgeNodes = new Dictionary<Node, HashSet<Node>>();

         foreach (Node/*!*/ h in headers) {

           Contract.Assert(h != null);

-          Set<Node> bs = new Set<Node>();

-          foreach (Pair<Node, Node> backedge in backEdges) {

-            Contract.Assert(backedge.First != null);

-            Contract.Assert(backedge.Second != null);

-            if (backedge.Second.Equals(h)) {

-              bs.Add(backedge.First);

+          HashSet<Node> bs = new HashSet<Node>();

+          foreach (Tuple<Node, Node> backedge in backEdges) {

+            Contract.Assert(backedge.Item1 != null);

+            Contract.Assert(backedge.Item2 != null);

+            if (backedge.Item2.Equals(h)) {

+              bs.Add(backedge.Item1);

             }

           }

           backEdgeNodes.Add(h, bs);

         }

 

         // original A#:

-        //Map<Pair<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };

-        Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops = new Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>>();

-        foreach (Pair<Node/*!*/, Node/*!*/> e in backEdges) {

-          Contract.Assert(e.First != null && e.Second != null);

+        //Map<Tuple<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };

+        Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops = new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>();

+        foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {

+          Contract.Assert(e.Item1 != null && e.Item2 != null);

           naturalLoops.Add(e, NaturalLoop(g, e));

         }

 

@@ -743,13 +707,13 @@ namespace Graphing {
       Contract.Requires(h != null);

       // original A#:

       //return h in backEdgeNodes ? backEdgeNodes[h] : null;

-      return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new Seq<Node>());

+      return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new List<Node>());

     }

     public IEnumerable<Node> NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) {

       Contract.Requires(header != null);

       Contract.Requires(backEdgeNode != null);

-      Pair<Node/*!*/, Node/*!*/> e = new Pair<Node/*!*/, Node/*!*/>(backEdgeNode, header);

-      return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new Seq<Node>();

+      Tuple<Node/*!*/, Node/*!*/> e = new Tuple<Node/*!*/, Node/*!*/>(backEdgeNode, header);

+      return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new List<Node>();

     }

 

     public void ComputeLoops() {

@@ -772,7 +736,7 @@ namespace Graphing {
                 if (b.Equals(c)) continue;

                 if (DominatorMap.DominatedBy(b, c))

                 {

-                    Debug.Assert(!DominatorMap.DominatedBy(c, b));

+                    System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b));

                     dag.AddEdge(b, c);

                 }

             }

@@ -782,12 +746,12 @@ namespace Graphing {
   } // end: class Graph

 

   public class GraphProgram {

-    static void TestGraph<T>(T/*!*/ source, params Pair<T/*!*/, T/*!*/>[] edges) {

+    static void TestGraph<T>(T/*!*/ source, params Tuple<T/*!*/, T/*!*/>[] edges) {

       Contract.Requires(source != null);

-      Contract.Requires(Contract.ForAll(edges, pair => pair.First != null && pair.Second != null));

-      Set<Pair<T/*!*/, T/*!*/>> es = new Set<Pair<T/*!*/, T/*!*/>>();

-      foreach (Pair<T/*!*/, T/*!*/> e in edges) {

-        Contract.Assert(e.First != null && e.Second != null);

+      Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null));

+      HashSet<Tuple<T/*!*/, T/*!*/>> es = new HashSet<Tuple<T/*!*/, T/*!*/>>();

+      foreach (Tuple<T/*!*/, T/*!*/> e in edges) {

+        Contract.Assert(e.Item1 != null && e.Item2 != null);

         es.Add(e);

       }

       Graph<T> g = new Graph<T>(es);

@@ -804,64 +768,64 @@ namespace Graphing {
     {

       Console.WriteLine("Spec# says hello!");

       // This generates bad IL -- need to fix a bug in the compiler

-      //Graph<int> g = new Graph<int>(new Set<Pair<int,int>>{ new Pair<int,int>(1,2), new Pair<int,int>(1,3), new Pair<int,int>(2,3) });

+      //Graph<int> g = new Graph<int>(new Set<Tuple<int,int>>{ new Tuple<int,int>(1,2), new Tuple<int,int>(1,3), new Tuple<int,int>(2,3) });

 

       Console.WriteLine("");

       TestGraph<char>('a',

-        new Pair<char, char>('a', 'b'),

-        new Pair<char, char>('a', 'c'),

-        new Pair<char, char>('b', 'c')

+        new Tuple<char, char>('a', 'b'),

+        new Tuple<char, char>('a', 'c'),

+        new Tuple<char, char>('b', 'c')

       );

 

       Console.WriteLine("");

       TestGraph<char>('a',

-        new Pair<char, char>('a', 'b'),

-        new Pair<char, char>('a', 'c'),

-        new Pair<char, char>('b', 'd'),

-        new Pair<char, char>('c', 'e'),

-        new Pair<char, char>('c', 'f'),

-        new Pair<char, char>('d', 'e'),

-        new Pair<char, char>('e', 'd'),

-        new Pair<char, char>('e', 'f'),

-        new Pair<char, char>('f', 'e')

+        new Tuple<char, char>('a', 'b'),

+        new Tuple<char, char>('a', 'c'),

+        new Tuple<char, char>('b', 'd'),

+        new Tuple<char, char>('c', 'e'),

+        new Tuple<char, char>('c', 'f'),

+        new Tuple<char, char>('d', 'e'),

+        new Tuple<char, char>('e', 'd'),

+        new Tuple<char, char>('e', 'f'),

+        new Tuple<char, char>('f', 'e')

       );

 

       Console.WriteLine("");

       TestGraph<char>('a',

-        new Pair<char, char>('a', 'b'),

-        new Pair<char, char>('a', 'c'),

-        new Pair<char, char>('b', 'c'),

-        new Pair<char, char>('c', 'b')

+        new Tuple<char, char>('a', 'b'),

+        new Tuple<char, char>('a', 'c'),

+        new Tuple<char, char>('b', 'c'),

+        new Tuple<char, char>('c', 'b')

       );

 

       Console.WriteLine("");

       TestGraph<int>(1,

-        new Pair<int, int>(1, 2),

-        new Pair<int, int>(1, 3),

-        new Pair<int, int>(2, 3)

+        new Tuple<int, int>(1, 2),

+        new Tuple<int, int>(1, 3),

+        new Tuple<int, int>(2, 3)

       );

 

       Console.WriteLine("");

       TestGraph<int>(1,

-        new Pair<int, int>(1, 2),

-        new Pair<int, int>(1, 3),

-        new Pair<int, int>(2, 3),

-        new Pair<int, int>(3, 2)

+        new Tuple<int, int>(1, 2),

+        new Tuple<int, int>(1, 3),

+        new Tuple<int, int>(2, 3),

+        new Tuple<int, int>(3, 2)

       );

 

       Console.WriteLine("");

       TestGraph<int>(2,

-        new Pair<int, int>(2, 3),

-        new Pair<int, int>(2, 4),

-        new Pair<int, int>(3, 2)

+        new Tuple<int, int>(2, 3),

+        new Tuple<int, int>(2, 4),

+        new Tuple<int, int>(3, 2)

       );

 

       Console.WriteLine("");

       TestGraph<char>('a',

-        new Pair<char, char>('a', 'b'),

-        new Pair<char, char>('a', 'c'),

-        new Pair<char, char>('b', 'c'),

-        new Pair<char, char>('b', 'b')

+        new Tuple<char, char>('a', 'b'),

+        new Tuple<char, char>('a', 'c'),

+        new Tuple<char, char>('b', 'c'),

+        new Tuple<char, char>('b', 'b')

       );

 

 

diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj
index 868af223..5e7473ea 100644
--- a/Source/Graph/Graph.csproj
+++ b/Source/Graph/Graph.csproj
@@ -99,10 +99,6 @@
     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="Microsoft.SpecSharp.Runtime, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index aac48bda..8a340538 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -100,10 +100,6 @@
   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

     </Reference>

diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj
index 1b73435b..42c441bf 100644
--- a/Source/Provers/Simplify/Simplify.csproj
+++ b/Source/Provers/Simplify/Simplify.csproj
@@ -100,10 +100,6 @@
   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

   </ItemGroup>

diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
index 89faad74..33b8ba7b 100644
--- a/Source/Provers/Z3/Z3.csproj
+++ b/Source/Provers/Z3/Z3.csproj
@@ -100,10 +100,6 @@
   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

     </Reference>

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 7d080eb3..a67530cc 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 750e4a00..fd9944ee 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index cffcd9bf..ba75c772 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 28c71751..b8aa607f 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 0d79bd5a..009a6a59 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 using System.Diagnostics;

-using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index a659c3f2..19b6348a 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -82,10 +82,6 @@
       <HintPath>..\..\..\Binaries\Microsoft.Z3.dll</HintPath>

     </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

     </Reference>

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index c63a158f..6cc021fa 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -227,8 +227,8 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
         storeTypes[i] = abstractedType;

       else

         storeTypes[i] = AxBuilder.U;

-      Microsoft.Contracts.NonNullType.AssertInitialized(selectTypes);

-      Microsoft.Contracts.NonNullType.AssertInitialized(storeTypes);

+      Contract.Assert(cce.NonNullElements<Type>(selectTypes));

+      Contract.Assert(cce.NonNullElements<Type>(storeTypes));

 

       select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);

       store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);

diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index 382a6694..116112a0 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -100,10 +100,6 @@
   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

   </ItemGroup>

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 7002ad61..d465a483 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -362,9 +362,9 @@ namespace VC
                 coverageProcess.StandardInput.WriteLine("batch-graph-command-begin");

                 coverageProcess.StandardInput.WriteLine("reset-color");

                 // Go through the curr candidates and draw edges

-                var nodes = new Microsoft.SpecSharp.Collections.Set<int>();

-                var greenNodes = new Microsoft.SpecSharp.Collections.Set<int>();

-                var redNodes = new Microsoft.SpecSharp.Collections.Set<int>();

+                var nodes = new HashSet<int>();

+                var greenNodes = new HashSet<int>();

+                var redNodes = new HashSet<int>();

                 var edges = new List<KeyValuePair<int, int>>();

                 foreach (var id in calls.currCandidates)

                 {

@@ -1365,7 +1365,7 @@ namespace VC
             // User info -- to decrease/increase calculcation of recursion bound

             public Dictionary<int, int> recursionIncrement;

 

-            public Microsoft.SpecSharp.Collections.Set<int> currCandidates;

+            public HashSet<int> currCandidates;

             [ContractInvariantMethod]

             void ObjectInvariant()

             {

@@ -1398,7 +1398,7 @@ namespace VC
                 id2ControlVar = new Dictionary<int, VCExprVar>();

                 boogieExpr2Id = new Dictionary<BoogieCallExpr, int>();

                 label2Id = new Dictionary<string, int>();

-                currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();

+                currCandidates = new HashSet<int>();

                 currInlineCount = 0;

                 currProc = null;

                 labelRenamer = new Dictionary<string, int>();

@@ -1410,7 +1410,7 @@ namespace VC
 

             public void Clear()

             {

-                currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();

+                currCandidates = new HashSet<int>();

             }

 

             // Given a candidate "id", let proc(id) be the

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index b2d514f6..9906070a 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -99,15 +99,7 @@
     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="Microsoft.SpecSharp.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

   </ItemGroup>

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 4d0b3bad..f989c7bd 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -211,7 +211,7 @@ F -> *10
 m@0 -> -2

 r@0 -> -2

 x@@4 -> 797

-m@1 -> -1

+m@2 -> -1

 m@3 -> -1

 y@@1 -> **y@@1

 r -> **r

@@ -250,8 +250,8 @@ MapType0TypeInv0 -> {
 }

 @MV_state -> {

   0 -> true

-  1 -> true

-  2 -> true

+  3 -> true

+  4 -> true

   5 -> true

 }

 [3] -> {