From 7ba4dee1dd9bf600256827b3517db338d7390566 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 24 Oct 2016 14:54:05 +0200
Subject: Test file for #5127: Memory corruption with the VM

---
 test-suite/bugs/closed/5127.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/5127.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v
new file mode 100644
index 0000000000..831e8fb507
--- /dev/null
+++ b/test-suite/bugs/closed/5127.v
@@ -0,0 +1,15 @@
+Fixpoint arrow (n: nat) :=
+  match n with
+  | S n => bool -> arrow n
+  | O => bool
+  end.
+
+Fixpoint apply (n : nat) : arrow n -> bool :=
+  match n return arrow n -> bool with
+  | S n => fun f => apply _ (f true)
+  | O => fun x => x
+  end.
+
+Axiom f : arrow 10000.
+Definition v : bool := Eval compute in apply _ f.
+Definition w : bool := Eval vm_compute in v.
-- 
cgit v1.2.3