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