diff options
| author | Guillaume Melquiond | 2020-08-31 08:55:28 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-10-08 11:22:24 +0200 |
| commit | c3cfb3c26241c374545380f08aa4345eb553000e (patch) | |
| tree | 6962bd3aba332715f49dcd64baa0f0956b98332f | |
| parent | e3764e1e857fce9b6d4cb018db676db3612c00a0 (diff) | |
Check complexity of primitive arrays.
| -rw-r--r-- | test-suite/bugs/closed/bug_12947.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |