From c3cfb3c26241c374545380f08aa4345eb553000e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 31 Aug 2020 08:55:28 +0200
Subject: Check complexity of primitive arrays.

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

diff --git a/test-suite/bugs/closed/bug_12947.v b/test-suite/bugs/closed/bug_12947.v
new file mode 100644
index 0000000000..baf0579465
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12947.v
@@ -0,0 +1,9 @@
+Require Import BinPos Int63 PArray.
+
+Definition foo (n : positive) :=
+  let a := make 2 0 in
+  let b := Pos.iter (fun b => set b 1 1) a 100000 in
+  let v := get b 0 in
+  Pos.iter (fun v => v + get a 0) v n.
+
+Timeout 5 Time Eval vm_compute in foo 1000000.
-- 
cgit v1.2.3