Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dictionaries are non-null, which is enforced by the implementation of Dictionary.

Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.

8 files changed, 49 insertions, 49 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 64239e42..4d8fed6a 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.VCExprAST {
       private readonly List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ Mapping;

       [ContractInvariantMethod]

       void ObjectInvariant() {

-        Contract.Invariant(Mapping != null && Contract.ForAll(Mapping, i => cce.NonNullElements(i)));

+        Contract.Invariant(Mapping != null && Contract.ForAll(Mapping, i => cce.NonNullDictionaryAndValues(i)));

       }

 

 

@@ -147,7 +147,7 @@ namespace Microsoft.Boogie.VCExprAST {
         List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ mapping =

           new List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>();

         foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in vm.Mapping) {

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

+          Contract.Assert(cce.NonNullDictionaryAndValues(d));

           mapping.Add(new Dictionary<VarKind/*!*/, VCExprVar/*!*/>(d));

         }

         this.Mapping = mapping;

diff --git a/Source/VCExpr/Clustering.cs b/Source/VCExpr/Clustering.cs
index 0f08c98e..1efc3606 100644
--- a/Source/VCExpr/Clustering.cs
+++ b/Source/VCExpr/Clustering.cs
@@ -25,8 +25,8 @@ namespace Microsoft.Boogie.Clustering {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Gen != null);

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

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(SubtermClusters));

     }

 

 

@@ -117,7 +117,7 @@ namespace Microsoft.Boogie.Clustering {
     void ObjectInvariant() {

       Contract.Invariant(Op != null);

       Contract.Invariant(Gen != null);

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));

     }

     // variables that are global and treated like constants

     private readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ GlobalVariables;

@@ -125,7 +125,7 @@ namespace Microsoft.Boogie.Clustering {
     private readonly VCExpressionGenerator/*!*/ Gen;

 

     public TermClustersSameHead(VCExprOp op, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator/*!*/ gen) {

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

       Contract.Requires(gen != null);

       Contract.Requires(op != null);

       Op = op;

@@ -207,7 +207,7 @@ namespace Microsoft.Boogie.Clustering {
       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(Gen != null);

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

+        Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));

         Contract.Invariant(Clusters != null);

         Contract.Invariant(RemainingClusters != null);

         Contract.Invariant(Distances != null);

@@ -220,7 +220,7 @@ namespace Microsoft.Boogie.Clustering {
 

         public Distance(Cluster a, Cluster b, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator gen) {

           Contract.Requires(gen != null);

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

+          Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

           AntiUnificationVisitor/*!*/ visitor = new AntiUnificationVisitor(gen);

           Generator = (VCExprNAry)visitor.AntiUnify(a.Generator, b.Generator);

 

@@ -233,7 +233,7 @@ namespace Microsoft.Boogie.Clustering {
       public ClusteringMatrix(List<Cluster> clusters, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator gen) {

         Contract.Requires(gen != null);

         Contract.Requires(clusters != null);

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

+        Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

         List<Cluster> c = new List<Cluster>();

         c.AddRange(clusters);

         Clusters = c;

@@ -346,7 +346,7 @@ namespace Microsoft.Boogie.Clustering {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Gen != null);

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(Representation));

     }

 

 

@@ -397,7 +397,7 @@ namespace Microsoft.Boogie.Clustering {
     }

 

     public bool RepresentationIsRenaming(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

       if (!Contract.ForAll(Representation, pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1))))

         return false;

       // check that all substituted variables are distinct

@@ -407,12 +407,12 @@ namespace Microsoft.Boogie.Clustering {
     }

 

     public void RepresentationSize(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, out int expr0Size, out int expr1Size) {

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

       ReprSizeComputingVisitor/*!*/ size0Visitor = new ReprSizeComputingVisitor();

       ReprSizeComputingVisitor/*!*/ size1Visitor = new ReprSizeComputingVisitor();

 

       foreach (KeyValuePair<ExprPair, VCExprVar/*!*/> pair in Representation) {

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

+        Contract.Assert(pair.Value != null);

         size0Visitor.ComputeSize(pair.Key.Expr0, globalVars);

         size1Visitor.ComputeSize(pair.Key.Expr1, globalVars);

       }

@@ -505,7 +505,7 @@ Contract.Ensures(Contract.Result<VCExprVar>() != null);
 

     public void ComputeSize(VCExpr expr, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {

       Contract.Requires(expr != null);

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));

       Traverse(expr, globalVars);

     }

 

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index 7c06af18..f811461d 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -58,12 +58,12 @@ namespace Microsoft.Boogie.VCExprAST {
     private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;

     [ContractInvariantMethod]

     void GlobalNamesInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalNames));

     }

     private readonly List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ LocalNames;

     [ContractInvariantMethod]

     void LocalNamesInvariantMethod() {

-      Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullElements(i)));

