Fixing integration tests

dafny-lang · Nov 8, 2022 · 4ce0a00 · 4ce0a00
1 parent 944c359
commit 4ce0a00
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
@@ -2750,7 +2750,11 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
               if (field.Rhs != null) {
                 var ec = reporter.Count(ErrorLevel.Error);
                 scope.PushMarker();
-                scope.AllowInstance = currentClass is ClassDecl cd && !cd.IsDefaultClass;
+                if ((currentClass is ClassDecl cd && !cd.IsDefaultClass) || currentClass is DatatypeDecl ||
+                    currentClass is OpaqueTypeDecl) {
+                } else {
+                  scope.AllowInstance = false;
+                }
                 ResolveExpression(field.Rhs, resolutionContext);
                 scope.PopMarker();
                 if (reporter.Count(ErrorLevel.Error) == ec) {