Fixed a null reference problem in class 'Constant'.

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9cc4ae1d..07448087 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1995,16 +1995,16 @@ namespace Microsoft.Boogie {
     }

     public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent,

                     bool unique,

-                    List<ConstantParent/*!*/> parents, bool childrenComplete,

+                    IEnumerable<ConstantParent/*!*/> parents, bool childrenComplete,

                     QKeyValue kv)

       : base(tok, typedIdent, kv) {

       Contract.Requires(tok != null);

       Contract.Requires(typedIdent != null);

-      Contract.Requires(parents == null || cce.NonNullElements(parents));

+      Contract.Requires(cce.NonNullElements(parents, true));

       Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);

       Contract.Requires(typedIdent.WhereExpr == null);

       this.Unique = unique;

-      this.Parents = new List<ConstantParent>(parents).AsReadOnly();

+      this.Parents = parents == null ? null : new ReadOnlyCollection<ConstantParent>(parents.ToList());

       this.ChildrenComplete = childrenComplete;

     }

     public override bool IsMutable {