8000 Timeout due to excessive shrinking in `Lin Dynarray test with Domain` · Issue #514 · ocaml-multicore/multicoretests · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Timeout due to excessive shrinking in Lin Dynarray test with Domain #514

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
jmid opened this issue Jan 15, 2025 · 1 comment · Fixed by #517
Closed

Timeout due to excessive shrinking in Lin Dynarray test with Domain #514

jmid opened this issue Jan 15, 2025 · 1 comment · Fixed by #517
Labels
test suite reliability Issue concerns tests that should behave more predictably

Comments

@jmid
Copy link
Collaborator
jmid commented Jan 15, 2025

On #513 in the Cygwin trunk workflow we just saw an excessively long shrinking run causing a timeout:
https://github.com/ocaml-multicore/multicoretests/actions/runs/12777231067/job/35617614765?pr=513

random seed: 302513680
generated error fail pass / total     time test name

[ ]    0    0    0    0 / 1000     0.0s Lin Dynarray test with Domain
[ ]    0    0    0    0 / 1000     0.0s Lin Dynarray test with Domain (generating)
[ ]    0    0    0    0 / 1000    60.1s Lin Dynarray test with Domain (shrinking:   15.0195)
[ ]    0    0    0    0 / 1000   120.2s Lin Dynarray test with Domain (shrinking:   15.0533)
[ ]    0    0    0    0 / 1000   180.2s Lin Dynarray test with Domain (shrinking:   15.0871)

[...]

[ ]    0    0    0    0 / 1000  7409.1s Lin Dynarray test with Domain (shrinking:   92.0853)
[ ]    0    0    0    0 / 1000  7469.2s Lin Dynarray test with Domain (shrinking:   92.1169)
[ ]    0    0    0    0 / 1000  7529.2s Lin Dynarray test with Domain (shrinking:   92.1372)
Error: The operation was canceled.

Despite having found an expected counter example and succesfully reduced it 15 times within the first 60.1s,
Lin spends an additional 2h ~ 124min (7529.2 -. 60.1) /. 60.) reducing it - and eventually causing a timeout...
@jmid jmid added the test suite reliability Issue concerns tests that should behave more predictably label Jan 15, 2025
This was referenced Jan 15, 2025
Merged
Closed
@jmid
Copy link
Collaborator Author
jmid commented Jan 15, 2025

Rerunning locally on Linux with

$ dune exec src/dynarray/lin_tests.exe -- -v -s 302513680 --debug-shrink shrink.log

