summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasureArguments.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/TypeErasureArguments.cs')
-rw-r--r--Source/VCExpr/TypeErasureArguments.cs4
1 files changed, 2 insertions, 2 deletions
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);