diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index dee5a1c26f3..4fcc7757294 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -3105,12 +3105,6 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod } } - protected override void OrganizeModules(Program program, out List modules) { - modules = program.CompileModules.ToList(); - modules.Sort((a, b) => - String.Compare(a.FullDafnyName, b.FullDafnyName, StringComparison.Ordinal)); - } - protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) { TrStmt(body, wr); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy deleted file mode 100644 index 543a05b0e48..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy +++ /dev/null @@ -1,20 +0,0 @@ -// NONUNIFORM: Test of the Rust compiler to ensure it emits modules in a deterministic order. -// RUN: %baredafny translate rs "%s" > "%t" -// RUN: %OutputCheck --file-to-check "%S/moduleordering-rust/src/moduleordering.rs" "%s" -// CHECK-L: pub mod A { -// CHECK-L: pub mod B { -// CHECK-L: pub mod C { -// CHECK-L: pub mod D { -// CHECK-L: pub mod E { -// CHECK-L: pub mod F { -// CHECK-L: pub mod G { -// CHECK-L: pub mod H { - -module B { const X := "B" } -module D { import B const X := B.X } -module C { import A const X := A.X } -module E { import C const X := C.X } -module A { import G const X := G.X } -module G { const X := "G" } -module F { const X := "F" } -module H { const X := "H" } \ No newline at end of file