I'm seeing a very long sequence (7487-element or so) in shrink.log:

          append_seq t <8; 7; 4; 0; 23; 2; 31; 38; 4; 64; 2; 3; 7; 3; 1; 7; 11; 4; 7; 58; 1; 9; 2; 7; 67; 4; 2; 96; 3; 9; 7; 2; 4; 5; 5; 8; 1; 5; 9; 1; 89; 5; 5; 94; 1; 4; 79; 0; 6; 38; 30; 2; 2; 4; 8; 6; 8; 8; 1; 6; 1; 1; 57; 6; 8; 5; 0; 1; 3; 0; 0; 5; 4; 6; 6; 45; 6; 1; 73; 6; 77; 7; 95; 1; 4; 75; 4; 2; 0; 33; 8; 21; 8; 3; 2; 5; 20; 0; 2; 79; 8; 8; 9; 88; 5; 0; 2; 5; 0; 29; 5; 2; 2; 0; 0; 7; 5; 6; 74; 1; 97; 4; 3; 0; 87; 7; 6; 0; 8; 4; 2; 5; 1; 61; 0; 4; 8; 4; 26; 5; 7; 9; 8; 3; 6; 23; 46; 8; 7; 24; 5; 8; 73; 59; 26; 4; 0; 6; 4; 6; 33; 93; 85; 3; 8; 3; 1; 47; 8; 9; 9; 7; 2; 9; 6; 1; 6; 52; 6; 1; 7; 7; 5; 33; 7; 1; 7; 10; 96; 4; 1; 9; 40; 6; 1; 1; 65; 86; 1; 56; 6; 5; 8; 2; 7; 8; 4; 3; 50; 5; 2; 7; 61; 6; 9; 6; 29; 9; 3; 9; 4; 2; 6; 50; 36; 5; 4; 2; 8; 6; 3; 6; 6; 0; 1; 7; 0; 3; 39; 82; 1; 5; 13; 2; 8; 2; 2; 6; 13; 6; 8; 4; 3; 0; 2; 8; 21; 4; 9; 4; 8; 67; 0; 8; 7; 43; 3; 8; 1; 5; 6; 4; 5; 1; 90; 92; 5; 57; 57; 44; 46; 4; 22; 8; 9; 9; 0; 99; 66; 92; 4; 0; 33; 4; 9; 6; 17; 30; 2; 1; 32; 0; 4; 9; 24; 7; 18; 1; 8; 9; 48; 16; 8; 5; 67; 5; 0; 8; 4; 7; 5; 6; 2; 5; 4; 5; 7; 2; 7; 9; 9; 3; 0; 3; 63; 49; 4; 9; 0; 5; 7; 6; 87; 5; 7; 74; 2; 1; 1; 19; 6; 0; 7; 83; 53; 61; 1; 1; 5; 3; 0; 5; 0; 9; 7; 52; 0; 0; 0; 8; 1; 0; 3; 0; 9; 0; 5; 7; 8; 8; 0; 0; 0; 1; 3; 5; 1; 6; 8; 0; 61; 9; 3; 6; 71; 7; 7; 90; 3; 4; 1; 28; 4; 5; 1; 74; 50; 7; 5; 22; 7; 3; 43; 54; 91; 4; 4; 0; 7; 1; 8; 28; 0; 49; 74; 29; 62; 3; 74; 58; 3; 5; 5; 49; 4; 5; 3; 8; 5; 3; 83; 0; 4; 6; 7; 4; 6; 98; 4; 4; 8; 30; 9; 52; 7; 0; 54; 9; 2; 0; 8; 9; 5; 0; 1; 3; 9; 2; 7; 8; 53; 8; 1; 5; 4; 8; 6; 5; 8; 24; 2; 51; 70; 7; 1; 7; 8; 6; 0; 3; 9; 7; 1; 4; 7; 33; 30; 6; 42; 4; 3; 5; 38; 3; 8; 3; 71; 7; 9; 6; 4; 0; 6; 5; 1; 6; 5; 4; 5; 85; 0; 2; 1; 16; 7; 8; 8; 9; 24; 4; 15; 6; 2; 31; 47; 25; 3; 9; 5; 27; 5; 8; 3; 2; 8; 6; 0; 6; 89; 7; 58; 3; 5; 9; 20; 9; 44; 9; 7; 2; 0; 4; 74; 1; 40; 7; 6; 0; 8; 6; 2; 4; 7; 43; 9; 9; 4; 8; 7; 4; 0; 8; 9; 1; 2; 8; 3; 6; 0; 2; 3; 1; 3; 34; 70; 78; 9; 6; 4; 65; 0; 0; 3; 0; 3; 59; 0; 7; 6; 3; 2; 7; 2; 2; 3; 6; 42; 6; 7; 1; 5; 6; 3; 9; 5; 6; 56; 8; 8; 9; 5; 3; 43; 81; 4; 8; 0; 3; 6; 68; 15; 9; 76; 67; 8; 4; 2; 22; 6; 7; 2; 9; 3; 0; 1; 68; 88; 4; 6; 6; 4; 1; 8; 9; 5; 15; 55; 7; 4; 82; 6; 5; 0; 24; 34; 4; 0; 1; 7; 68; 3; 3; 94; 7; 3; 78; 47; 5; 3; 1; 3; 4; 7; 6; 6; 15; 0; 36; 5; 2; 4; 4; 62; 0; 5; 2; 3; 5; 6; 6; 3; 0; 7; 7; 94; 6; 8; 5; 4; 6; 9; 34; 5; 5; 9; 9; 7; 8; 58; 9; 1; 41; 9; 82; 4; 1; 4; 5; 89; 7; 23; 35; 5; 44; 7; 7; 5; 1; 5; 31; 55; 7; 66; 28; 2; 0; 3; 2; 7; 4; 8; 0; 86; 9; 93; 7; 1; 7; 9; 7; 25; 49; 7; 68; 0; 6; 1; 9; 55; 42; 8; 98; 34; 0; 98; 8; 7; 1; 4; 1; 6; 6; 20; 7; 9; 99; 0; 89; 53; 69; 2; 8; 9; 0; 6; 96; 41; 4; 0; 7; 7; 31; 9; 7; 1; 41; 7; 7; 2; 29; 1; 6; 3; 9; 4; 0; 52; 85; 2; 76; 9; 7; 6; 96; 6; 9; 0; 3; 3; 7; 68; 4; 79; 47; 47; 55; 99; 71; 83; 79; 3; 0; 2; 4; 9; 2; 7; 94; 70; 6; 0; 8; 6; 94; 82; 6; 7; 2; 2; 5; 1; 8; 1; 2; 0; 6; 2; 51; 0; 2; 2; 5; 1; 3; 0; 6; 0; 3; 1; 5; 6; 4; 9; 1; 1; 8; 5; 9; 9; 63; 5; 5; 92; 1; 6; 74; 3; 0; 2; 4; 58; 19; 6; 25; 94; 9; 37; 6; 86; 0; 0; 80; 1; 7; 4; 2; 8; 24; 9; 70; 56; 2; 6; 1; 9; 1; 8; 3; 3; 5; 7; 2; 17; 6; 8; 5; 8; 18; 0; 9; 57; 24; 7; 6; 0; 3; 34; 7; 3; 6; 7; 4; 1; 4; 6; 8; 0; 0; 10; 3; 9; 0; 0; 95; 69; 83; 7; 28; 5; 1; 1; 9; 6; 8; 95; 9; 6; 3; 4; 7; 80; 2; 9; 6; 67; 41; 1; 8; 0; 7; 7; 7; 6; 4; 9; 9; 9; 8; 49; 5; 5; 2; 6; 29; 0; 6; 0; 2; 6; 6; 9; 2; 3; 54; 8; 1; 6; 3; 86; 8; 4; 3; 7; 5; 8; 6; 2; 2; 4; 4; 84; 2; 1; 83; 94; 3; 1; 7; 9; 3; 7; 96; 1; 13; 9; 2; 51; 9; 5; 53; 71; 4; 2; 2; 5; 74; 0; 30; 0; 4; 6; 6; 4; 18; 8; 8; 5; 85; 8; 4; 65; 5; 85; 89; 29; 0; 79; 60; 18; 8; 6; 6; 8; 12; 56; 4; 5; 79; 8; 82; 9; 7; 0; 1; 13; 0; 0; 31; 31; 3; 0; 3; 6; 2; 6; 8; 5; 3; 8; 9; 3; 48; 16; 20; 2; 2; 3; 60; 5; 46; 15; 9; 38; 5; 1; 2; 86; 0; 5; 8; 9; 7; 0; 8; 2; 9; 6; 6; 2; 0; 1; 72; 0; 51; 0; 2; 8; 37; 82; 9; 6; 9; 87; 3; 0; 6; 9; 3; 8; 1; 98; 72; 8; 94; 8; 5; 8; 3; 74; 2; 3; 24; 9; 2; 4; 0; 8; 4; 6; 0; 28; 99; 7; 27; 25; 4; 6; 2; 5; 58; 97; 6; 99; 84; 9; 0; 45; 67; 9; 3; 0; 0; 8; 32; 7; 50; 86; 3; 8; 2; 2; 5; 2; 20; 9; 82; 4; 84; 7; 63; 2; 96; 9; 59; 3; 90; 7; 7; 4; 9; 69; 34; 7; 87; 4; 51; 49; 9; 5; 8; 73; 3; 2; 0; 1; 6; 6; 9; 20; 40; 0; 3; 47; 8; 4; 9; 7; 9; 0; 89; 5; 28; 8; 78; 3; 7; 38; 3; 0; 0; 23; 58; 3; 13; 40; 6; 8; 0; 6; 8; 1; 8; 1; 66; 7; 5; 0; 61; 5; 0; 0; 9; 7; 4; 3; 3; 6; 8; 1; 21; 7; 9; 2; 8; 81; 1; 6; 34; 8; 0; 9; 7; 4; 5; 1; 5; 4; 6; 3; 6; 26; 6; 6; 5; 2; 2; 4; 24; 0; 98; 11; 2; 22; 3; 4; 6; 2; 4; 8; 4; 2; 9; 9; 77; 1; 5; 2; 8; 4; 35; 6; 8; 42; 5; 4; 9; 85; 84; 5; 56; 69; 6; 43; 9; 0; 7; 63; 8; 3; 9; 0; 2; 0; 6; 9; 3; 60; 9; 3; 6; 6; 7; 0; 7; 6; 6; 15; 6; 4; 7; 6; 49; 2; 46; 9; 99; 9; 3; 6; 7; 3; 8; 9; 6; 78; 7; 4; 7; 1; 6; 3; 9; 0; 7; 0; 54; 2; 7; 9; 0; 0; 4; 8; 4; 2; 95; 9; 0; 3; 25; 53; 1; 3; 35; 7; 5; 7; 8; 3; 3; 70; 38; 47; 8; 1; 9; 6; 9; 1; 7; 0; 2; 5; 3; 7; 35; 2; 6; 8; 1; 2; 82; 0; 1; 6; 8; 1; 8; 4; 7; 6; 1; 3; 93; 3; 0; 21; 8; 62; 2; 8; 89; 6; 13; 37; 8; 24; 5; 2; 1; 8; 9; 3; 3; 2; 6; 1; 9; 3; 47; 5; 5; 15; 4; 65; 2; 20; 74; 4; 4; 8; 48; 2; 7; 0; 8; 65; 3; 72; 0; 9; 5; 5; 0; 4; 8; 5; 9; 48; 19; 8; 9; 4; 3; 75; 8; 8; 28; 9; 18; 9; 8; 8; 20; 2; 93; 6; 3; 2; 4; 1; 2; 0; 9; 85; 3; 6; 87; 6; 3; 23; 3; 3; 1; 5; 9; 7; 6; 4; 6; 51; 8; 6; 5; 5; 0; 3; 3; 3; 2; 44; 4; 84; 5; 2; 1; 6; 3; 3; 4; 1; 8; 6; 63; 6; 6; 95; 94; 5; 82; 4; 8; 30; 2; 6; 8; 0; 52; 8; 0; 3; 6; 8; 0; 9; 83; 4; 7; 9; 0; 64; 7; 5; 3; 2; 3; 8; 0; 3; 9; 73; 1; 0; 7; 46; 8; 4; 8; 2; 2; 68; 9; 92; 2; 6; 7; 1; 0; 2; 8; 3; 40; 9; 6; 3; 2; 0; 4; 6; 5; 3; 1; 3; 7; 7; 1; 95; 0; 5; 1; 6; 8; 75; 9; 52; 91; 4; 4; 7; 9; 6; 0; 3; 40; 14; 3; 5; 9; 6; 9; 7; 8; 2; 2; 2; 8; 2; 2; 29; 9; 5; 3; 7; 0; 4; 19; 21; 9; 2; 6; 8; 36; 12; 9; 1; 10; 4; 2; 8; 4; 9; 77; 2; 8; 0; 26; 4; 9; 9; 2; 0; 5; 7; 7; 3; 7; 5; 6; 9; 48; 70; 4; 85; 2; 5; 5; 3; 8; 6; 0; 1; 6; 9; 4; 5; 3; 2; 2; 68; 4; 5; 2; 2; 3; 83; 3; 13; 8; 6; 5; 1; 1; 0; 7; 59; 4; 6; 1; 9; 7; 3; 6; 1; 9; 7; 2; 0; 1; 28; 5; 3; 6; 5; 68; 6; 0; 9; 9; 33; 55; 28; 5; 2; 8; 42; 0; 22; 4; 6; 5; 98; 8; 6; 99; 9; 3; 69; 4; 99; 6; 3; 87; 9; 5; 7; 60; 8; 9; 9; 4; 7; 4; 1; 1; 6; 2; 5; 76; 0; 3; 3; 2; 2; 4; 5; 9; 2; 6; 1; 6; 52; 33; 88; 1; 0; 6; 8; 4; 2; 5; 58; 7; 9; 20; 5; 8; 5; 0; 7; 2; 2; 54; 87; 2; 5; 18; 2; 8; 12; 2; 1; 5; 61; 0; 4; 6; 4; 2; 2; 1; 35; 3; 0; 7; 26; 43; 14; 50; 23; 5; 0; 26; 14; 4; 2; 72; 2; 59; 5; 2; 48; 6; 7; 3; 12; 4; 7; 6; 2; 9; 2; 36; 8; 4; 2; 5; 7; 89; 72; 5; 5; 7; 4; 9; 34; 6; 40; 8; 2; 8; 1; 4; 1; 1; 0; 7; 0; 6; 54; 1; 5; 6; 3; 0; 8; 9; 24; 2; 7; 24; 5; 6; 65; 5; 6; 0; 9; 72; 7; 5; 8; 1; 5; 8; 5; 64; 4; 99; 35; 5; 54; 6; 95; 2; 8; 88; 8; 60; 1; 8; 26; 8; 43; 8; 8; 9; 4; 1; 4; 7; 0; 0; 5; 0; 26; 69; 9; 3; 3; 52; 75; 14; 5; 7; 8; 1; 3; 5; 3; 2; 23; 3; 7; 2; 4; 46; 7; 2; 23; 9; 4; 0; 5; 0; 9; 5; 4; 1; 7; 1; 4; 45; 3; 4; 11; 0; 8; 66; 67; 1; 1; 55; 7; 2; 0; 1; 1; 10; 7; 0; 1; 7; 4; 5; 2; 4; 2; 0; 9; 6; 5; 5; 4; 9; 7; 1; 9; 4; 7; 4; 20; 6; 60; 2; 7; 6; 8; 7; 97; 7; 4; 8; 1; 2; 7; 5; 7; 9; 2; 3; 20; 5; 9; 3; 63; 9; 8; 3; 88; 0; 1; 3; 95; 0; 9; 1; 6; 9; 43; 7; 5; 6; 1; 18; 9; 2; 7; 7; 5; 4; 9; 5; 8; 26; 65; 7; 1; 6; 5; 8; 0; 27; 8; 63; 85; 44; 7; 6; 51; 2; 3; 7; 5; 5; 8; 2; 7; 4; 8; 0; 7; 8; 31; 2; 92; 3; 7; 3; 8; 5; 5; 6; 0; 5; 4; 0; 4; 1; 1; 5; 7; 75; 6; 25; 4; 46; 0; 1; 8; 65; 68; 3; 7; 1; 7; 9; 6; 3; 2; 30; 4; 60; 48; 5; 1; 19; 4; 6; 5; 6; 0; 9; 0; 2; 94; 2; 83; 3; 2; 2; 2; 1; 8; 69; 5; 7; 5; 9; 4; 8; 92; 6; 2; 9; 9; 99; 7; 7; 3; 2; 46; 6; 8; 4; 84; 0; 8; 7; 1; 2; 2; 6; 6; 1; 3; 71; 8; 8; 31; 0; 7; 7; 5; 4; 80; 7; 3; 5; 9; 2; 6; 7; 3; 2; 8; 8; 2; 7; 59; 88; 40; 0; 4; 58; 1; 12; 0; 5; 85; 6; 0; 1; 9; 8; 3; 1; 79; 0; 8; 34; 69; 7; 91; 8; 2; 8; 6; 6; 3; 19; 2; 9; 57; 2; 1; 5; 0; 3; 7; 70; 3; 9; 9; 7; 2; 49; 3; 30; 18; 8; 99; 6; 2; 1; 2; 8; 8; 19; 67; 4; 5; 8; 4; 63; 49; 0; 5; 77; 7; 60; 93; 1; 29; 47; 32; 0; 0; 88; 3; 2; 6; 23; 2; 98; 5; 4; 4; 9; 9; 5; 1; 9; 2; 7; 4; 8; 8; 6; 2; 8; 9; 46; 72; 9; 9; 8; 3; 1; 3; 0; 3; 87; 13; 46; 6; 2; 5; 9; 4; 0; 7; 79; 8; 44; 4; 4; 33; 4; 2; 1; 4; 0; 1; 9; 7; 1; 6; 65; 4; 8; 0; 0; 1; 8; 2; 46; 35; 4; 6; 3; 7; 3; 5; 14; 3; 7; 33; 6; 89; 36; 39; 7; 4; 8; 1; 76; 1; 2; 4; 4; 6; 2; 0; 4; 2; 7; 5; 2; 47; 9; 8; 2; 5; 8; 87; 9; 3; 81; 1; 42; 8; 3; 6; 7; 1; 7; 0; 50; 2; 10; 8; 6; 5; 21; 1; 8; 5; 65; 2; 8; 0; 8; 4; 7; 66; 1; 1; 6; 9; 6; 1; 1; 9; 2; 18; 6; 42; 7; 60; 9; 3; 0; 9; 7; 4; 4; 94; 41; 4; 7; 3; 4; 8; 87; 9; 7; 2; 8; 2; 8; 0; 9; 28; 2; 9; 1; 41; 4; 8; 9; 6; 8; 81; 7; 3; 4; 1; 60; 6; 6; 0; 3; 87; 80; 0; 7; 67; 9; 64; 3; 74; 4; 6; 1; 0; 0; 3; 6; 2; 2; 7; 9; 2; 42; 1; 2; 98; 3; 2; 7; 86; 9; 48; 0; 4; 7; 6; 24; 70; 0; 70; 9; 0; 0; 4; 8; 3; 3; 3; 2; 25; 4; 2; 7; 4; 18; 94; 25; 5; 9; 9; 9; 4; 42; 0; 98; 4; 8; 8; 74; 6; 7; 7; 4; 9; 3; 2; 41; 2; 1; 6; 3; 95; 1; 1; 2; 1; 29; 24; 2; 88; 5; 8; 12; 7; 5; 2; 3; 3; 2; 7; 3; 23; 3; 8; 3; 0; 8; 9; 5; 2; 74; 6; 0; 0; 1; 6; 7; 2; 3; 61; 15; 8; 6; 4; 8; 73; 0; 95; 1; 83; 7; 49; 61; 8; 2; 7; 5; 61; 9; 87; 5; 99; 6; 3; 4; 2; 7; 85; 6; 91; 2; 2; 6; 9; 86; 2; 9; 64; 44; 2; 50; 3; 3; 3; 27; 1; 4; 4; 36; 5; 6; 8; 1; 6; 48; 1; 43; 6; 75; 1; 1; 2; 2; 1; 9; 1; 87; 34; 3; 92; 58; 4; 8; 1; 9; 4; 5; 8; 1; 9; 56; 5; 7; 3; 9; 7; 50; 1; 0; 70; 1; 2; 99; 28; 0; 7; 4; 3; 3; 9; 77; 88; 4; 4; 41; 1; 90; 4; 9; 4; 5; 5; 5; 0; 7; 8; 45; 44; 1; 38; 3; 85; 74; 2; 1; 78; 55; 3; 1; 4; 9; 5; 8; 1; 5; 7; 0; 8; 6; 6; 5; 3; 7; 9; 87; 4; 8; 3; 9; 8; 7; 4; 5; 5; 0; 9; 7; 0; 23; 9; 26; 7; 4; 61; 2; 0; 8; 52; 7; 4; 3; 7; 4; 88; 0; 7; 8; 15; 7; 5; 0; 7; 0; 5; 6; 4; 0; 7; 51; 3; 7; 54; 40; 6; 0; 33; 9; 7; 9; 7; 19; 0; 23; 4; 2; 8; 9; 7; 1; 3; 0; 72; 1; 42; 2; 5; 7; 4; 7; 76; 74; 0; 9; 6; 5; 1; 5; 6; 98; 0; 3; 5; 4; 7; 7; 26; 7; 3; 6; 50; 4; 7; 0; 4; 6; 38; 6; 2; 1; 2; 0; 1; 5; 3; 10; 0; 1; 6; 73; 4; 5; 2; 2; 5; 9; 3; 0; 0; 4; 7; 1; 9; 1; 3; 2; 8; 0; 7; 6; 7; 3; 3; 3; 2; 9; 7; 81; 5; 3; 0; 9; 0; 3; 4; 8; 0; 2; 0; 9; 8; 0; 9; 6; 6; 41; 70; 4; 9; 6; 30; 2; 5; 2; 0; 6; 74; 4; 76; 0; 8; 5; 5; 7; 1; 67; 4; 5; 4; 6; 0; 7; 23; 4; 40; 4; 17; 3; 0; 2; 5; 7; 7; 8; 56; 3; 10; 6; 7; 71; 66; 0; 76; 3; 7; 0; 8; 4; 8; 94; 9; 74; 7; 1; 2; 2; 73; 7; 7; 6; 4; 7; 4; 6; 3; 3; 5; 81; 2; 0; 6; 0; 3; 9; 10; 9; 6; 4; 0; 41; 1; 5; 8; 2; 7; 1; 3; 9; 9; 49; 6; 8; 54; 9; 9; 4; 5; 55; 76; 6; 87; 8; 4; 8; 2; 93; 53; 0; 1; 4; 4; 8; 5; 3; 73; 8; 76; 4; 80; 1; 3; 63; 95; 6; 2; 4; 1; 3; 6; 7; 4; 7; 7; 88; 4; 5; 4; 9; 3; 8; 7; 1; 1; 7; 35; 7; 3; 5; 8; 7; 6; 2; 9; 8; 1; 9; 8; 8; 1; 2; 20; 41; 2; 2; 3; 7; 6; 41; 0; 42; 9; 2; 27; 9; 6; 7; 8; 4; 65; 1; 8; 0; 3; 5; 8; 34; 6; 65; 7; 4; 1; 52; 60; 2; 72; 8; 5; 1; 5; 8; 80; 20; 4; 3; 1; 5; 0; 7; 1; 6; 4; 0; 0; 82; 1; 9; 8; 8; 2; 0; 31; 8; 3; 8; 2; 2; 11; 6; 2; 3; 9; 50; 40; 4; 5; 6; 0; 2; 5; 2; 2; 8; 5; 7; 4; 46; 9; 6; 2; 0; 15; 0; 45; 3; 9; 5; 8; 7; 4; 9; 11; 6; 5; 8; 6; 2; 5; 5; 6; 8; 8; 1; 24; 60; 0; 8; 66; 8; 4; 4; 0; 7; 4; 5; 5; 5; 6; 8; 23; 1; 46; 3; 3; 7; 3; 8; 3; 8; 6; 2; 39; 28; 1; 1; 9; 68; 6; 3; 90; 8; 8; 14; 2; 4; 1; 2; 74; 3; 3; 6; 80; 9; 7; 7; 7; 3; 7; 27; 38; 69; 61; 7; 0; 72; 4; 8; 3; 23; 6; 0; 3; 1; 0; 66; 7; 4; 2; 1; 36; 13; 9; 7; 2; 35; 3; 86; 1; 7; 1; 9; 0; 88; 9; 0; 6; 48; 4; 1; 1; 3; 8; 5; 0; 6; 9; 6; 97; 4; 32; 79; 40; 6; 5; 0; 31; 91; 1; 9; 0; 4; 65; 9; 43; 0; 9; 42; 2; 8; 62; 3; 9; 64; 3; 0; 9; 11; 4; 8; 7; 7; 1; 52; 3; 11; 1; 3; 5; 26; 7; 90; 9; 7; 6; 2; 7; 84; 0; 67; 6; 5; 6; 0; 4; 4; 2; 3; 8; 4; 4; 4; 4; 2; 3; 2; 7; 0; 0; 36; 6; 8; 9; 5; 8; 30; 2; 84; 4; 4; 9; 1; 6; 6; 42; 7; 6; 0; 77; 6; 4; 4; 6; 19; 53; 9; 2; 8; 8; 9; 3; 8; 6; 8; 3; 5; 4; 1; 7; 11; 0; 1; 1; 4; 2; 4; 8; 13; 0; 5; 4; 5; 6; 0; 99; 9; 2; 96; 8; 6; 2; 1; 8; 5; 1; 71; 6; 17; 5; 2; 9; 58; 3; 99; 5; 10; 0; 6; 7; 5; 45; 4; 2; 9; 0; 32; 0; 0; 67; 1; 6; 47; 9; 9; 0; 48; 5; 5; 9; 9; 6; 47; 0; 9; 4; 0; 9; 5; 0; 1; 88; 8; 98; 8; 49; 7; 6; 3; 2; 0; 3; 13; 0; 1; 7; 7; 9; 1; 3; 2; 5; 0; 73; 5; 6; 5; 4; 20; 7; 6; 46; 6; 4; 0; 8; 80; 33; 7; 8; 8; 9; 2; 36; 4; 95; 8; 2; 53; 2; 6; 7; 8; 9; 0; 5; 24; 1; 9; 8; 0; 0; 0; 34; 23; 65; 4; 15; 9; 7; 18; 8; 5; 3; 1; 7; 88; 8; 9; 0; 0; 6; 5; 8; 6; 39; 86; 1; 4; 7; 7; 3; 43; 53; 3; 1; 7; 8; 7; 5; 51; 58; 38; 23; 2; 1; 9; 6; 6; 4; 4; 3; 8; 0; 0; 0; 2; 7; 57; 9; 7; 2; 60; 7; 9; 9; 93; 6; 9; 4; 6; 0; 3; 4; 10; 3; 5; 28; 6; 50; 4; 3; 2; 3; 8; 7; 0; 3; 0; 6; 74; 0; 4; 70; 59; 1; 5; 2; 10; 6; 56; 97; 5; 68; 8; 28; 6; 4; 8; 8; 1; 2; 6; 9; 6; 9; 96; 61; 5; 7; 8; 8; 5; 1; 4; 5; 9; 81; 7; 0; 9; 7; 3; 9; 9; 27; 2; 72; 4; 84; 39; 7; 43; 4; 5; 1; 57; 7; 9; 8; 7; 11; 0; 6; 5; 18; 2; 2; 1; 4; 91; 1; 92; 1; 1; 9; 8; 1; 56; 9; 7; 50; 7; 95; 27; 2; 2; 0; 95; 3; 87; 5; 8; 9; 4; 2; 6; 6; 9; 3; 3; 0; 8; 6; 4; 9; 2; 8; 2; 1; 7; 3; 95; 35; 2; 8; 23; 4; 8; 87; 8; 0; 72; 8; 1; 8; 2; 6; 9; 18; 8; 0; 2; 1; 9; 44; 4; 7; 9; 96; 2; 2; 50; 3; 5; 2; 4; 0; 6; 1; 1; 5; 3; 6; 5; 17; 3; 9; 4; 1; 2; 6; 9; 0; 0; 95; 5; 0; 38; 29; 5; 7; 7; 5; 4; 8; 65; 1; 47; 2; 8; 4; 3; 0; 9; 36; 8; 7; 0; 86; 
