diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml
index 3109c167ccb..79d72f30dcf 100644
--- a/.github/workflows/integration-tests-reusable.yml
+++ b/.github/workflows/integration-tests-reusable.yml
@@ -72,6 +72,11 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
+    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
     - name: C++ for ubuntu 20.04
       if: matrix.os == 'ubuntu-20.04'
       run: |
diff --git a/Scripts/package.py b/Scripts/package.py
index f543d37715c..aaffbfe4e20 100755
--- a/Scripts/package.py
+++ b/Scripts/package.py
@@ -161,7 +161,6 @@ def build(self):
         if path.exists(self.buildDirectory):
             shutil.rmtree(self.buildDirectory)
         run(["make", "--quiet", "clean"])
-        self.run_publish("DafnyLanguageServer")
         self.run_publish("DafnyServer")
         self.run_publish("DafnyRuntime", "netstandard2.0")
         self.run_publish("DafnyRuntime", "net452")
diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
index 9bbc493116e..dbfb67041ad 100644
--- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -265,15 +265,27 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<{CharTypeName}>> {argsParameterName})");
     }
 
+    /// <summary>
+    /// Compute the name of the class to use to translate a data-type or a class
+    /// </summary>
+    private string protectedTypeName(TopLevelDecl dt) {
+      var protectedName = IdName(dt);
+      if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
+        return $"_{protectedName}";
+      }
+      return protectedName;
+    }
+
     string IdProtectModule(string moduleName) {
+      Contract.Requires(moduleName != null);
       return string.Join(".", moduleName.Split(".").Select(IdProtect));
     }
 
     protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
       ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
-      moduleName = IdProtectModule(moduleName);
-      return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
+      var protectedModuleName = IdProtectModule(moduleName);
+      return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace {protectedModuleName}");
     }
 
     protected override string GetHelperModuleName() => DafnyHelpersClass;
@@ -305,8 +317,9 @@ string PrintVariance(TypeParameter.TPVariance variance) {
       return $"<{targs.Comma(PrintTypeParameter)}>";
     }
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string /*?*/ fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
+      var name = protectedTypeName(cls);
       var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr);
 
       ConcreteSyntaxTree/*?*/ wCtorBody = null;
@@ -442,7 +455,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
       //     }
       //   }
 
-      var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr);
       var w = cw.InstanceMemberWriter;
       // here come the fields
 
@@ -559,7 +572,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       // }
       var nonGhostTypeArgs = SelectNonGhost(dt, dt.TypeArgs);
       var DtT_TypeArgs = TypeParameters(nonGhostTypeArgs);
-      var DtT_protected = IdName(dt) + DtT_TypeArgs;
+      var DtT_protected = protectedTypeName(dt) + DtT_TypeArgs;
       var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(dt.Origin, dt));
       var simplifiedTypeName = TypeName(simplifiedType, wr, dt.Origin);
 
@@ -581,7 +594,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       } else {
         EmitTypeDescriptorsForClass(dt.TypeArgs, dt, out var wTypeFields, out var wCtorParams, out _, out var wCtorBody);
         wr.Append(wTypeFields);
-        wr.Format($"public {IdName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
+        wr.Format($"public {protectedTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
       }
 
       var wDefault = new ConcreteSyntaxTree();
@@ -995,7 +1008,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
         //   public override _IDt<T> _Get() { if (c != null) { d = c(); c = null; } return d; }
         //   public override string ToString() { return _Get().ToString(); }
         // }
-        var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {IdName(dt)}{typeParams}");
+        var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {protectedTypeName(dt)}{typeParams}");
         w.WriteLine($"public {NeedsNew(dt, "Computer")}delegate {DtTypeName(dt)} Computer();");
         w.WriteLine($"{NeedsNew(dt, "c")}Computer c;");
         w.WriteLine($"{NeedsNew(dt, "d")}{DtTypeName(dt)} d;");
@@ -1017,7 +1030,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
       int constructorIndex = 0; // used to give each constructor a different name
       foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
         var wr = wrx.NewNamedBlock(
-          $"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {IdName(dt)}{typeParams}");
+          $"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {protectedTypeName(dt)}{typeParams}");
         DatatypeFieldsAndConstructor(ctor, constructorIndex, wr);
         constructorIndex++;
       }
