1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 2bff422f..d8ff3989 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -210,3 +210,20 @@ module GhostLetExpr {
     G(5, xyz)
   }
 }
+
+class DigitUnderscore_Names {
+  // the following would be the same integers, but they are different fields
+  var 0_1_0: int;
+  var 010: int;
+  var 10: int;
+  // ... as we see here:
+  method M()
+    modifies this;
+  {
+    this.0_1_0 := 007;
+    this.010 := 000_008;
+    this.10 := 0x0000_0009;
+    assert this.0_1_0 == int(00_07.0_0) && this.010 == 8 && this.10 == 9;
+    this.10 := 20;
+  }
+}