diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
index dbfb67041a..d8092b8467 100644
--- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -2490,6 +2490,7 @@ public override string PublicIdProtect(string name) {
         case "ToString":
         case "GetHashCode":
         case "Main":
+        case "Default":
           return "_" + name;
         default:
           return name;
diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
index 953f7d4347..12dfa815b0 100644
--- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -2515,7 +2515,7 @@ private string IdName(Declaration decl) {
         // Don't use Go_ because Capitalize might use it and we know there's a conflict
         return "Go__" + decl.GetCompileName(Options);
       } else {
-        return Capitalize(decl.GetCompileName(Options));
+        return IdProtect(Capitalize(decl.GetCompileName(Options)));
       }
     }
 
@@ -2579,6 +2579,7 @@ public override string PublicIdProtect(string name) {
         case "String":
         case "Equals":
         case "EqualsGeneric":
+        case "Default":
 
         // Built-in types (can also be used as functions)
         case "bool":
diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
index 88a80e524e..89c86b482a 100644
--- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -2440,6 +2440,7 @@ private static string PublicIdProtectAux(string name) {
         case "toString":
         case "equals":
         case "hashCode":
+        case "Default":
           return name + "_"; // TODO: figure out what to do here (C# uses @, Go uses _, JS uses _$$_)
         default:
           return name; // Package name is not a keyword, so it can be used
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy
new file mode 100644
index 0000000000..be8e13ec89
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy
@@ -0,0 +1,26 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" 
+
+module m {
+  datatype D = A
+             | B
+             | C {
+    static const Default: D := B // This one will be translated as Default_
+    method Default_() { // Just to be sure there is no clash: this is translated as Default__
+      print "Default_ Method\n";
+    }
+  }
+
+
+
+  method Main() {
+    var x := D.Default;
+    x.Default_();
+    match x {
+      case A => print "A!\n";
+      case B => print "B!\n";
+      case C => print "C!\n";
+    }
+    print "Hello!\n";
+  }
+
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect
new file mode 100644
index 0000000000..9ba695c450
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect
@@ -0,0 +1,3 @@
+Default_ Method
+B!
+Hello!