@@ -1191,7 +1204,7 @@ string DtCtorDeclarationName(DatatypeCtor ctor) {
       Contract.Ensures(Contract.Result<string>() != null);
 
       var dt = ctor.EnclosingDatatype;
-      return dt.IsRecordType ? IdName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
+      return dt.IsRecordType ? protectedTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
     }
 
     /// <summary>
@@ -1217,7 +1230,7 @@ string DtCtorName(DatatypeCtor ctor) {
       Contract.Ensures(Contract.Result<string>() != null);
 
       var dt = ctor.EnclosingDatatype;
-      var dtName = IdName(dt);
+      var dtName = protectedTypeName(dt);
       if (!dt.EnclosingModuleDefinition.TryToAvoidName) {
         dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName;
       }
@@ -1235,7 +1248,7 @@ string DtCreateName(DatatypeCtor ctor) {
     }
 
     protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr);
       var w = cw.StaticMemberWriter;
       if (nt.NativeType != null) {
         var wEnum = w.NewBlock($"public static System.Collections.Generic.IEnumerable<{GetNativeTypeName(nt.NativeType)}> IntegerRange(BigInteger lo, BigInteger hi)");
@@ -1304,7 +1317,7 @@ void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
     }
 
     protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr);
       if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
         var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel);
         var wStmts = cw.InstanceMemberWriter.Fork();
@@ -2507,6 +2520,10 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
         return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
       }
 
+      if (cl is DatatypeDecl) {
+        return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as DatatypeDecl);
+      }
+
       if (cl.EnclosingModuleDefinition.TryToAvoidName) {
         return IdProtect(cl.GetCompileName(Options));
       }
@@ -2514,6 +2531,11 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
       if (cl.IsExtern(Options, out _, out _)) {
         return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + cl.GetCompileName(Options);
       }
+
+      if (cl is ClassDecl) {
+        return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as ClassDecl);
+      }
+
       return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
     }
 
@@ -2528,7 +2550,7 @@ protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMemb
 
     protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescriptorArguments, string arguments, ConcreteSyntaxTree wr) {
       var dt = dtv.Ctor.EnclosingDatatype;
-      var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
+      var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + protectedTypeName(dt);
 
       var nonGhostInferredTypeArgs = SelectNonGhost(dt, dtv.InferredTypeArgs);
       var typeParams = nonGhostInferredTypeArgs.Count == 0 ? "" : $"<{TypeNames(nonGhostInferredTypeArgs, wr, dtv.Origin)}>";
diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
index 04f08c8794f..dc8d8715169 100644
--- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
@@ -149,7 +149,7 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) {
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
       var w = wr.NewBlock("int main(int argc, char *argv[])");
       var tryWr = w.NewBlock("try");
-      tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), mainMethod.EnclosingClass.GetCompileName(Options), mainMethod.Name));
+      tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), clName(mainMethod.EnclosingClass), mainMethod.Name));
       var catchWr = w.NewBlock("catch (DafnyHaltException & e)");
       catchWr.WriteLine("std::cout << \"Program halted: \" << e.what() << std::endl;");
     }
@@ -226,9 +226,18 @@ private string InstantiateTemplate(List<Type> typeArgs) {
 
     protected override string GetHelperModuleName() => "_dafny";
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
+    private string clName(TopLevelDecl cl) {
+      var className = IdName(cl);
+      if (cl is ClassDecl || cl is DefaultClassDecl) {
+        return className;
+      }
+      return "class_" + className;
+    }
+
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
+      var className = clName(cls);
       if (isExtern) {
-        throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", name));
+        throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className));
       }
       if (superClasses != null && superClasses.Any(trait => !trait.IsObject)) {
         throw new UnsupportedFeatureException(tok, Feature.Traits);
@@ -242,17 +251,17 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
         classDefWriter.WriteLine(DeclareTemplate(typeParameters));
       }
 
-      var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", name), ";");
+      var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", className), ";");
       var methodDefWriter = wr;
 
-      classDeclWriter.WriteLine("class {0};", name);
+      classDeclWriter.WriteLine("class {0};", className);
 
       methodDeclWriter.Write("public:\n");
       methodDeclWriter.WriteLine("// Default constructor");
