Add fix for exception that could occur when using includes and top level members

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -173,7 +173,9 @@ void AddFunction_Top(Function f, bool includeAllMethods) {
     }
 
     void AddMethod_Top(MethodOrConstructor m, bool isByMethod, bool includeAllMethods) {
-      if (!includeAllMethods && !InVerificationScope(m) && !referencedMembers.Contains(m)) {
+      if (!includeAllMethods &&
+          m.EnclosingClass.EnclosingModuleDefinition != forModule &&
+          !referencedMembers.Contains(m)) {
         // do nothing
         return;
       }

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -147,7 +147,12 @@ private void EstablishModuleScope(ModuleDefinition systemModule, ModuleDefinitio
 
     private ProofDependencyManager proofDependencies;
 
-    // optimizing translation
+    /**
+     * The behavior around this field assumes that usages are visited before declarations
+     * which is only the case when the usage is in a different module than the declaration.
+     * However, we alleviate this problem by saying that any declaration must be kept
+     * if any code in that module is verified.
+     */
     readonly ISet<MemberDecl> referencedMembers = new HashSet<MemberDecl>();
 
     public void AddReferencedMember(MemberDecl m) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/files/defaultModuleAndIncludes/Inputs/producer.dfy

@@ -0,0 +1,2 @@
+
+method Foo() {}

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/files/defaultModuleAndIncludes/root.dfy

@@ -0,0 +1,10 @@
+// RUN: %verify "%s" &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Inputs/producer.dfy"
+
+class X {
+  method Bar() {
+    Foo();
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/files/defaultModuleAndIncludes/root.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/news/6192.fix

@@ -0,0 +1 @@
+prevent an exception that could occur when using includes and top level members