1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
new file mode 100644
index 00000000..301a4e94
--- /dev/null
+++ b/Test/dafny0/Compilation.dfy
@@ -0,0 +1,13 @@
+// The tests in this file are designed to run through the compiler.  They contain
+// program snippets that are tricky to compile or whose compilation once was buggy.
+
+datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
+
+method M<U>(x: MyDt<int>)
+{
+  match (x) {
+    case Cons(head, tail) =>
+      var y: int := head;
+    case Nil =>
+  }
+}