diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs
index 3d31b95d1dc..71815f08d36 100644
--- a/Source/DafnyCore/DooFile.cs
+++ b/Source/DafnyCore/DooFile.cs
@@ -54,7 +54,7 @@ public static ManifestData Read(TextReader reader) {
     }
 
     public void Write(TextWriter writer) {
-      writer.Write(Toml.FromModel(this, new TomlModelOptions()));
+      writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n"));
     }
   }
 
@@ -103,7 +103,9 @@ private static DooFile Read(ZipArchive archive) {
   }
 
   public DooFile(Program dafnyProgram) {
-    var tw = new StringWriter();
+    var tw = new StringWriter {
+      NewLine = "\n"
+    };
     var pr = new Printer(tw, ProgramSerializationOptions, PrintModes.Serialization);
     // afterResolver is false because we don't yet have a way to safely skip resolution
     // when reading the program back into memory.
@@ -191,7 +193,7 @@ public void Write(ConcreteSyntaxTree wr) {
     var manifestWr = wr.NewFile(ManifestFileEntry);
     using var manifestWriter = new StringWriter();
     Manifest.Write(manifestWriter);
-    manifestWr.Write(manifestWriter.ToString());
+    manifestWr.Write(manifestWriter.ToString().Replace("\r\n", "\n"));
 
     var programTextWr = wr.NewFile(ProgramFileEntry);
     programTextWr.Write(ProgramText);
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
index b42c835e832..9fe2b35e51c 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ
diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
index dd7095061ff..eaddebc3a3c 100644
--- a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
@@ -666,7 +666,7 @@ module Std.Collections.Seq {
     Some((s[..i], s[(i + 1)..]))
   }
 
-  lemma WillSplitOnDelim<T>(s: seq<T>, delim: T, prefix: seq<T>)
+  lemma {:rlimit 1000} {:vcs_split_on_every_assert} WillSplitOnDelim<T>(s: seq<T>, delim: T, prefix: seq<T>)
     requires |prefix| < |s|
     requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i]
     requires delim !in prefix && s[|prefix|] == delim
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy
new file mode 100644
index 00000000000..2d2b01476d7
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy
@@ -0,0 +1,11 @@
+// RUN: %baredafny verify %args --type-system-refresh --general-traits=datatype "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait Test<T> {
+  function Cast(t: T): Test<T>
+}
+
+datatype Impl extends Test<Impl> = ImplConstructor()
+{
+  function Cast(t: Impl): Test<Impl> { t }
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/4823.fix b/docs/dev/news/4823.fix
new file mode 100644
index 00000000000..400cee8379b
--- /dev/null
+++ b/docs/dev/news/4823.fix
@@ -0,0 +1 @@
+Ability to cast a datatype to its trait when overriding functions
\ No newline at end of file