Check the AllowGlobals flag in one additional location to avoid a contract failure

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 23f6bc6c..c7f452f6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1020,7 +1020,7 @@ namespace Microsoft.Dafny
           }

           if (cl.IsDefaultClass) {

             foreach (MemberDecl m in cl.Members) {

-              Contract.Assert(!m.HasStaticKeyword);  // note, the IsStatic value isn't available yet; when it becomes available, we expect it will have the value 'true'

+              Contract.Assert(!m.HasStaticKeyword || DafnyOptions.O.AllowGlobals);  // note, the IsStatic value isn't available yet; when it becomes available, we expect it will have the value 'true'

               if (m is Function || m is Method) {

                 sig.StaticMembers[m.Name] = m;

               }