8000
3; 37; 38; 12; 2; 1; 4; 2; 90; 4; 2; 95; 7; 7; 65; 8; 9; 3; 3; 4; 89; 0; 0; 6; 54; 58; 3; 7; 0; 5; 9; 36; 1; 9; 7; 0; 4; 0; 3; 8; 9; 44; 0; 7; 6; 0; 6; 7; 0; 50; 1; 9; 6; 5; 2; 1; 30; 4; 3; 8; 9; 6; 75; 0; 9; 4; 9; 7; 20; 9; 1; 7; 11; 40; 3; 8; 2; 9; 1; 3; 8; 0; 5; 1; 9; 8; 1; 1; 0; 9; 2; 23; 89; 40; 2; 0; 7; 5; 9; 5; 12; 5; 0; 32; 8; 8; 0; 2; 8; 0; 9; 6; 29; 0; 9; 96; 1; 5; 2; 4; 0; 7; 7; 8; 8; 3; 0; 43; 2; 80; 0; 6; 74; 9; 7; 9; 0; 8; 8; 5; 1; 8; 5; 9; 11; 2; 5; 2; 40; 4; 2; 91; 6; 69; 4; 0; 3; 15; 6; 5; 5; 6; 0; 59; 6; 4; 6; 7; 3; 8; 5; 9; 2; 7; 5; 7; 5; 4; 70; 9; 8; 8; 0; 41; 6; 2; 74; 5; 9; 4; 6; 3; 3; 6; 8; 6; 6; 9; 4; 1; 6; 6; 26; 6; 2; 8; 0; 1; 4; 0; 2; 4; 6; 1; 50; 6; 12; 0; 3; 7; 55; 6; 73; 5; 9; 4; 2; 3; 0; 72; 1; 5; 16; 3; 99; 9; 39; 7; 6; 7; 1; 0; 77; 8; 7; 61; 1; 5; 9; 6; 5; 4; 76; 5; 11; 4; 7; 5; 8; 49; 8; 84; 7; 7; 3; 6; 3; 6; 94; 5; 0; 73; 3; 4; 3; 0; 0; 2; 7; 51; 4; 2; 9; 73; 2; 0; 1; 35; 97; 3; 5; 35; 8; 1; 3; 3; 92; 6; 7; 1; 3; 4; 8; 8; 7; 5; 10; 5; 9; 5; 5; 13; 1; 7; 9; 4; 4; 0; 6; 8; 2; 6; 2; 4; 4; 2; 0; 12; 2; 77; 8; 3; 3; 8; 6; 8; 2; 44; 9; 7; 8; 7; 8; 89; 2; 8; 2; 70; 1; 7; 3; 9; 43; 89; 60; 85; 56; 1; 7; 6; 5; 57; 2; 6; 1; 26; 1; 5; 0; 1; 4; 29; 97; 6; 8; 97; 7; 41; 41; 0; 1; 72; 43; 8; 4; 2; 2; 8; 54; 0; 40; 35; 7; 6; 6; 0; 74; 0; 7; 4; 4; 1; 73; 9; 93; 26; 6; 8; 6; 8; 3; 9; 18; 63; 19; 63; 0; 41; 6; 13; 0; 33; 8; 6; 6; 1; 74; 51; 4; 9; 78; 7; 5; 19; 1; 6; 9; 5; 3; 21; 3; 9; 4; 2; 3; 19; 3; 75; 74; 3; 16; 7; 1; 6; 1; 1; 7; 50; 1; 7; 9; 1; 97; 9; 96; 1; 87; 6; 79; 93; 7; 3; 52; 4; 4; 8; 4; 4; 7; 1; 2; 4; 28; 7; 6; 1; 78; 6; 8; 14; 2; 2; 6; 7; 32; 5; 20; 8; 68; 0; 76; 23; 6; 25; 65; 1; 0; 7; 25; 1; 1; 2; 3; 44; 6; 1; 6; 18; 1; 2; 1; 37; 9; 0; 7; 4; 9; 5; 0; 87; 2; 2; 8; 35; 46; 1; 5; 5; 82; 8; 9; 5; 7; 3; 4; 62; 7; 2; 5; 5; 8; 1; 19; 0; 7; 7; 3; 8; 4; 8; 1; 8; 15; 62; 8; 7; 8; 5; 3; 4; 3; 7; 2; 36; 4; 8; 8; 0; 9; 6; 6; 42; 3; 8; 5; 80; 3; 2; 9; 7; 7; 8; 0; 1; 55; 8; 2; 7; 4; 7; 91; 88; 19; 7; 5; 9; 0; 2; 23; 97; 1; 2; 5; 9; 7; 5; 3; 3; 0; 4; 36; 3; 82; 41; 65; 4; 2; 6; 3; 9; 2; 2; 1; 0; 2; 48; 4; 0; 66; 49; 6; 13; 3; 39; 7; 9; 4; 8; 4; 1; 9; 4; 8; 2; 4; 58; 0; 5; 64; 8; 8; 4; 4; 11; 9; 6; 0; 8; 8; 0; 7; 9; 9; 2; 4; 0; 9; 5; 0; 0; 6; 1; 2; 8; 0; 7; 8; 0; 6; 4; 2; 14; 97; 1; 14; 2; 3; 1; 9; 97; 6; 3; 1; 4; 7; 2; 8; 29; 78; 67; 5; 8; 4; 9; 2; 8; 3; 6; 6; 2; 1; 5; 2; 7; 1; 8; 4; 7; 5; 1; 3; 65; 0; 0; 33; 8; 2; 72; 7; 70; 7; 1; 1; 3; 9; 4; 9; 5; 1; 2; 4; 7; 4; 64; 9; 5; 5; 9; 9; 62; 7; 10; 47; 3; 0; 9; 7; 50; 7; 8; 10; 2; 40; 4; 6; 3; 12; 4; 3; 4; 0; 37; 1; 54; 8; 8; 2; 6; 2; 6; 7; 9; 1; 75; 8; 8; 5; 4; 13; 2; 9; 2; 94; 5; 8; 83; 3; 0; 5; 7; 2; 3; 4; 0; 24; 23; 1; 4; 6; 7; 30; 9; 3; 0; 63; 8; 24; 5; 8; 7; 64; 50; 95; 82; 7; 7; 5; 4; 4; 9; 5; 7; 5; 3; 4; 60; 0; 9; 47; 4; 6; 0; 52; 7; 2; 0; 3; 0; 0; 13; 5; 8; 2; 2; 3; 0; 5; 4; 5; 0; 0; 7; 7; 8; 0; 5; 6; 1; 5; 49; 8; 5; 88; 88; 3; 9; 7; 2; 2; 4; 8; 6; 5; 5; 8; 79; 0; 9; 26; 6; 8; 79; 2; 1; 4; 7; 6; 98; 2; 2; 9; 4; 2; 10; 6; 0; 56; 8; 84; 4; 2; 4; 2; 7; 67; 4; 9; 2; 2; 54; 8; 0; 4; 6; 3; 30; 61; 4; 7; 44; 7; 5; 1; 9; 6; 5; 2; 69; 4; 60; 8; 0; 8; 1; 2; 5; 12; 5; 6; 8; 5; 2; 5; 2; 89; 5; 50; 2; 0; 1; 4; 6; 6; 4; 2; 0; 2; 6; 0; 9; 8; 5; 4; 4; 8; 3; 6; 4; 0; 75; 6; 0; 0; 10; 8; 64; 90; 36; 4; 6; 16; 3; 4; 3; 2; 4; 7; 90; 3; 86; 0; 5; 0; 0; 1; 0; 9; 3; 7; 4; 2; 1; 5; 6; 7; 42; 7; 2; 7; 2; 0; 7; 5; 7; 8; 6; 85; 4; 0; 4; 2; 1; 2; 69; 12; 76; 9; 26; 1; 8; 1; 6; 0; 53; 5; 3; 7; 6; 3; 69; 8; 38; 9; 2; 75; 1; 5; 8; 2; 8; 7; 2; 3; 5; 0; 1; 1; 81; 9; 0; 9; 2; 9; 6; 8; 9; 5; 31; 8; 57; 0; 3; 2; 34; 3; 4; 7; 6; 5; 0; 4; 9; 29; 3; 5; 8; 6; 2; 47; 75; 5; 1; 0; 8; 3; 6; 8; 4; 1; 4; 0; 84; 7; 2; 83; 14; 34; 2; 0; 75; 42; 7; 6; 5; 44; 59; 0; 5; 6; 1; 19; 5; 1; 4; 7; 5; 1; 2; 29; 2; 8; 0; 2; 91; 7; 14; 14; 0; 40; 37; 3; 2; 2; 2; 6; 56; 25; 3; 6; 8; 8; 4; 3; 9; 56; 8; 8; 5; 46; 5; 2; 8; 5; 3; 21; 9; 1; 3; 63; 7; 4; 1; 5; 7; 0; 2; 0; 7; 41; 8; 5; 3; 53; 5; 2; 4; 0; 0; 5; 82; 0; 2; 63; 1; 0; 52; 11; 3; 1; 7; 3; 5; 57; 3; 8; 14; 6; 22; 9; 84; 6; 59; 1; 5; 0; 25; 8; 22; 2; 6; 25; 2; 6; 9; 79; 9; 7; 56; 1; 30; 94; 7; 1; 30; 6; 8; 9; 52; 86; 9; 2; 1; 4; 8; 8; 7; 3; 9; 8; 1; 46; 8; 6; 2; 9; 1; 0; 95; 46; 21; 7; 2; 11; 9; 1; 4; 8; 0; 7; 0; 6; 2; 8; 67; 45; 5; 9; 71; 2; 8; 7; 82; 7; 4; 93; 5; 8; 4; 9; 0; 7; 8; 5; 13; 9; 8; 5; 0; 5; 3; 0; 40; 6; 9; 5; 85; 8; 9; 41; 4; 67; 0; 1; 8; 9; 8; 4; 23; 18; 7; 88; 4; 6; 45; 86; 0; 3; 51; 0; 3; 2; 5; 27; 2; 65; 4; 3; 3; 2; 6; 84; 19; 5; 7; 5; 44; 2; 61; 0; 2; 14; 7; 57; 57; 20; 51; 15; 7; 2; 4; 9; 3; 2; 7; 43; 8; 8; 3; 9; 9; 24; 1; 1; 7; 8; 6; 88; 3; 9; 9; 0; 49; 31; 2; 5; 42; 8; 7; 39; 9; 0; 31; 8; 9; 1; 7; 3; 8; 4; 3; 63; 9; 9; 8; 89; 2; 54; 2; 1; 4; 3; 67; 0; 2; 7; 5; 7; 82; 4; 8; 1; 2; 77; 7; 76; 12; 3; 7; 36; 5; 9; 6; 9; 15; 2; 8; 27; 63; 3; 2; 8; 3; 22; 3; 2; 98; 3; 1; 7; 7; 0; 5; 6; 8; 7; 1; 2; 8; 5; 5; 18; 30; 4; 7; 49; 40; 2; 56; 7; 1; 9; 7; 9; 7; 3; 52; 4; 9; 61; 1; 79; 3; 8; 44; 5; 2; 5; 90; 43; 9; 4; 4; 0; 3; 8; 4; 18; 0; 6; 4; 3; 59; 5; 49; 5; 49; 8; 5; 8; 4; 5; 5; 7; 1; 4; 9; 5; 9; 7; 6; 2; 22; 7; 13; 3; 9; 8; 5; 34; 9; 3; 1; 8; 0; 1; 2; 6; 2; 25; 7; 6; 11; 2; 74; 4; 9; 3; 6; 4; 3; 1; 1; 8; 5; 5; 7; 1; 84; 25; 7; 7; 2; 6; 8; 1; 8; 71; 5; 1; 1; 9; 81; 63; 7; 4; 5; 1; 8; 40; 4; 6; 8; 1; 0; 4; 5; 7; 1; 9; 4; 9; 13; 6; 9; 2; 9; 0; 9; 0; 3; 8; 4; 0; 7; 1; 8; 5; 94; 4; 1; 1; 0; 7; 9; 5; 5; 7; 9; 9; 7; 1; 2; 2; 7; 0; 9; 78; 4; 3; 87; 4; 89; 1; 66; 4; 71; 7; 98; 96; 0; 1; 91; 2; 5; 89; 3; 1; 1; 3; 13; 7; 6; 0; 0; 0; 5; 8; 46; 9; 39; 8; 8; 9; 2; 30; 2; 8; 8; 4; 7; 4; 2; 4; 78; 51; 6; 9; 0; 6; 34; 4; 0; 1; 3; 72; 4; 40; 0; 9; 5; 1; 5; 7; 0; 5; 1; 5; 78; 31; 1; 7; 7; 9; 8; 7; 3; 1; 3; 2; 4; 5; 7; 3; 6; 9; 73; 41; 1; 3; 88; 5; 5; 1; 5; 2; 6; 43; 1; 2; 2; 72; 7; 3; 39; 7; 9; 28; 0; 0; 8; 77; 0; 4; 1; 66; 8; 3; 27; 2; 44; 7; 8; 4; 7; 9; 7; 6; 5; 9; 9; 4; 9; 39; 2; 7; 9; 6; 9; 7; 8; 44; 44; 9; 7; 3; 5; 3; 7; 9; 8; 0; 6; 0; 0; 9; 0; 3; 7; 6; 11; 5; 0; 4; 1; 0; 2; 9; 3; 4; 2; 1; 2; 68; 1; 62; 9; 9; 7; 8; 7; 41; 7; 6; 3; 3; 7; 0; 8; 73; 14; 2; 8; 64; 9; 9; 5; 2; 0; 2; 65; 4; 46; 3; 5; 0; 22; 3; 4; 24; 0; 1; 2; 3; 8; 61; 0; 0; 4; 6; 8; 2; 5; 17; 48; 3; 3; 4; 7; 4; 6; 22; 0; 8; 5; 3; 5; 4; 0; 0; 3; 3; 4; 3; 5; 3; 6; 7; 0; 8; 1; 6; 38; 6; 8; 5; 47; 7; 71; 3; 9; 31; 56; 8; 52; 1; 1; 6; 9; 7; 2; 8; 8; 1; 67; 4; 5; 1; 0; 9; 7; 6; 98; 6; 80; 3; 5; 20; 7; 73; 7; 0; 5; 1; 2; 8; 0; 8; 5; 4; 3; 34; 9; 1; 3; 74; 1; 63; 61; 3; 7; 7; 3; 4; 1; 1; 3; 2; 4; 6; 2; 3; 3; 3; 2; 3; 8; 4; 3; 7; 5; 6; 30; 13; 27; 65; 3; 5; 5; 8; 9; 8; 8; 72; 8; 0; 61; 6; 4; 8; 8; 5; 0; 1; 2; 13; 98; 10; 7; 7; 7; 8; 9; 2; 2; 5; 6; 43; 17; 3; 3; 5; 4; 0; 8; 2; 74; 5; 8; 3; 95; 5; 7; 70; 6; 1; 3; 6; 9; 89; 20; 86; 1; 9; 5; 1; 53; 94; 8; 83; 52; 6; 3; 7; 7; 3; 61; 9; 8; 8; 3; 1; 6; 0; 90; 30; 27; 9; 9; 8; 5; 45; 6; 1; 19; 5; 35; 4; 6; 6; 0; 6; 7; 8; 1; 17; 3; 5; 8; 8; 1; 12; 89; 78; 6; 1; 2; 8; 7; 15; 7; 99; 4; 1; 3; 44; 9; 79; 6; 0; 67; 47; 0; 2; 8; 4; 6; 2; 4; 4; 81; 16; 5; 5; 4; 7; 8; 1; 2; 6; 3; 0; 7; 2; 1; 5; 3; 1; 1; 9; 72; 1; 2; 9; 99; 9; 2; 1; 7; 6; 1; 43; 7; 2; 55; 6; 7; 2; 4; 4; 4; 8; 53; 51; 7; 1; 31; 50; 9; 0; 5; 7; 7; 5; 9; 8; 8; 7; 7; 8; 1; 5; 3; 3; 5; 0; 5; 88; 9; 2; 8; 2; 5; 7; 6; 1; 7; 3; 88; 0; 4; 9; 18; 5; 8; 6; 2; 4; 4; 3; 2; 3; 2; 7; 66; 90; 6; 32; 55; 1; 3; 8; 57; 60; 17; 1; 48; 1; 7; 7; 0; 0; 0; 1; 2; 93; 7; 7; 56; 5; 78; 9; 2; 76; 0; 4; 5; 92; 9; 42; 5; 4; 3; 7; 8; 90; 1; 4; 6; 1; 2; 87; 5; 8; 7; 0; 9; 6; 1; 35; 3; 9; 9; 12; 6; 6; 9; 64; 39; 6; 5; 7; 5; 8; 5; 82; 50; 6; 39; 43; 63; 8; 8; 11; 0; 7; 7; 91; 24; 4; 2; 0; 2; 2; 5; 6; 1; 2; 82; 89; 26; 0; 9; 8; 6; 2; 2; 6; 0; 7; 4; 9; 44; 3; 24; 39; 2; 4; 9; 9; 7; 70; 0; 4; 24; 0; 32; 3; 94; 8; 0; 8; 8; 33; 6; 39; 9; 9; 1; 0; 4; 6; 81; 33; 1; 3; 4; 42; 57; 2; 0; 6; 7; 0; 2; 51; 52; 8; 99; 6; 59; 0; 64; 2; 32; 4; 2; 7; 5; 1; 9; 7; 4; 9; 3; 9; 2; 74; 2; 7; 90; 1; 0; 19; 8; 8; 5; 2; 9; 0; 6; 4; 82; 9; 1; 9; 2; 24; 6; 98; 5; 9; 2; 8; 9; 9; 73; 0; 38; 0; 7; 1; 3; 8; 7; 3; 0; 32; 4; 0; 0; 5; 6; 8; 3; 9; 9; 3; 3; 7; 0; 4; 7; 0; 87; 8; 21; 7; 5; 72; 5; 0; 6; 36; 81; 0; 64; 6; 6; 29; 1; 8; 6; 38; 57; 62; 2; 0; 2; 3; 7; 8; 7; 1; 2; 3; 3; 8; 1; 0; 6; 7; 7; 49; 2; 42; 20; 98; 8; 9; 13; 9; 8; 6; 8; 4; 8; 6; 61; 6; 3; 1; 0; 0; 2; 4; 0; 1; 5; 9; 1; 62; 5; 0; 7; 6; 3; 4; 4; 0; 8; 1; 8; 98; 57; 2; 72; 3; 0; 0; 5; 4; 5; 9; 3; 9; 88; 8; 59; 9; 3; 5; 8; 4; 94; 44; 9; 6; 0; 3; 81; 34; 81; 7; 8; 85; 12; 7; 3; 65; 1; 4; 8; 8; 15; 5; 5; 5; 78; 6; 0; 4; 4; 5; 4; 5; 2; 3; 3; 1; 3; 0; 1; 0; 2; 0; 3; 5; 0; 0; 4; 1; 5; 3; 9; 2; 48; 6; 9; 46; 9; 4; 69; 55; 32; 47; 21; 9; 4; 94; 2; 68; 3; 0; 0; 9; 2; 8; 3; 7; 7; 3; 9; 5; 4; 61; 3; 3; 69; 97; 97; 5; 2; 3; 42; 6; 2; 77; 4; 1; 7; 8; 8; 7; 36; 1; 9; 7; 3; 1; 7; 4; 87; 64; 2; 8; 96; 96; 8; 88; 7; 27; 0; 0; 0; 7; 63; 8; 3; 0; 2; 5; 8; 66; 8; 99; 1; 54; 55; 8; 9; 6; 9; 11; 5; 9; 6; 4; 1; 7; 5; 6; 9; 37; 67; 5; 2; 7; 0; 0; 3; 0; 1; 3; 1; 21; 16; 5; 6; 9; 24; 7; 4; 2; 6; 4; 7; 6; 9; 3; 1; 6; 18; 74; 0; 7; 1; 3; 9; 1; 1; 6; 2; 9; 6; 1; 95; 9; 7; 4; 0; 3; 67; 0; 2; 6; 4; 5; 8; 6; 0; 2; 4; 39; 5; 7; 2; 7; 78; 40; 77; 8; 7; 55; 5; 53; 6; 0; 18; 71; 2; 8; 48; 90; 4; 4; 71; 38; 6; 3; 1; 3; 14; 9; 6; 0; 2; 5; 7; 74; 8; 1; 8; 7; 8; 3; 3; 6; 1; 9; 71; 3; 6; 9; 1; 57; 9; 8; 4; 6; 9; 4; 8; 2; 66; 2; 7; 55; 3; 5; 8; 2; 7; 0; 4; 5; 37; 4; 2; 3; 25; 1; 0; 8; 93; 3; 5; 4; 2; 7; 3; 0; 7; 3; 5; 4; 45; 8; 1; 5; 6; 6; 29; 4; 5; 8; 5; 9; 7; 8; 9; 6; 4; 88; 9; 0; 1; 15; 43; 5; 3; 8; 9; 7; 9; 67; 7; 9; 2; 1; 5; 97; 79; 9; 0; 7; 1; 2; 7; 6; 6; 30; 7; 1; 11; 0; 5; 3; 54; 56; 1; 8; 0; 3; 8; 0; 3; 7; 8; 5; 9; 0; 64; 56; 6; 9; 55; 2; 2; 3; 0; 6; 86; 3; 7; 0; 0; 8; 7; 42; 2; 38; 34; 4; 1; 5; 2; 68; 23; 83; 2; 55; 6; 7; 1; 99; 2; 7; 1; 4; 7; 55; 4; 72; 0; 8; 96; 80; 4; 9; 9; 9; 3; 4; 5; 50; 6; 8; 2; 4; 8; 3; 32; 6; 3; 0; 61; 5; 8; 0; 0; 4; 1; 0; 7; 2; 0; 5; 54; 3; 5; 9; 8; 35; 3; 5; 68; 31; 31; 68; 0; 0; 4; 0; 0; 99; 9; 8; 7; 20; 5; 2; 1; 26; 90; 6; 4; 0; 1; 7; 9; 9; 3; 4; 2; 2; 9; 6; 9; 5; 8; 9; 6; 4; 3; 6; 2; 8; 5; 9; 5; 8; 4; 6; 7; 6; 4; 3; 1; 3; 80; 10; 6; 35; 6; 5; 24; 0; 71; 4; 47; 0; 8; 9; 0; 74; 90; 6; 3; 11; 9; 5; 6; 4; 1; 8; 21; 3; 5; 8; 1; 3; 9; 2; 6; 2; 8; 53; 7; 3; 9; 90; 39; 3; 77; 5; 4; 7; 7; 0; 39; 0; 6; 0; 1; 4; 0; 7; 9; 2; 1; 3; 2; 3; 1; 6; 3; 49; 5; 9; 6; 2; 10; 3; 0; 6; 91; 4; 7; 8; 3; 2; 5; 9; 6; 41; 2; 7; 7; 0; 7; 2; 6; 6; 9; 3; 4; 9; 2; 5; 6; 2; 6; 1; 9; 9; 4; 2; 5; 0; 0; 0; 0; 4; 2; 6; 0; 9; 7; 6; 5; 76; 3; 1; 5; 6; 69; 5; 4; 0; 16; 5; 72; 34; 0; 0; 3; 6; 20; 8; 1; 2; 2; 4; 9; 8; 5; 3; 65; 3; 7; 0; 2; 4; 7; 8; 4; 7; 74; 0; 5; 42; 3; 9; 99; 4; 2; 3; 3; 7; 32; 9; 35; 66; 2; 75; 3; 4; 19; 76; 5; 9; 4; 4; 7; 5; 0; 9; 94; 6; 1; 96; 8; 1; 95; 0; 40; 8; 8; 8; 0; 6; 7; 3; 9; 5; 76; 6; 98; 88; 4; 3; 91; 0; 4; 3; 3; 8; 5; 5; 0; 63; 0; 53; 8; 6; 0; 7; 2; 4; 1; 6; 6; 0; 8; 6; 4; 51; 9; 31; 8; 6; 6; 9; 0; 6; 5; 23; 9; 29; 8; 52; 5; 85; 0; 0; 6; 88; 9; 4; 0; 2; 4; 75; 66; 97; 33; 3; 1; 9; 7; 5; 6; 9; 56; 8; 5; 7; 93; 0; 6; 9; 6; 5; 1; 2; 9; 4; 13; 9; 0; 7; 3; 97; 7; 6; 4; 7; 38; 2; 40; 5; 36; 62; 3; 1; 1; 8; 65; 5; 3; 8; 59; 1; 3; 1; 4; 2; 7; 4; 43; 6; 8; 73; 8; 27; 39; 6; 5; 8; 52; 3; 0; 1; 1; 6; 47; 0; 8; 54; 90; 1; 45; 8; 5; 5; 91; 7; 8; 3; 0; 2; 0; 2; 5; 4; 5; 5; 9; 8; 0; 65; 37; 5; 7; 9; 4; 45; 4; 83; 5; 2; 9; 1; 9; 49; 4; 7; 4; 8; 6; 0; 2; 5; 1; 2; 5; 3; 15; 1; 3; 4; 87; 2; 3; 94; 2; 5; 1; 43; 4; 43; 9; 0; 3; 7; 0; 9; 1; 9; 0; 4; 7; 0; 1; 3; 0; 91; 6; 9; 80; 9; 69; 82; 2; 30; 7; 4; 2; 5; 33; 3; 9; 4; 5; 40; 3; 9; 5; 6; 3; 1; 3; 5; 5; 1; 0; 76; 7; 8; 9; 8; 1; 44; 0; 8; 0; 2; 9; 0; 9; 30; 0; 9; 6; 2; 7; 18; 9; 6; 1; 9; 9; 72; 7; 96; 15; 2; 24; 8; 41; 2; 5; 9; 97; 4; 2; 5; 3; 79; 1; 9; 3; 4; 39; 4; 2; 1; 5; 2; 5; 7; 3; 9; 4; 7; 5; 4; 9; 2; 5; 2; 6; 4; 13; 7; 0; 7; 23; 0; 36; 59; 4; 46; 28; 7; 5; 8; 9; 2; 3; 3; 8; 8; 1; 84; 1; 3; 43; 8; 31; 4; 9; 7; 7; 89; 3; 6; 8; 0; 5>