+      Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullDictionaryAndValues(i)));

     }

 

     // dictionary of all names that have already been used

@@ -71,17 +71,17 @@ namespace Microsoft.Boogie.VCExprAST {
     private readonly IDictionary<string/*!*/, bool/*!*/>/*!*/ UsedNames;

     [ContractInvariantMethod]

     void UsedNamesInvariantMethod() {

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

+      Contract.Invariant(UsedNames != null);

     }

     private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;

     [ContractInvariantMethod]

     void CurrentCountersInvariantMethod() {

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

+      Contract.Invariant(CurrentCounters != null);

     }

     private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalPlusLocalNames;

     [ContractInvariantMethod]

     void GlobalPlusLocalNamesInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalPlusLocalNames));

     }

 

     ////////////////////////////////////////////////////////////////////////////

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 5f3dbc36..616575db 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -74,7 +74,7 @@ namespace Microsoft.Boogie.TypeErasure {
       return arguments;

     }

 

-    public static List<T/*!*/>/*!*/ ToList<T>(params T[] args) {

+    public static List<T/*!*/>/*!*/ ToList<T>(params T[] args) where T : class{

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

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

       return new List<T>(args);

@@ -335,7 +335,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<Type/*!*/, VCExpr/*!*/>/*!*/ BasicTypeReprs;

     [ContractInvariantMethod]

     void BasicTypeReprsInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(BasicTypeReprs));

     }

 

     private VCExpr GetBasicTypeRepr(Type type) {

@@ -354,7 +354,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<TypeCtorDecl/*!*/, TypeCtorRepr/*!*/>/*!*/ TypeCtorReprs;

     [ContractInvariantMethod]

     void TypeCtorReprsInvariantMethod() {

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

+      Contract.Invariant(TypeCtorReprs != null);

     }

 

     internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl decl) {

@@ -395,7 +395,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<TypeVariable/*!*/, VCExprVar/*!*/>/*!*/ TypeVariableMapping;

     [ContractInvariantMethod]

     void TypeVariableMappingInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableMapping));

     }

 

     public VCExprVar Typed2Untyped(TypeVariable var) {

@@ -417,7 +417,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ Typed2UntypedVariables;

     [ContractInvariantMethod]

     void Typed2UntypedVariablesInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedVariables));

     }

 

     // This method must only be used for free (unbound) variables

@@ -457,7 +457,7 @@ namespace Microsoft.Boogie.TypeErasure {
 

     public VCExpr Type2Term(Type type, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {

       Contract.Requires(type != null);

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));

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

       //

       if (type.IsBasic || type.IsBv) {

@@ -654,7 +654,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<Type/*!*/, TypeCastSet/*!*/>/*!*/ TypeCasts;

     [ContractInvariantMethod]

     void TypeCastsInvariantMethod() {

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

+      Contract.Invariant(TypeCasts != null);

     }

 

     private TypeCastSet GetTypeCasts(Type type) {

@@ -911,7 +911,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<MapType/*!*/, MapTypeClassRepresentation/*!*/>/*!*/ ClassRepresentations;

     [ContractInvariantMethod]

     void ClassRepresentationsInvariantMethod() {

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

+      Contract.Invariant(ClassRepresentations != null);

     }

 

     protected MapTypeClassRepresentation GetClassRepresentation(MapType abstractedType) {

@@ -1062,15 +1062,15 @@ namespace Microsoft.Boogie.TypeErasure {
     public readonly IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ TypeVariableBindings;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(VCExprVarBindings));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableBindings));

     }

 

 

     public VariableBindings(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ vcExprVarBindings,

                             IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ typeVariableBindings) {

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

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(vcExprVarBindings));

+      Contract.Requires(cce.NonNullDictionaryAndValues(typeVariableBindings));

       this.VCExprVarBindings = vcExprVarBindings;

       this.TypeVariableBindings = typeVariableBindings;

     }

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 6cc021fa..8187fa10 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -96,7 +96,7 @@ namespace Microsoft.Boogie.TypeErasure {
     private readonly IDictionary<Function/*!*/, Function/*!*/>/*!*/ Typed2UntypedFunctions;

     [ContractInvariantMethod]

     void Typed2UntypedFunctionsInvariantMethod() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedFunctions));

     }

 

     public Function Typed2Untyped(Function fun) {

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 25aa8074..b20fa143 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -332,7 +332,7 @@ namespace Microsoft.Boogie.TypeErasure
     private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;

     [ContractInvariantMethod]

     void Typed2UntypedFunctionsInvariantMethod() {

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

+      Contract.Invariant(Typed2UntypedFunctions != null);

     }

 

     // distinguish between implicit and explicit type parameters

@@ -509,7 +509,7 @@ namespace Microsoft.Boogie.TypeErasure
     public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {

       Contract.Requires(var != null);

       Contract.Requires(originalType != null);

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));

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

 

       if (!var.Type.Equals(originalType)) {

@@ -583,7 +583,7 @@ namespace Microsoft.Boogie.TypeErasure
       new Dictionary<MapType/*!*/, List<int>/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvarant() {

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(explicitSelectTypeParamsCache));

     }

 

 

