diff options
| -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. |