-      methodDeclWriter.WriteLine("{0}() {{}}", name);
+      methodDeclWriter.WriteLine("{0}() {{}}", className);
 
       // Create the code for the specialization of get_default
-      var fullName = moduleName + "::" + name;
+      var fullName = moduleName + "::" + className;
       var getDefaultStr = String.Format("template <{0}>\nstruct get_default<std::shared_ptr<{1}{2} > > {{\n",
         TypeParameters(typeParameters),
         fullName,
@@ -266,7 +275,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
 
       var fieldWriter = methodDeclWriter;
 
-      return new ClassWriter(name, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
+      return new ClassWriter(className, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
     }
 
     protected override bool SupportsProperties { get => false; }
@@ -615,8 +624,8 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre
       } else {
         throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes);
       }
-      var className = "class_" + IdName(nt);
-      var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), className, nt, wr) as ClassWriter;
+      var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, wr) as ClassWriter;
+      var className = clName(nt);
       var w = cw.MethodDeclWriter;
       if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
         var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel);
@@ -653,8 +662,8 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree
 
       this.modDeclWr.WriteLine("{0} using {1} = {2};", templateDecl, IdName(sst), TypeName(sst.Var.Type, wr, sst.Origin));
 
-      var className = "class_" + IdName(sst);
-      var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), className, sst, wr) as ClassWriter;
+      var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, wr) as ClassWriter;
+      var className = clName(sst);
       var w = cw.MethodDeclWriter;
 
       if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
@@ -785,7 +794,7 @@ public void Finish() { }
 
       wr.Write("{0} {1}{2}::{3}",
         targetReturnTypeReplacement ?? "void",
-        m.EnclosingClass.GetCompileName(Options),
+        clName(m.EnclosingClass),
         InstantiateTemplate(m.EnclosingClass.TypeArgs),
         IdName(m));
 
@@ -1043,7 +1052,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
       } else if (cl is NewtypeDecl) {
         var td = (NewtypeDecl)cl;
         if (td.Witness != null) {
-          return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
+          return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
         } else if (td.NativeType != null) {
           return "0";
         } else {
@@ -1052,7 +1061,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
       } else if (cl is SubsetTypeDecl) {
         var td = (SubsetTypeDecl)cl;
         if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
-          return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
+          return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
         } else if (td.WitnessKind == SubsetTypeDecl.WKind.Special) {
           // WKind.Special is only used with -->, ->, and non-null types:
           Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl);
@@ -1762,7 +1771,7 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
         // This used to work, but now obj comes in wanting to use TypeName on the class, which results in (std::shared_ptr<_module::MyClass>)::c;
         //return SuffixLvalue(obj, "::{0}", member.CompileName);
         return SimpleLvalue(wr => {
-          wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(member.EnclosingClass.GetCompileName(Options)), IdProtect(member.GetCompileName(Options)));
+          wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(clName(member.EnclosingClass)), IdProtect(member.GetCompileName(Options)));
         });
       } else if (member is DatatypeDestructor dtor && dtor.EnclosingClass is TupleTypeDecl) {
         return SuffixLvalue(obj, ".get<{0}>()", dtor.Name);
diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
index 05b0ba6a851..ba17c4a4d15 100644
--- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -193,13 +193,13 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to
       }
     }
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
       if (currentBuilder is ClassContainer builder) {
         List<DAST.TypeArgDecl> typeParams = typeParameters.Select(tp => GenTypeArgDecl(tp)).ToList();
 
         return new ClassWriter(this, typeParams.Count > 0, builder.Class(
-          name, moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(),
+          IdName(cls), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(),
           ParseAttributes(cls.Attributes), GetDocString(cls))
           );
       } else {
diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
index edbeb76c7c0..953f7d43470 100644
--- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -329,16 +329,16 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete
 
     private string HelperModulePrefix => ModuleName == "dafny" ? "" : $"{GetHelperModuleName()}.";
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
       var isDefaultClass = cls is DefaultClassDecl;
 
       bool isSequence = superClasses.Any(superClass => superClass is UserDefinedType udt && IsDafnySequence(udt.ResolvedClass));
-      return CreateClass(cls, name, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence);
+      return CreateClass(cls, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence);
     }
 
     // TODO Consider splitting this into two functions; most things seem to be passing includeRtd: false, includeEquals: false and includeString: true.