@@ -1039,7 +1039,7 @@ namespace Microsoft.Boogie.TypeErasure
                                      out List<VCTrigger/*!*/>/*!*/ triggers) {

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

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

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(typeVarTranslation));

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

       Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out triggers)));

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

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 49440ff0..552df3ed 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie {
     internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;

     [ContractInvariantMethod]

     void MiscInvariant() {

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

+      Contract.Invariant(SingletonOpDict != null);

     }

 

 

@@ -693,7 +693,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

-    public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) {

+    public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) where T : class {

       Contract.Requires(args != null);

       List<T/*!*/>/*!*/ res = new List<T>(args.Length);

       foreach (T t in args)

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 344d795b..3d407150 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -419,8 +419,8 @@ namespace Microsoft.Boogie.VCExprAST {
       new Dictionary<VCExprVar/*!*/, int>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

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

+      Contract.Invariant(BoundTermVarsDict != null);

+      Contract.Invariant(BoundTypeVarsDict != null);

     }

 

     private readonly IDictionary<TypeVariable/*!*/, int>/*!*/ BoundTypeVarsDict =

@@ -441,7 +441,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     private void AddBoundVar<T>(IDictionary<T, int> dict, T sym) {

       Contract.Requires(sym != null);

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

+      Contract.Requires(dict != null);

       int n;

       if (dict.TryGetValue(sym, out n))

         dict[sym] = n + 1;

@@ -451,7 +451,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     private void RemoveBoundVar<T>(IDictionary<T/*!*/, int/*!*/>/*!*/ dict, T sym) {

       Contract.Requires(sym != null);

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

+      Contract.Requires(dict != null);

       int n;

       bool b = dict.TryGetValue(sym, out n);

       Contract.Assert(b && n > 0);

@@ -969,17 +969,17 @@ namespace Microsoft.Boogie.VCExprAST {
     private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;

     [ContractInvariantMethod]

     void TermSubstsInvariantMethod() {

-      Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));

+      Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullDictionaryAndValues(i)));

     }

     private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;

     [ContractInvariantMethod]

     void TypeSubstsInvariantMethod() {

-      Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));

+      Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullDictionaryAndValues(i)));

     }

 

     public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {

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

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

+      Contract.Requires(cce.NonNullDictionaryAndValues(termSubst));

+      Contract.Requires(cce.NonNullDictionaryAndValues(typeSubst));

       List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ termSubsts =

         new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>();

       termSubsts.Add(termSubst);

@@ -1059,7 +1059,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {

       get {

-        Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));

+        Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

         IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

         foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

           foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {

@@ -1232,7 +1232,7 @@ namespace Microsoft.Boogie.VCExprAST {
           // right types

           boundVars = new List<VCExprVar/*!*/>();

           IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

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

+          Contract.Assert(cce.NonNullDictionaryAndValues(typeSubst));

           foreach (VCExprVar/*!*/ var in node.BoundVars) {

             Contract.Assert(var != null);

             VCExprVar/*!*/ freshVar =

@@ -1302,7 +1302,7 @@ namespace Microsoft.Boogie.VCExprAST {
           // right types

           newBoundVars = new List<VCExprVar/*!*/>();

           IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

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

+          Contract.Assert(cce.NonNullDictionaryAndValues(typeSubst));

           foreach (VCExprVar/*!*/ var in node.BoundVars) {

             Contract.Assert(var != null);

             VCExprVar/*!*/ freshVar =