This makes sense as sequences are generated based on QCheck.list, which uses QCheck.gen.nat for length generation underneath the hood, and that can produce up to size 10.000.

One option is of course to generate shorter sequences. I've experimented with adding a combinator Lin.seq_small for doing so.

Alternatively, one could spend less time shrinking.
I've thus experimented with using just QCheck.Shrink.list_spine instead. Interestingly, this

  • completes quickly, yet
  • may produce counterexamples with 1 - or 2 - long sequences, as different non-det runs may take different shrinking routes, even on the same seed.

This suggests that element shrinking causes enough reruns to help reduce the spine even further - indicating that their combination has a hand in both (a) size reduction and (b) long shrink times.

As another experiment I experimented with adjusting retries:
Turning it up to 4/5/6 (meaning 200/250/300 repetitions) resulted in shorter counter examples but longer shrinking time.

In retrospect, I think this is natural for this to show up now with the recent merge of #463 - and with not a lot of other Lin tests using the seq combinator for input generation...

@jmid jmid mentioned this issue Jan 15, 2025
Merged
@jmid jmid closed this as completed in #517 Jan 15, 2025
@jmid jmid mentioned this issue Jan 16, 2025
Closed
@jmid jmid mentioned this issue May 5, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
test suite reliability Issue concerns tests that should behave more predictably
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Lin Dynarray tweaks + add Lin.{seq_small, array_small, list_small} ocaml-multicore/multicoretests
1 participant
@jmid
0