merge

5 files changed, 85 insertions, 84 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 0d6e2aab..dbe20415 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -257,14 +257,15 @@ namespace Microsoft.Boogie {
         var s = states[i];

         if (0 <= s && s < MvInfo.CapturePoints.Count) {

           VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];

-          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();

+          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary<Variable, Expr>();

           var cs = m.MkState(map.Description);

 

           foreach (Variable v in MvInfo.AllVariables) {

-            var e = (Expr)map.IncarnationMap[v];

+            Expr e = map.IncarnationMap.ContainsKey(v) ? map.IncarnationMap[v] : null;

             if (e == null) continue;

 

-            if (prevInc[v] == e) continue; // skip unchanged variables

+            Expr prevIncV = prevInc.ContainsKey(v) ? prevInc[v] : null;

+            if (prevIncV == e) continue; // skip unchanged variables

 

             Model.Element elt;

 

@@ -578,7 +579,7 @@ namespace VC {
     protected VariableSeq CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

-    protected Hashtable /*Variable -> int*/ variable2SequenceNumber;

+    protected Dictionary<Variable, int> variable2SequenceNumber;

     public Dictionary<Incarnation, Absy>/*!>!*/ incarnationOriginMap = new Dictionary<Incarnation, Absy>();

 

     public Program program;

@@ -756,7 +757,7 @@ namespace VC {
     /// already been constructed for the implementation (and so

     /// is already an element of impl.Blocks)

     /// </param>

-    protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) {

+    protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {

       Contract.Requires(impl != null);

       Contract.Requires(unifiedExitBlock != null);

       Contract.Requires(gotoCmdOrigins != null);

@@ -1085,7 +1086,7 @@ namespace VC {
     }

 

 

-    protected Block GenerateUnifiedExit(Implementation impl, Hashtable gotoCmdOrigins) {

+    protected Block GenerateUnifiedExit(Implementation impl, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {

       Contract.Requires(impl != null);

       Contract.Requires(gotoCmdOrigins != null);

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

@@ -1112,7 +1113,7 @@ namespace VC {
               BlockSeq bs = new BlockSeq();

               bs.Add(unifiedExit);

               GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);

-              gotoCmdOrigins[go] = b.TransferCmd;

+              gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd;

               b.TransferCmd = go;

               unifiedExit.Predecessors.Add(b);

             }

@@ -1162,7 +1163,7 @@ namespace VC {
       int currentIncarnationNumber =

         variable2SequenceNumber.ContainsKey(x)

         ?

-        (int)cce.NonNull(variable2SequenceNumber[x])

+        variable2SequenceNumber[x]

         :

         -1;

       Variable v = new Incarnation(x, currentIncarnationNumber + 1);

@@ -1187,31 +1188,31 @@ namespace VC {
     /// <param name="b"></param>

     /// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>

     /// <returns></returns>

-    protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) {

+    protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {

       Contract.Requires(b != null);

       Contract.Requires(block2Incarnation != null);

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

 

       if (b.Predecessors.Length == 0) {

-        return new Hashtable();

+        return new Dictionary<Variable, Expr>();

       }

 

-      Hashtable /*Variable -> Expr*/ incarnationMap = null;

+      Dictionary<Variable, Expr> incarnationMap = null;

       Set /*Variable*/ fixUps = new Set /*Variable*/ ();

       foreach (Block pred in b.Predecessors) {

         Contract.Assert(pred != null);

-        Contract.Assert(block2Incarnation.Contains(pred));  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet

-        Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)block2Incarnation[pred];

+        Contract.Assert(block2Incarnation.ContainsKey(pred));  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet

+        Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)block2Incarnation[pred];

         Contract.Assert(predMap != null);

         if (incarnationMap == null) {

-          incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();

+          incarnationMap = new Dictionary<Variable, Expr>(predMap);

           continue;

         }

 

         ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();

         foreach (Variable v in incarnationMap.Keys) {

           Contract.Assert(v != null);

-          if (!predMap.Contains(v)) {

+          if (!predMap.ContainsKey(v)) {

             // conflict!!

             conflicts.Add(v);

             fixUps.Add(v);

@@ -1224,7 +1225,7 @@ namespace VC {
         }

         foreach (Variable v in predMap.Keys) {

           Contract.Assert(v != null);

-          if (!incarnationMap.Contains(v)) {

+          if (!incarnationMap.ContainsKey(v)) {

             // v was not in the domain of the predecessors seen so far, so it needs to be fixed up

             fixUps.Add(v);

           } else {

@@ -1251,10 +1252,10 @@ namespace VC {
           Contract.Assert(pred != null);

           #region Create an assume command equating v_prime with its last incarnation in pred

           #region Create an identifier expression for the last incarnation in pred

-          Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);

+          Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)cce.NonNull(block2Incarnation[pred]);

 

           Expr pred_incarnation_exp;

-          Expr o = (Expr)predMap[v];

+          Expr o = predMap.ContainsKey(v) ? predMap[v] : null;

           if (o == null) {

             Variable predIncarnation = v;

             IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation);

@@ -1279,9 +1280,9 @@ namespace VC {
       return incarnationMap;

     }

 

-    Hashtable preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

+    Dictionary<Variable, Expr> preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

 

-    protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

+    protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

       Contract.Requires(b != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(mvInfo != null);

@@ -1304,11 +1305,11 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

       Contract.Requires(mvInfo != null);

 

-      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

+      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

 

       RestoreParamWhereClauses(impl);

 

@@ -1322,7 +1323,7 @@ namespace VC {
       return r;

     }

 

-    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

       Contract.Requires(mvInfo != null);

@@ -1349,13 +1350,13 @@ namespace VC {
 

       // Now we can process the nodes in an order so that we're guaranteed to have

       // processed all of a node's predecessors before we process the node.

-      Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

+      Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();

       Block exitBlock = null;

-      Hashtable exitIncarnationMap = null;

+      Dictionary<Variable, Expr> exitIncarnationMap = null;

       foreach (Block b in sortedNodes) {

         Contract.Assert(b != null);

-        Contract.Assert(!block2Incarnation.Contains(b));

-        Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

+        Contract.Assert(!block2Incarnation.ContainsKey(b));

+        Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

 

         // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.

         b.liveVarsBefore = null;

@@ -1398,11 +1399,11 @@ namespace VC {
     /// </summary>

     protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

     {

-      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

+      Dictionary<Variable, Expr> oldFrameMap = new Dictionary<Variable, Expr>();

       foreach (IdentifierExpr ie in modifies)

       {

         Contract.Assert(ie != null);

-        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

+        if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl)))

           oldFrameMap.Add(ie.Decl, ie);

       }

       return Substituter.SubstitutionFromHashtable(oldFrameMap);

@@ -1412,7 +1413,7 @@ namespace VC {
     /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

     /// Meanwhile, record any information needed to later reconstruct a model view.

     /// </summary>

-    protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

+    protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

       Contract.Requires(c != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(oldFrameSubst != null);

@@ -1432,14 +1433,14 @@ namespace VC {
           if (description != null) {

             Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

             copy = Bpl.Expr.And(mv, copy);

-            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));

+            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap)));

           }

         }

         Contract.Assert(copy != null);

         if (pc is AssertCmd) {

           ((AssertCmd)pc).OrigExpr = pc.Expr;

           Contract.Assert(((AssertCmd)pc).IncarnationMap == null);

-          ((AssertCmd)pc).IncarnationMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(incarnationMap.Clone());

+          ((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

         }

         pc.Expr = copy;

         passiveCmds.Add(pc);

@@ -1518,7 +1519,7 @@ namespace VC {
       #region havoc w |--> assume whereClauses, out := in( w |-> w' )

  else if (c is HavocCmd) {

         if (this.preHavocIncarnationMap == null)      // Save a copy of the incarnation map (at the top of a sequence of havoc statements)

-          this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();

+          this.preHavocIncarnationMap = new Dictionary<Variable, Expr>(incarnationMap);

 

         HavocCmd hc = (HavocCmd)c;

         Contract.Assert(c != null);

@@ -1748,8 +1749,8 @@ namespace VC {
     public class Mapping

     {

       public readonly string Description;

-      public readonly Hashtable /*Variable -> Expr*/ IncarnationMap;

-      public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) {

+      public readonly Dictionary<Variable, Expr> IncarnationMap;

+      public Mapping(string description, Dictionary<Variable, Expr> incarnationMap) {

         Description = description;

         IncarnationMap = incarnationMap;

       }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 3299ef76..78ed8cb5 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -126,7 +126,7 @@ namespace Microsoft.Boogie
             Contract.Requires(impl != null);

 

             CurrentLocalVariables = impl.LocVars;

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

+            variable2SequenceNumber = new Dictionary<Variable, int>();

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

 

             ResetPredecessors(impl.Blocks);

@@ -395,7 +395,7 @@ namespace Microsoft.Boogie
             public Dictionary<Incarnation, Absy> incarnationOriginMap;

             public Hashtable /*Variable->Expr*/ exitIncarnationMap;

             public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;

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

+            public Dictionary<int, Absy> label2absy;

             public VC.ModelViewInfo mvInfo;

 

             public Dictionary<Block, VCExprVar> reachVars;

@@ -514,7 +514,7 @@ namespace Microsoft.Boogie
             //public VCExpr vcexpr;

             //public List<VCExprVar> interfaceExprVars;

             //public List<VCExprVar> privateExprVars;

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

+            //public Dictionary<int, Absy> label2absy;

             //public VC.ModelViewInfo mvInfo;

             //public Dictionary<Block, List<CallSite>> callSites;

             //public Dictionary<Block, List<CallSite>> recordProcCallSites;

@@ -1007,7 +1007,7 @@ namespace Microsoft.Boogie
             ConvertCFG2DAG(impl,edgesCut);

             VC.ModelViewInfo mvInfo;

             PassifyImpl(impl, out mvInfo);

-            Hashtable/*<int, Absy!>*/ label2absy = null;

+            Dictionary<int, Absy> label2absy = null;

             VCExpressionGenerator gen = checker.VCExprGen;

             Contract.Assert(gen != null);

             VCExpr vcexpr;

@@ -1871,7 +1871,7 @@ namespace Microsoft.Boogie
                 Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

                 VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

                 var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)

-                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();

                 var cs = m.MkState(map.Description);

 

                 foreach (Variable v in info.AllVariables)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index f90788d7..da413984 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -185,7 +185,7 @@ namespace VC {
     public VCExpr vcexpr;

     public List<VCExprVar> interfaceExprVars;

     public List<VCExprVar> privateExprVars;

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

+    public Dictionary<int, Absy> label2absy;

     public ModelViewInfo mvInfo;

     public Dictionary<Block, List<CallSite>> callSites;

     public Dictionary<Block, List<CallSite>> recordProcCallSites;

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

       // Get the VC of the current procedure

       VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;

-      Hashtable/*<int, Absy!>*/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;

+      Dictionary<int, Absy> mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;

 

       // Find all procedure calls in vc and put labels on them      

       FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);

@@ -1349,7 +1349,7 @@ namespace VC {
       StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];

       info.GenerateVC();

       VCExpr vc = info.vcexpr;

-      Hashtable mainLabel2absy = info.label2absy;

+      Dictionary<int, Absy> mainLabel2absy = info.label2absy;

       var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);

 

       // Find all procedure calls in vc and put labels on them      

@@ -1851,7 +1851,7 @@ namespace VC {
     //    VCs with different labels each time)

     public class FCallHandler : MutatingVCExprVisitor<bool> {

       Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;

-      public readonly Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy;

+      public readonly Dictionary<int, Absy>/*!*/ mainLabel2absy;

       public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;

       public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;

       public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;

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

       public FCallHandler(VCExpressionGenerator/*!*/ gen,

                             Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

-                            string mainProcName, Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy)

+                            string mainProcName, Dictionary<int, Absy>/*!*/ mainLabel2absy)

         : base(gen) {

         Contract.Requires(gen != null);

         Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));

@@ -2116,7 +2116,7 @@ namespace VC {
         return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);

       }

 

-      public Hashtable/*<int,absy>*/ getLabel2absy() {

+      public Dictionary<int, Absy> getLabel2absy() {

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

 

         Contract.Assert(currProc != null);

@@ -2158,7 +2158,7 @@ namespace VC {
         string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)

         if (lop.label.Substring(1).StartsWith(prefix)) {

           int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));

-          Hashtable label2absy = getLabel2absy();

+          Dictionary<int, Absy> label2absy = getLabel2absy();

           Absy cmd = label2absy[id] as Absy;

           //label2absy.Remove(id);

 

@@ -2472,7 +2472,7 @@ namespace VC {
           Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

           VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

           var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)

-            ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+            ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();

           var cs = m.MkState(map.Description);

 

           foreach (Variable v in info.AllVariables) {

@@ -2718,7 +2718,7 @@ namespace VC {
         Contract.Ensures(Contract.Result<Absy>() != null);

 

         int id = int.Parse(label);

-        Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;

+        Dictionary<int, Absy> l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;

         return cce.NonNull((Absy)l2a[id]);

       }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 80ffa072..09874382 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -290,7 +290,7 @@ namespace VC {
         parent.CurrentLocalVariables = impl.LocVars;

         ModelViewInfo mvInfo;

         parent.PassifyImpl(impl, out mvInfo);

-        Hashtable label2Absy;

+        Dictionary<int, Absy> label2Absy;

         Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

 

@@ -441,7 +441,7 @@ namespace VC {
       }

 

       class ErrorHandler : ProverInterface.ErrorHandler {

-        Hashtable label2Absy;

+        Dictionary<int, Absy> label2Absy;

         VerifierCallback callback;

         [ContractInvariantMethod]

         void ObjectInvariant() {

@@ -450,7 +450,7 @@ namespace VC {
         }

 

 

-        public ErrorHandler(Hashtable label2Absy, VerifierCallback callback) {

+        public ErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback) {

           Contract.Requires(label2Absy != null);

           Contract.Requires(callback != null);

           this.label2Absy = label2Absy;

@@ -531,7 +531,7 @@ namespace VC {
       double total_cost;

       int assertion_count;

       double assertion_cost; // without multiplication by paths

-      Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;

+      Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;

       readonly public VCGen/*!*/ parent;

       Implementation/*!*/ impl;

 

@@ -548,7 +548,7 @@ namespace VC {
       private int splitNo;

       internal ErrorReporter reporter;

 

-      public Split(List<Block/*!*/>/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {

+      public Split(List<Block/*!*/>/*!*/ blocks, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {

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

         Contract.Requires(gotoCmdOrigins != null);

         Contract.Requires(par != null);

@@ -974,14 +974,14 @@ namespace VC {
         copies.Clear();

         CloneBlock(blocks[0]);

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

-        Hashtable newGotoCmdOrigins = new Hashtable();

+        Dictionary<TransferCmd, ReturnCmd> newGotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();

         foreach (Block b in blocks) {

           Contract.Assert(b != null);

           Block tmp;

           if (copies.TryGetValue(b, out tmp)) {

             newBlocks.Add(cce.NonNull(tmp));

-            if (gotoCmdOrigins.ContainsKey(b)) {

-              newGotoCmdOrigins[tmp] = gotoCmdOrigins[b];

+            if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) {

+              newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd];

             }

 

             foreach (Block p in b.Predecessors) {

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

         this.checker = checker;

 

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

+        Dictionary<int, Absy> label2absy = new Dictionary<int, Absy>();

 

         ProverContext ctx = checker.TheoremProver.Context;

         Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;

@@ -1228,14 +1228,14 @@ namespace VC {
           delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)

           {

             VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

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

+            vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();

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

             vcgen.CurrentLocalVariables = codeExpr.LocVars;

             // codeExpr.Blocks.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

 

             ResetPredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

+            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

             int ac;  // computed, but then ignored for this CodeExpr

             VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

@@ -1350,18 +1350,18 @@ namespace VC {
     }

     #endregion

 

-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)

+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)

     {

       Contract.Requires(impl != null);

       Contract.Requires(proverContext != null);

       Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);

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

 

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

+      label2absy = new Dictionary<int, Absy>();

       return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);

     }

 

-    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {

+    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {

       Contract.Requires(impl != null);

       Contract.Requires(proverContext != null);

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

@@ -1653,8 +1653,8 @@ namespace VC {
     }

 

     public class ErrorReporter : ProverInterface.ErrorHandler {

-      Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;

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

+      Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;

+      Dictionary<int, Absy>/*!*/ label2absy;

       List<Block/*!*/>/*!*/ blocks;

       protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;

       protected VerifierCallback/*!*/ callback;

@@ -1686,8 +1686,8 @@ namespace VC {
       protected ProverContext/*!*/ context;

       Program/*!*/ program;

 

-      public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,

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

+      public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,

+          Dictionary<int, Absy>/*!*/ label2absy,

           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

@@ -1751,7 +1751,7 @@ namespace VC {
           foreach (Block b in returnExample.Trace) {

             Contract.Assert(b != null);

             Contract.Assume(b.TransferCmd != null);

-            ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];

+            ReturnCmd cmd = gotoCmdOrigins.ContainsKey(b.TransferCmd) ? gotoCmdOrigins[b.TransferCmd] : null;

             if (cmd != null) {

               returnExample.FailingReturn = cmd;

               break;

@@ -1782,8 +1782,8 @@ namespace VC {
     }

 

     public class ErrorReporterLocal : ErrorReporter {

-      public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,

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

+      public ErrorReporterLocal(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,

+          Dictionary<int, Absy>/*!*/ label2absy,

           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

@@ -1861,7 +1861,7 @@ namespace VC {
       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

 

       CurrentLocalVariables = impl.LocVars;

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

+      variable2SequenceNumber = new Dictionary<Variable, int>();

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

 

       #region Debug Tracing

@@ -2097,13 +2097,13 @@ namespace VC {
       }

     }

 

-    public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

+    public Dictionary<TransferCmd, ReturnCmd> PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

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

 

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();

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

       Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

       

       #region Debug Tracing

@@ -2216,7 +2216,7 @@ namespace VC {
           cmds.AddRange(entryBlock.Cmds);

           entryBlock.Cmds = cmds;

           // Make sure that all added commands are passive commands.

-          Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());

+          Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());

           TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,

                                ComputeOldExpressionSubstitution(impl.Proc.Modifies));

         }

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

     static VCExpr LetVC(Block startBlock,

                         VCExpr controlFlowVariableExpr,

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

+                        Dictionary<int, Absy> label2absy,

                         ProverContext proverCtxt,

                         out int assertionCount) {

       Contract.Requires(startBlock != null);

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

     static VCExpr LetVCIterative(List<Block> blocks,

                                  VCExpr controlFlowVariableExpr,

-                                 Hashtable label2absy,

+                                 Dictionary<int, Absy> label2absy,

                                  ProverContext proverCtxt,

                                  out int assertionCount) {

       Contract.Requires(blocks != null);

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

     static VCExpr LetVC(Block block,

                         VCExpr controlFlowVariableExpr,

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

+                        Dictionary<int, Absy> label2absy,

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

                         List<VCExprLetBinding/*!*/>/*!*/ bindings,

                         ProverContext proverCtxt,

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

     static VCExpr DagVC(Block block,

                          VCExpr controlFlowVariableExpr,

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

+                         Dictionary<int, Absy> label2absy,

                          Hashtable/*<Block, VCExpr!>*/ blockEquations,

                          ProverContext proverCtxt,

                          out int assertionCount)

@@ -2738,7 +2738,7 @@ namespace VC {
     }

 

     static VCExpr FlatBlockVC(Implementation impl,

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

+                              Dictionary<int, Absy> label2absy,

                               bool local, bool reach, bool doomed,

                               ProverContext proverCtxt,

                               out int assertionCount)

@@ -2874,7 +2874,7 @@ namespace VC {
     }

 

     static VCExpr NestedBlockVC(Implementation impl,

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

+                                Dictionary<int, Absy> label2absy,

                                 bool reach,

                                 ProverContext proverCtxt,

                                 out int assertionCount){

@@ -2997,7 +2997,7 @@ namespace VC {
     }

 

     static VCExpr VCViaStructuredProgram

-                  (Implementation impl, Hashtable/*<int, Absy!>*/ label2absy,

+                  (Implementation impl, Dictionary<int, Absy> label2absy,

                    ProverContext proverCtxt,

                    out int assertionCount)

     {

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index d82310ee..eed4e2a5 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -20,19 +20,19 @@ namespace VC {
       Contract.Invariant(Ctxt != null);

     }

 

-    [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;

+    [Rep] public readonly Dictionary<int, Absy> Label2absy;

     [Rep] public readonly ProverContext Ctxt;

     public readonly VCExpr ControlFlowVariableExpr;

     public int AssertionCount;  // counts the number of assertions for which Wlp has been computed

     

-    public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

     }

     

-    public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;