-    private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) {
+    private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) {
       // See docs/Compilation/ReferenceTypes.md for a description of how instance members of classes and traits are compiled into Go.
       //
       // func New_Class_(Type0 _dafny.TypeDescriptor, Type1 _dafny.TypeDescriptor) *Class {
@@ -382,7 +382,7 @@ private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, strin
       //   return "module.Class"
       // }
       //
-      name = Capitalize(name);
+      var name = Capitalize(IdName(classContext));
 
       var w = CreateDescribedSection("class {0}", wr, name);
 
@@ -586,7 +586,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
       //   // break becomes:
       //   return
       // }()
-      var cw = CreateClass(iter, IdName(iter), false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true);
+      var cw = CreateClass(iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true);
 
       cw.InstanceFieldWriter.WriteLine("cont chan<- struct{}");
       cw.InstanceFieldWriter.WriteLine("yielded <-chan struct{}");
@@ -1084,7 +1084,7 @@ string StructOfCtor(DatatypeCtor ctor) {
     }
 
     protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
-      var cw = CreateClass(nt, IdName(nt), false, null, nt.TypeArgs,
+      var cw = CreateClass(nt, false, null, nt.TypeArgs,
         nt.ParentTypeInformation.UniqueParentTraits(), null, wr, includeRtd: false, includeEquals: false, includeString: true);
       var w = cw.ConcreteMethodWriter;
       var nativeType = nt.NativeType != null ? GetNativeTypeName(nt.NativeType) : null;
@@ -1130,7 +1130,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre
     }
 
     protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
-      var cw = CreateClass(sst, IdName(sst), false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true);
+      var cw = CreateClass(sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true);
       var w = cw.ConcreteMethodWriter;
       if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
         var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel);
diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
index 868393dc65b..88a80e524e6 100644
--- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -373,7 +373,7 @@ protected override void FinishModule() {
     }
 
     protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr);
       if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
         var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel);
         var wStmts = cw.InstanceMemberWriter.Fork();
@@ -870,8 +870,9 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
     //     }
     //   }
     //
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string /*?*/ fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> /*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
+      var name = IdName(cls);
       var javaName = isExtern ? FormatExternBaseClassName(name) : name;
       var filename = $"{ModulePath}/{javaName}.java";
       var w = wr.NewFile(filename);
@@ -3601,7 +3602,7 @@ protected override void EmitHalt(IOrigin tok, Expression messageExpr, ConcreteSy
     }
 
     protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr);
       var w = cw.StaticMemberWriter;
       if (nt.NativeType != null) {
         var nativeType = GetBoxedNativeTypeName(nt.NativeType);
diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
index 5593c745011..a75fd312f41 100644
--- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
@@ -90,8 +90,9 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri
 
     protected override string GetHelperModuleName() => "_dafny";
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
+      var name = IdName(cls);
       var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";");
       w.Write("constructor (");
       var sep = "";
@@ -160,7 +161,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
       //     }
       //   }
 
-      var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr) as JavaScriptCodeGenerator.ClassWriter;
+      var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr) as JavaScriptCodeGenerator.ClassWriter;
       var w = cw.MethodWriter;
       var instanceFieldsWriter = cw.FieldWriter;
       // here come the fields
@@ -575,7 +576,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
     }
 
     protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr);
       var w = cw.MethodWriter;
       if (nt.NativeType != null) {
         var wIntegerRangeBody = w.NewBlock("static *IntegerRange(lo, hi)");
@@ -638,7 +639,7 @@ void GenerateIsMethod(RedirectingTypeDecl declWithConstraints, ConcreteSyntaxTre
     }
 
     protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr);
       var w = cw.MethodWriter;
       var udt = UserDefinedType.FromTopLevelDecl(sst.Origin, sst);
       string d;
diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
index 7654c96ec0e..e95837a998b 100644
--- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -231,12 +231,13 @@ private static string MangleName(string name) {
       return name;
     }
 
-    protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName,
+    protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
       var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List<Type>();
       var baseClasses = realSuperClasses.Any()
         ? $"({realSuperClasses.Comma(trait => TypeName(trait, wr, tok))})"
         : "";
+      var name = IdName(cls);
       var methodWriter = wr.NewBlockPy(header: $"class {IdProtect(name)}{baseClasses}:");
 
       var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor).ToList();
@@ -276,7 +277,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List<Typ
     }
 
     protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
-      var cw = (ClassWriter)CreateClass(PublicModuleIdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), false,
+      var cw = (ClassWriter)CreateClass(PublicModuleIdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), false,
         iter.FullName, iter.TypeArgs, iter, null, iter.Origin, wr);
       var constructorWriter = cw.ConstructorWriter;
       var w = cw.MethodWriter;
@@ -458,7 +459,7 @@ private string DtCtorDeclarationName(DatatypeCtor ctor, bool full = false) {
     protected IClassWriter DeclareType(TopLevelDecl d, SubsetTypeDecl.WKind witnessKind, Expression witness, ConcreteSyntaxTree wr) {
       Contract.Requires(d is SubsetTypeDecl or NewtypeDecl);
 
-      var cw = (ClassWriter)CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(d), d, wr);
+      var cw = (ClassWriter)CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), d, wr);
       var w = cw.MethodWriter;
       var udt = UserDefinedType.FromTopLevelDecl(d.Origin, d);
       w.WriteLine("@staticmethod");
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
index 8b17121ed14..0d3c5a7b5f2 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
@@ -218,15 +218,15 @@ protected interface IClassWriter {
     protected virtual bool SupportsStaticsInGenericClasses => true;
     protected virtual bool TraitRepeatsInheritedDeclarations => false;
     protected virtual bool InstanceMethodsAllowedToCallTraitMethods => true;
-    protected IClassWriter CreateClass(string moduleName, string name, TopLevelDecl cls, ConcreteSyntaxTree wr) {
-      return CreateClass(moduleName, name, false, null, cls.TypeArgs,
+    protected IClassWriter CreateClass(string moduleName, TopLevelDecl cls, ConcreteSyntaxTree wr) {
+      return CreateClass(moduleName, false, null, cls.TypeArgs,
         cls, (cls as TopLevelDeclWithMembers)?.ParentTypeInformation.UniqueParentTraits(), null, wr);
     }
 
     /// <summary>
     /// "tok" can be "null" if "superClasses" is.
     /// </summary>
-    protected abstract IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName,
+    protected abstract IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName,
       List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr);
 
     /// <summary>
@@ -1685,7 +1685,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
           if (include) {
             var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)),
-              IdName(defaultClassDecl),
               classIsExtern, defaultClassDecl.FullName,
               defaultClassDecl.TypeArgs, defaultClassDecl,
               defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.Origin, wr);
@@ -1700,7 +1699,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
           var (classIsExtern, include) = GetIsExternAndIncluded(cl);
 
           if (include) {
-            var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl),
+            var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)),
               classIsExtern, cl.FullName,
               cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.Origin, wr);
             CompileClassMembers(program, cl, cw);
diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
index 2983c3dbf3b..59ffe8bfcbe 100644
--- a/Source/DafnyCore/Options/BoogieOptionBag.cs
+++ b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -51,8 +51,8 @@ public static class BoogieOptionBag {
     IsHidden = true
   };
 
-  public static readonly Option<uint> VerificationTimeLimit = new("--verification-time-limit",
-    "Limit the number of seconds spent trying to verify each procedure") {
+  public static readonly Option<uint> VerificationTimeLimit = new("--verification-time-limit", () => 30,
+    "Limit the number of seconds spent trying to verify each assertion batch. A value of 0 indicates no limit") {
     ArgumentHelpName = "seconds",
   };
 
diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
index d89a6b973fd..0ecaadeae78 100644
--- a/Source/DafnyCore/Pipeline/Compilation.cs
+++ b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -4,6 +4,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.CommandLine;
+using System.CommandLine.Help;
 using System.IO;
 using System.Linq;
 using System.Reactive;
@@ -560,17 +561,96 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
       errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel);
     }
 
-    // This reports problems that are not captured by counter-examples, like a time-out
-    // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options.
-    var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(),
-      CustomStackSizePoolTaskScheduler.Create(0, 0));
-    boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false),
-      name, token, null, TextWriter.Null,
-      timeLimit, result.CounterExamples);
+    var outcomeError = ReportOutcome(options, outcome, name, token, timeLimit, result.CounterExamples);
+    if (outcomeError != null) {
+      errorReporter.ReportBoogieError(outcomeError, null, false);
+    }
+  }
+
+  private static ErrorInformation? ReportOutcome(DafnyOptions options,
+      VcOutcome vcOutcome, string name,
+      IToken token, uint timeLimit, List<Counterexample> errors) {
+    ErrorInformation? errorInfo = null;
+
+    switch (vcOutcome) {
+      case VcOutcome.Correct:
+        break;
+      case VcOutcome.Errors:
+      case VcOutcome.TimedOut: {
+          if (vcOutcome != VcOutcome.TimedOut &&
+              (!errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) {
+            break;
+          }
+
+          string msg = string.Format("Verification of '{1}' timed out after {0} seconds. (the limit can be increased using --verification-time-limit)", timeLimit, name);
+          errorInfo = ErrorInformation.Create(token, msg);
+
+          //  Report timed out assertions as auxiliary info.
+          var comparer = new CounterexampleComparer();
+          var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(comparer)
+            .OrderBy(x => x, comparer).ToList();
+          if (0 < timedOutAssertions.Count) {
+            errorInfo!.Msg += $" with {timedOutAssertions.Count} check(s) that timed out individually";
+          }
+
+          foreach (Counterexample error in timedOutAssertions) {
+            IToken tok;
+            string auxMsg = null!;
+            switch (error) {
+              case CallCounterexample callCounterexample:
+                tok = callCounterexample.FailingCall.tok;
+                auxMsg = callCounterexample.FailingCall.Description.FailureDescription;
+                break;
+              case ReturnCounterexample returnCounterexample:
+                tok = returnCounterexample.FailingReturn.tok;
+                auxMsg = returnCounterexample.FailingReturn.Description.FailureDescription;
+                break;
+              case AssertCounterexample assertError: {
+                  tok = assertError.FailingAssert.tok;
+                  if (!(assertError.FailingAssert.ErrorMessage == null ||
+                        ((ExecutionEngineOptions)options).ForceBplErrors)) {
+                    auxMsg = assertError.FailingAssert.ErrorMessage;
+                  }
+
+                  auxMsg ??= assertError.FailingAssert.Description.FailureDescription;
+                  break;
+                }
+              default: throw new Exception();
+            }
+
+            errorInfo.AddAuxInfo(tok, auxMsg, "Unverified check due to timeout");
+          }
+
+          break;
+        }
+      case VcOutcome.OutOfResource: {
+          string msg = "Verification out of resource (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+      case VcOutcome.OutOfMemory: {
+          string msg = "Verification out of memory (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+      case VcOutcome.SolverException: {
+          string msg = "Verification encountered solver exception (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+
+      case VcOutcome.Inconclusive: {
+          string msg = "Verification inconclusive (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+    }
+
+    return errorInfo;
   }
 
   private static void AddAssertedExprToCounterExampleErrorInfo(
-      DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
+    DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
     Boogie.ProofObligationDescription? boogieProofObligationDesc = null;
     switch (errorInformation.Kind) {
       case ErrorKind.Assertion:
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index 0177973871e..bbe45a1e715 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -1665,9 +1665,13 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt
         }
       }
 
-      var kv = etran.TrAttributes(m.Attributes, null);
 
+      var kv = etran.TrAttributes(m.Attributes, null);
       var tok = m.Origin;
+      var canCalls = traitFrameExps.Concat(classFrameExps)
+        .Select(e => etran.CanCallAssumption(e.E))
+        .Aggregate((Bpl.Expr)Bpl.Expr.True, BplAnd);
+      builder.Add(TrAssumeCmd(tok, canCalls));
       var oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", Predef.RefType));
       var o = new Boogie.IdentifierExpr(tok, oVar);
       var fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", Predef.FieldName(tok)));
diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs
index a4cdf8c92b3..51381672ef5 100644
--- a/Source/DafnyDriver/Commands/ServerCommand.cs
+++ b/Source/DafnyDriver/Commands/ServerCommand.cs
@@ -1,6 +1,4 @@
-using System.Collections.Generic;
 using System.CommandLine;
-using DafnyCore;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index f928e3f5043..0236f2ce5f6 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -13,16 +13,6 @@
 
       <IsPackable>true</IsPackable>
   </PropertyGroup>
-
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
     
   <ItemGroup>
     <PackageReference Include="Microsoft.TestPlatform.Extensions.TrxLogger" Version="17.9.0" />
@@ -42,8 +32,8 @@
     
   <ItemGroup>
     <ProjectReference Include="..\DafnyCore\DafnyCore.csproj" />
+    <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
   </ItemGroup>
   
   <ItemGroup>
diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
index 93087fe8e5d..e6e27c8b151 100644
--- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
+++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
@@ -4,7 +4,6 @@
 using System.Linq;
 using System.Text.Json.Nodes;
 using DafnyCore.Verifier;
-using DafnyServer;
 using Microsoft.Boogie;
 using VC;
 
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
index 67513425d4e..92f1fad7dff 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
@@ -6,7 +6,6 @@
     <Nullable>enable</Nullable>
     <RootNamespace>Microsoft.Dafny.LanguageServer</RootNamespace>
     <OutputPath>..\..\Binaries\</OutputPath>
-    <IsPackable>true</IsPackable>
     <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
     <PackageReadmeFile>README.md</PackageReadmeFile>
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
index fc267756b73..5e7e3a67e82 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
@@ -2106,7 +2106,7 @@ impl DafnyPrint for () {
     }
 }
 
-#[derive(Clone)]
+#[derive(Clone, Copy)]
 pub struct DafnyCharUTF16(pub u16);
 pub type DafnyStringUTF16 = Sequence<DafnyCharUTF16>;
 
@@ -2182,7 +2182,7 @@ impl Sub<DafnyCharUTF16> for DafnyCharUTF16 {
     }
 }
 
-#[derive(Clone)]
+#[derive(Clone, Copy)]
 pub struct DafnyChar(pub char);
 pub type DafnyString = Sequence<DafnyChar>;
 
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
index 6f04042bd62..f3ce7796c7f 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
@@ -1022,6 +1022,18 @@ mod tests {
         assert_eq!(gtsgt._as_Datatype(), x);
         assert_eq!(gtsgt._as_Datatype(), x);
     }
+
+    #[test]
+    fn test_chars_copy() {
+        let c = DafnyChar('a');
+        let c2 = c;
+        let c3 = c;
+        assert_eq!(c3, c2);
+        let c = DafnyCharUTF16(213);
+        let c2 = c;
+        let c3 = c;
+        assert_eq!(c3, c2);
+    }
     /*impl GeneralTrait for Rc<ADatatype> {
         fn _clone(&self) -> Box<dyn GeneralTrait> {
             Box::new(self.as_ref().clone())
diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj
index d736ee1074e..f9cd46eb532 100644
--- a/Source/DafnyServer/DafnyServer.csproj
+++ b/Source/DafnyServer/DafnyServer.csproj
@@ -10,16 +10,6 @@
       <PackageLicenseExpression>MIT</PackageLicenseExpression>
   </PropertyGroup>
 
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
-
   <ItemGroup>
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
index 016cf01c491..f4f2f78ffd1 100644
--- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
+++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
@@ -15,7 +15,6 @@
   </PropertyGroup>
   
   <ItemGroup>
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy
new file mode 100644
index 00000000000..e91e3331f33
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy
@@ -0,0 +1,17 @@
+// RUN: ! %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Foo() {
+  // Assert something that takes a long time to verify
+  assert Ack(4, 2) == 1;
+}
+
+function Ack(m: nat, n: nat): nat
+{
+  if m == 0 then
+    n + 1
+  else if n == 0 then
+    Ack(m - 1, 1)
+  else
+    Ack(m - 1, Ack(m, n - 1))
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect
new file mode 100644
index 00000000000..b7677c39850
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect
@@ -0,0 +1,7 @@
+defaultTimeLimit.dfy(4,7): Error: Verification of 'Foo' timed out after 30 seconds. (the limit can be increased using --verification-time-limit)
+  |
+4 | method Foo() {
+  |        ^^^
+
+
+Dafny program verifier finished with 1 verified, 0 errors, 1 time out
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy
deleted file mode 100644
index 9ce07b0f267..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy
+++ /dev/null
@@ -1,2 +0,0 @@
-// RUN: %exits-with 1 %baredafny "" 2> "%t"
-// RUN: %diff "%s.expect" "%t"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect
deleted file mode 100644
index 3ccac32363e..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect
+++ /dev/null
@@ -1 +0,0 @@
-Invalid filename: The value cannot be an empty string. (Parameter 'path')
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
index e7965e56414..2c2bc4bc249 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
@@ -1,5 +1,5 @@
 git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated
-git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
+git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds. (the limit can be increased using --verification-time-limit)
 git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved
 git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check
deleted file mode 100644
index a8dfdf5ec16..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check
+++ /dev/null
@@ -1 +0,0 @@
-CHECK: Failed to compile C# source code .*
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect
new file mode 100644
index 00000000000..dcab703fd3b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect
@@ -0,0 +1,3 @@
+AnyName.B
+AnyName._AnyName
+done
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check
deleted file mode 100644
index 6d927bd7912..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check
+++ /dev/null
@@ -1 +0,0 @@
-CHECK: error: cannot find symbol
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
index 38f582328fa..b43e78bfeb9 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
@@ -1,6 +1,4 @@
-// NONUNIFORM: Test still fails on CS (https://github.com/dafny-lang/dafny/issues/5746)
-// RUN: %run --target java "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" 
 
 module State {
 
@@ -17,4 +15,47 @@ module Foo {
    method Main() {
      print "Hello!\n";
   }
-}
\ No newline at end of file
+}
+
+module Enclosing {
+
+  module A {
+    datatype A = Whatever
+  }
+
+}
+
+module UsingEnclosing {
+
+   import opened Enclosing
+
+   const bar: A.A
+
+   method Main2() {
+     print "Hello!\n";
+  }
+}
+
+module A {
+
+  trait T<X> {
+    var a: X
+  }
+
+  class A extends T<int> {
+    var x : int
+    constructor() {x := 0;}
+  }
+
+}
+
+module UsingA {
+
+   import opened A
+
+   method Main3() {
+     var b := new A();
+
+     print "Hello!\n";
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect
index 3b538928db8..10ddd6d257e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect
@@ -1,3 +1 @@
-
-Dafny program verifier finished with 0 verified, 0 errors
 Hello!
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy
new file mode 100644
index 00000000000..8a0794b9789
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy
@@ -0,0 +1,22 @@
+// RUN: %verify %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+
+  ghost function Modifies(): set<object>
+
+  method Foo()
+    modifies Modifies()
+}
+
+class {:compile false} C extends T {
+
+  const Repr: set<object>
+
+  ghost function Modifies(): set<object> {
+    Repr
+  }
+
+  method Foo()
+    modifies Modifies()
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy.expect
new file mode 100644
index 00000000000..ebe2328e072
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 578b63c6924..8fd4ce1c5dc 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -2769,7 +2769,7 @@ The following options are also commonly used:
   but a large positive number reports more errors per run
 
 * `--verification-time-limit:<n>` (was `-timeLimit:<n>`) - limits 
-  the number of seconds spent trying to verify each procedure.
+  the number of seconds spent trying to verify each assertion batch.
 
 
 ### 13.9.11. Controlling test generation {#sec-controlling-test-gen}
diff --git a/docs/news/fix.6006 b/docs/news/6006.fix
similarity index 100%
rename from docs/news/fix.6006
rename to docs/news/6006.fix
diff --git a/docs/news/6028.feat b/docs/news/6028.feat
new file mode 100644
index 00000000000..2bfb7957467
--- /dev/null
+++ b/docs/news/6028.feat
@@ -0,0 +1 @@
+Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit)
\ No newline at end of file
diff --git a/docs/news/fix.5746 b/docs/news/fix.5746
new file mode 100644
index 00000000000..19e1b00b370
--- /dev/null
+++ b/docs/news/fix.5746
@@ -0,0 +1 @@
+Fix C# generated code when a module contains a type with the same name
diff --git a/docs/news/fix.6014 b/docs/news/fix.6014
new file mode 100644
index 00000000000..614d71f3329
--- /dev/null
+++ b/docs/news/fix.6014
@@ -0,0 +1 @@
+Fix Java generated code when a module contains a type with the same name