Tool 2LS 0.5.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]]
Run set sv-comp17.ReachSafety-ProductLines
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/product-lines/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
elevator_spec14_product20_false-unreach-call_true-termination.cil.c 1 5.7  5.7  63    1200 .0041 0     12   6.5 170 510 13   6.7 240 500
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 1 9.6  9.6  110    1900 .0041 0     14   7.6 240 530 12   6.7 240 500
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 1 6.2  6.2  57    1200 .0041 0     11   5.9 240 470 18   9.3 220 510
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 1 10    10    93    2000 .0041 0     12   6.3 220 500 13   6.9 220 510
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 1 34    34    400    6700 .0041 0     13   6.8 86 510 12   6.5 190 440
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 0 38    38    420    800 .0041 0     14   7.5 250 660 11   5.8 160 410
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 0 35    35    350    840 .0041 .27  17   8.7 260 760 15   7.8 140 430
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 0 43    43    440    1100 .0041 0     14   7.6 300 720 12   6.3 220 420
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 0 46    46    410    1200 .0041 0     17   9.1 360 890 11   6.0 150 420
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 0 37    37    360    830 .0041 0     13   7.0 160 680 11   6.0 210 400
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 0 37    37    510    890 .0041 0     16   8.5 120 780 12   6.4 180 430
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 0 41    41    490    1200 .0041 0     14   7.3 130 730 12   6.7 270 430
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 0 46    46    470    1200 .0041 0     16   8.4 140 880 11   6.1 150 420
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 110    110    1000    3600 .0041 0     16   8.3 330 760 12   6.4 230 440
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 0 32    32    300    800 .0041 0     13   6.9 270 670 11   5.8 200 400
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 0 33    33    320    860 .0041 0     17   9.1 240 750 11   6.0 210 400
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 0 39    39    380    1100 .0041 0     15   7.8 200 700 11   5.8 170 400
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 0 35    35    380    1200 .0041 0     19   10   170 780 11   6.0 250 410
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 0 35    35    300    840 .0041 0     13   6.9 230 670 10   5.6 150 400
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 0 35    35    310    900 .0041 0     17   8.8 240 780 11   6.1 200 410
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 0 44    44    390    1200 .0041 0     14   7.1 140 660 11   5.9 200 410
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 0 46    46    370    1300 .0041 0     16   8.4 190 790 12   6.3 230 420
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 0 100    100    840    3600 .0041 0     16   8.5 250 730 12   6.5 200 440
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 1 3.0  3.0  26    550 .0041 0     15   7.7 290 580 17   8.9 180 500
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 1 3.2  3.2  29    590 .0041 0     15   7.5 140 580 14   7.2 250 490
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 1 3.3  3.3  30    630 .0041 0     14   7.4 140 610 13   6.9 180 520
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 1 6.0  6.0  73    1200 .0041 0     19   9.7 240 680 14   7.5 240 510
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 1 5.2  5.2  49    1000 .0041 0     16   8.2 220 720 14   7.5 240 490
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 1 11    11    91    1900 .0041 0     16   8.5 330 690 14   7.2 180 510
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 1 3.4  3.4  30    670 .0041 0     15   7.7 300 620 14   7.4 230 520
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 1 6.5  6.5  68    1300 .0041 0     15   7.9 220 660 14   7.5 230 500
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 1 5.6  5.6  57    1000 .0041 0     16   8.3 270 690 16   8.3 260 500
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 1 11    11    88    2000 .0041 0     16   8.2 310 690 17   8.9 320 520
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 38    38    420    6700 .0041 0     16   8.2 130 700 18   9.5 220 480
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 0 34    34    320    840 .0041 0     13   6.7 170 650 12   6.2 240 410
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 0 35    35    350    900 .0041 0     17   8.9 280 790 12   6.2 170 430
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 0 42    42    390    1200 .0041 0     15   7.6 280 680 11   6.2 220 400
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 0 46    46    470    1300 .0041 0     18   9.4 350 900 15   7.8 140 410
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 87    87    1100    3600 .0041 0     15   8.0 180 760 13   7.1 180 450
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 4.6  4.6  43    960 .0041 0     .61 .40 9.2 44 6.0 3.2 130 290
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 8.9  8.9  84    1800 .0041 0     .48 .31 10   40 6.0 3.2 130 300
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 4.9  4.9  54    1100 .0041 0     .47 .30 9.4 40 6.2 3.3 120 310
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 10    10    93    2000 .0041 0     .59 .38 11   41 6.3 3.3 100 300
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 4.8  4.8  45    1000 .0041 0     .52 .34 7.8 42 6.8 3.5 130 320
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 9.4  9.4  79    1900 .0041 0     .67 .42 6.8 39 6.3 3.3 140 300
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 5.0  5.0  55    1100 .0041 0     .51 .33 12   43 5.6 3.0 37 300
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 9.7  9.7  110    2100 .0041 0     .53 .35 9.6 40 6.6 3.5 130 300
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c 0 41    41    400    7000 .0041 0     .55 .35 10   41 6.2 3.3 120 290
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 2 18    18    200    780 .0041 0     37    20    390   890 320   230   5900 7000
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 2 18    18    210    830 .0041 0     35    18    490   880 380   260   4600 7000
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 2 19    19    200    940 .0041 0     31    17    400   1300 310   220   5300 7000
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 2 19    19    160    1300 .0041 0     41    23    700   1600 350   250   4000 7000
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 2 22    22    310    940 .0041 0     30    16    460   1000 290   210   3000 7000
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 2 10    10    98    1200 .0041 0     43    24    630   1600 350   250   5400 7000
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 2 67    67    660    1000 .0041 0     75    58    1600   1700 230   150   3400 7000
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 2 72    72    680    1100 .0041 0     95    75    1400   1900 350   250   4000 7000
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 2 86    86    960    1100 .0041 0     86    68    1700   2000 230   150   3700 7000
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 2 82    82    750    1100 .0041 0     91    73    2400   2000 260   170   3500 7000
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 2 80    80    780    1100 .0041 0     83    64    1600   1900 210   140   1700 7000
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 2 86    86    780    1200 .0041 0     88    69    1800   2000 220   140   2900 7000
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 2 110    110    970    1500 .0041 0     160    140    4500   2100 220   140   3400 7000
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 2 110    110    1300    1600 .0041 0     160    140    2600   2300 280   190   4600 7000
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 2 90    90    810    1100 .0041 0     81    64    1500   2000 260   180   2700 7000
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 2 85    85    860    1200 .0041 0     110    94    2000   2100 310   200   5400 7000
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 2 100    100    990    1500 .0041 0     200    180    3700   2300 200   130   3000 7000
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 2 100    100    920    1600 .0041 0     170    150    3000   2500 250   170   3200 7000
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 2 59    59    570    770 .0041 0     45    27    590   1200 190   120   3200 7000
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 2 59    59    640    810 .0041 0     49    30    540   1100 240   160   4600 7000
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 2 66    66    740    800 .0041 0     40    24    860   1100 140   90   1600 7000
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 2 62    62    620    840 .0041 0     52    32    600   1100 200   130   1900 7000
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 2 74    74    670    840 .0041 0     39    24    890   1100 170   100   2600 7000
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 2 68    68    590    870 .0041 0     49    30    520   1200 230   150   2600 7000
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 2 72    72    870    1100 .0041 0     66    46    920   1500 170   100   2300 7000
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 2 80    80    890    1200 .0041 0     64    44    990   1600 240   150   2800 7000
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 2 74    74    600    860 .0041 0     40    25    810   1200 150   94   2400 7000
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 2 72    72    650    910 .0041 0     58    37    690   1600 220   140   2500 7000
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 2 90    90    780    1200 .0041 2.2   61    43    1300   1600 150   92   1800 7000
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 2 90    90    800    1200 .0041 0     56    37    910   1700 250   170   2700 7000
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 2 3.0  3.0  26    580 .0041 0     36    19    460   1200 160   100   2300 7000
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 2 3.2  3.2  30    630 .0041 0     39    21    380   890 160   110   3200 7000
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 2 3.4  3.4  32    670 .0041 0     37    19    530   870 190   120   2700 7000
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 2 6.4  6.4  54    1200 .0041 0     35    19    720   1700 180   110   2200 7000
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 2 5.6  5.6  51    1100 .0041 0     40    22    540   1400 160   100   2200 7000
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 2 11    11    120    2100 .0041 0     43    25    820   2000 180   110   1400 7000
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 2 3.6  3.6  31    710 .0041 0     39    21    500   1200 160   100   2900 7000
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 2 6.9  6.9  73    1300 .0041 0     40    23    490   1700 190   120   2100 7000
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 2 5.7  5.7  55    1100 .0041 0     41    23    550   1400 190   120   1700 7000
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 2 11    11    120    2200 .0041 0     47    27    700   1900 230   150   2000 7000
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 2 62    62    620    800 .0041 0     38    24    600   1100 160   97   2200 7000
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 2 59    59    740    830 .0041 0     39    24    350   1200 210   140   2800 7000
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 2 65    65    600    860 .0041 0     43    26    790   1200 170   100   2500 7000
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 2 77    77    770    910 .0041 0     49    31    690   1600 170   100   3100 7000
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 2 92    92    800    1200 .0041 0     51    35    920   1600 160   100   2200 7000
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 2 84    84    790    1200 .0041 0     62    43    930   1800 190   120   2200 7000
email_spec0_product16_false-unreach-call_true-termination.cil.c 1 38    38    340    310 .012  0     11   6.0 140 490 46   26   790 630
email_spec0_product21_false-unreach-call_true-termination.cil.c 1 57    57    840    530 .012  0     12   6.2 210 500 50   28   830 710
email_spec0_product22_false-unreach-call_true-termination.cil.c 1 43    43    390    330 .012  0     12   6.4 190 500 37   21   650 590
email_spec0_product26_false-unreach-call_true-termination.cil.c 1 73    73    710    590 .012  0     12   6.4 220 510 51   28   590 780
email_spec0_product31_false-unreach-call_true-termination.cil.c 1 35    35    460    340 .012  0     12   6.2 89 520 59   33   910 810
email_spec0_product33_false-unreach-call_true-termination.cil.c 1 42    42    410    370 .012  .19  13   6.7 140 600 40   23   670 620
email_spec0_product34_false-unreach-call_true-termination.cil.c 1 64    64    610    620 .012  0     12   6.3 88 530 53   30   970 760
email_spec0_product35_false-unreach-call_true-termination.cil.c 1 70    70    740    670 .012  .11  13   6.9 220 600 42   25   440 630
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 1 280    280    2200    7500 .012  0     13   6.9 250 650 12   6.7 220 470
email_spec11_product15_false-unreach-call_true-termination.cil.c 1 37    37    430    290 .012  0     12   6.2 230 500 48   26   810 640
email_spec11_product20_false-unreach-call_true-termination.cil.c 1 64    64    700    500 .012  0     11   6.1 140 500 38   22   610 610
email_spec11_product22_false-unreach-call_true-termination.cil.c 1 44    44    410    340 .012  0     12   6.2 240 460 41   23   630 580
email_spec11_product26_false-unreach-call_true-termination.cil.c 1 75    75    640    580 .012  0     15   7.7 190 500 40   23   440 610
email_spec11_product30_false-unreach-call_true-termination.cil.c 1 38    38    400    320 .012  0     12   6.6 250 520 45   25   610 680
email_spec11_product32_false-unreach-call_true-termination.cil.c 1 66    66    690    560 .012  0     12   6.4 240 550 57   33   840 820
email_spec11_product33_false-unreach-call_true-termination.cil.c 1 47    47    390    370 .012  0     12   6.4 260 520 48   27   750 720
email_spec11_product35_false-unreach-call_true-termination.cil.c 1 78    78    630    680 .012  0     12   6.1 99 530 54   31   960 820
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 1 380    380    2100    8000 .012  0     12   6.6 280 540 12   6.2 220 460
email_spec1_product14_false-unreach-call_true-termination.cil.c 1 28    28    380    350 .012  0     13   6.7 240 610 12   6.3 190 460
email_spec1_product15_false-unreach-call_true-termination.cil.c 1 18    18    180    230 .012  0     12   6.2 150 550 12   6.6 180 430
email_spec1_product16_false-unreach-call_true-termination.cil.c 1 19    19    240    240 .012  0     12   6.5 120 690 12   6.5 190 460
email_spec1_product20_false-unreach-call_true-termination.cil.c 1 36    36    390    390 .012  0     12   6.4 210 520 12   6.4 200 470
email_spec1_product21_false-unreach-call_true-termination.cil.c 1 31    31    380    430 .012  0     13   6.7 270 580 12   6.4 230 490
email_spec1_product22_false-unreach-call_true-termination.cil.c 1 23    23    230    270 .012  0     13   6.7 180 690 12   6.2 210 460
email_spec1_product26_false-unreach-call_true-termination.cil.c 1 43    43    440    480 .012  0     13   6.7 140 620 12   6.3 180 490
email_spec1_product29_false-unreach-call_true-termination.cil.c 1 34    34    330    420 .012  0     13   6.9 160 670 12   6.2 230 510
email_spec1_product30_false-unreach-call_true-termination.cil.c 1 21    21    210    260 .012  0     13   7.0 140 690 12   6.6 160 460
email_spec1_product31_false-unreach-call_true-termination.cil.c 1 22    22    210    280 .012  .10  14   7.5 280 680 13   6.7 210 480
email_spec1_product32_false-unreach-call_true-termination.cil.c 1 35    35    350    460 .012  .16  14   7.1 170 670 12   6.6 250 480
email_spec1_product33_false-unreach-call_true-termination.cil.c 1 23    23    230    300 .012  0     14   7.6 300 690 12   6.5 200 510
email_spec1_product34_false-unreach-call_true-termination.cil.c 1 40    40    410    530 .012  .11  14   7.2 190 690 12   6.5 200 500
email_spec1_product35_false-unreach-call_true-termination.cil.c 1 41    41    390    570 .012  0     15   8.1 300 710 12   6.6 200 480
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 140    140    1100    7100 .012  0     15   7.7 190 720 12   6.5 170 470
email_spec27_product17_false-unreach-call_true-termination.cil.c 1 30    30    320    370 .012  0     13   6.9 280 710 43   26   710 650
email_spec27_product18_false-unreach-call_true-termination.cil.c 1 22    22    200    230 .012  0     15   8.1 280 600 12   6.3 210 440
email_spec27_product19_false-unreach-call_true-termination.cil.c 1 21    21    270    250 .012  0     13   7.0 120 680 12   6.5 210 460
email_spec27_product23_false-unreach-call_true-termination.cil.c 1 38    38    420    410 .012  0     16   8.4 140 660 12   6.5 200 480
email_spec27_product24_false-unreach-call_true-termination.cil.c 1 23    23    230    270 .012  0     13   7.1 230 710 15   8.0 150 460
email_spec27_product25_false-unreach-call_true-termination.cil.c 1 37    37    390    440 .012  0     13   7.0 250 690 47   28   760 630
email_spec27_product27_false-unreach-call_true-termination.cil.c 1 40    40    470    480 .012  0     14   7.5 180 690 45   27   690 650
email_spec27_product29_false-unreach-call_true-termination.cil.c 1 32    32    330    430 .012  0     14   7.4 280 700 13   6.8 200 520
email_spec27_product30_false-unreach-call_true-termination.cil.c 1 20    20    260    260 .012  0     15   8.0 280 700 12   6.5 280 470
email_spec27_product31_false-unreach-call_true-termination.cil.c 1 22    22    200    290 .012  .38  15   8.1 290 720 12   6.3 180 500
email_spec27_product32_false-unreach-call_true-termination.cil.c 1 41    41    340    480 .012  0     15   7.8 310 690 14   7.2 220 500
email_spec27_product33_false-unreach-call_true-termination.cil.c 1 26    26    240    310 .012  0     15   7.9 300 710 14   7.6 210 500
email_spec27_product34_false-unreach-call_true-termination.cil.c 1 35    35    370    530 .012  0     14   7.6 130 720 12   6.6 210 510
email_spec27_product35_false-unreach-call_true-termination.cil.c 1 41    41    420    580 .012  .16  16   8.5 320 720 14   7.5 250 490
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c 1 450    450    2500    9800 .012  0     16   8.3 180 740 13   6.9 220 480
email_spec3_product13_false-unreach-call_true-termination.cil.c 1 .64 .63 5.8  100 .012  .11  10   5.4 190 440 31   17   580 530
email_spec3_product17_false-unreach-call_true-termination.cil.c 1 1.0  1.0  9.5  190 .012  0     11   6.0 220 470 35   20   630 550
email_spec3_product18_false-unreach-call_true-termination.cil.c 1 .67 .66 8.5  110 .012  .11  10   5.5 210 440 37   20   330 560
email_spec3_product19_false-unreach-call_true-termination.cil.c 1 .78 .76 6.8  130 .012  0     11   5.9 180 460 31   17   420 560
email_spec3_product23_false-unreach-call_true-termination.cil.c 1 1.0  1.0  11    220 .012  0     12   6.2 210 480 37   21   570 580
email_spec3_product24_false-unreach-call_true-termination.cil.c 1 .75 .74 7.4  140 .012  0     11   6.0 240 490 35   19   760 570
email_spec3_product25_false-unreach-call_true-termination.cil.c 1 1.2  1.2  11    260 .012  0     11   5.6 220 440 34   19   430 570
email_spec3_product27_false-unreach-call_true-termination.cil.c 1 1.4  1.3  13    280 .012  0     11   5.7 210 460 34   19   450 580
email_spec3_product28_false-unreach-call_true-termination.cil.c 1 .74 .73 7.3  120 .012  0     11   5.9 120 450 32   18   550 560
email_spec3_product29_false-unreach-call_true-termination.cil.c 1 1.2  1.2  15    250 .012  0     11   5.9 240 480 35   20   570 580
email_spec3_product30_false-unreach-call_true-termination.cil.c 1 .77 .76 6.8  130 .012  0     11   6.0 210 490 35   20   790 570
email_spec3_product31_false-unreach-call_true-termination.cil.c 1 .85 .89 7.9  170 .012  13     11   5.7 220 450 34   19   450 570
email_spec3_product32_false-unreach-call_true-termination.cil.c 1 1.3  1.3  14    280 .012  0     11   5.8 130 480 34   19   330 590
email_spec3_product33_false-unreach-call_true-termination.cil.c 1 .94 .93 7.3  170 .012  0     11   5.8 110 460 35   19   660 580
email_spec3_product34_false-unreach-call_true-termination.cil.c 1 1.5  1.5  14    350 .012  0     10   5.5 220 450 39   22   830 600
email_spec3_product35_false-unreach-call_true-termination.cil.c 1 1.7  1.7  18    380 .012  0     12   6.1 220 490 38   22   760 580
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 55    55    410    7300 .012  0     12   6.1 130 470 11   6.2 160 460
email_spec4_product18_false-unreach-call_true-termination.cil.c 1 18    18    250    230 .012  0     14   7.3 220 570 11   5.8 150 420
email_spec4_product19_false-unreach-call_true-termination.cil.c 1 19    19    200    250 .012  0     13   6.6 190 580 12   6.2 200 450
email_spec4_product23_false-unreach-call_true-termination.cil.c 1 31    31    300    390 .012  0     13   6.8 240 570 12   6.5 200 440
email_spec4_product24_false-unreach-call_true-termination.cil.c 1 25    25    270    270 .012  0     12   6.3 270 490 11   6.1 170 440
email_spec4_product25_false-unreach-call_true-termination.cil.c 1 36    36    360    430 .012  0     13   6.7 240 610 12   6.3 200 470
email_spec4_product27_false-unreach-call_true-termination.cil.c 1 38    38    390    470 .012  0     13   6.7 270 590 13   7.0 240 490
email_spec4_product30_false-unreach-call_true-termination.cil.c 1 20    20    200    250 .012  0     13   6.9 270 590 15   7.9 180 450
email_spec4_product31_false-unreach-call_true-termination.cil.c 1 19    19    210    280 .012  0     14   7.2 250 680 12   6.5 240 480
email_spec4_product32_false-unreach-call_true-termination.cil.c 1 35    35    330    450 .012  .10  13   6.7 230 640 12   6.5 240 480
email_spec4_product33_false-unreach-call_true-termination.cil.c 1 23    23    220    300 .012  0     15   8.1 270 710 12   6.6 210 510
email_spec4_product34_false-unreach-call_true-termination.cil.c 1 36    36    390    520 .012  0     13   7.0 99 710 12   6.3 240 500
email_spec4_product35_false-unreach-call_true-termination.cil.c 1 41    41    440    570 .012  0     15   7.7 220 690 14   7.5 290 500
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c 1 130    130    990    7100 .012  0     13   7.1 180 680 11   6.3 240 470
email_spec6_product12_false-unreach-call_true-termination.cil.c 1 18    18    200    210 .012  0     11   5.9 140 490 41   23   510 570
email_spec6_product14_false-unreach-call_true-termination.cil.c 1 30    30    410    370 .012  0     11   5.9 140 450 37   21   460 590
email_spec6_product15_false-unreach-call_true-termination.cil.c 1 16    16    170    230 .012  0     11   6.1 220 490 35   20   570 580
email_spec6_product16_false-unreach-call_true-termination.cil.c 1 21    21    220    250 .012  0     11   5.9 180 460 39   22   550 590
email_spec6_product20_false-unreach-call_true-termination.cil.c 1 36    36    390    410 .012  0     11   5.8 230 450 39   22   410 610
email_spec6_product21_false-unreach-call_true-termination.cil.c 1 37    37    450    460 .012  0     12   6.4 210 480 44   25   390 580
email_spec6_product22_false-unreach-call_true-termination.cil.c 1 26    26    280    280 .012  0     11   6.0 110 480 42   24   680 580
email_spec6_product26_false-unreach-call_true-termination.cil.c 1 40    40    390    490 .012  0     12   6.4 160 480 40   24   910 590
email_spec6_product28_false-unreach-call_true-termination.cil.c 1 19    19    220    240 .012  .12  11   5.9 190 490 39   23   640 580
email_spec6_product29_false-unreach-call_true-termination.cil.c 1 34    34    330    430 .012  0     11   6.0 190 450 46   27   470 610
email_spec6_product30_false-unreach-call_true-termination.cil.c 1 19    19    240    260 .012  0     12   6.1 230 480 38   22   580 600
email_spec6_product31_false-unreach-call_true-termination.cil.c 1 20    20    250    280 .012  0     12   6.1 220 450 38   22   560 590
email_spec6_product32_false-unreach-call_true-termination.cil.c 1 37    37    380    480 .012  0     12   6.2 220 500 43   25   540 630
email_spec6_product33_false-unreach-call_true-termination.cil.c 1 22    22    210    300 .012  0     12   6.2 200 500 37   22   650 580
email_spec6_product34_false-unreach-call_true-termination.cil.c 1 38    38    410    550 .012  0     12   6.2 140 510 42   24   620 610
email_spec6_product35_false-unreach-call_true-termination.cil.c 1 45    45    410    590 .012  0     16   8.1 230 540 41   24   550 630
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c 1 140    140    1400    7200 .012  0     13   6.9 160 560 13   6.9 260 470
email_spec7_product28_false-unreach-call_true-termination.cil.c 1 19    19    220    230 .012  0     12   6.5 190 490 38   21   620 570
email_spec7_product29_false-unreach-call_true-termination.cil.c 1 36    36    360    420 .012  0     12   6.1 170 480 40   22   610 600
email_spec7_product30_false-unreach-call_true-termination.cil.c 1 20    20    210    250 .012  0     11   5.6 87 450 34   19   380 580
email_spec7_product31_false-unreach-call_true-termination.cil.c 1 19    19    230    270 .012  0     11   6.0 210 460 38   21   590 590
email_spec7_product32_false-unreach-call_true-termination.cil.c 1 40    40    430    460 .012  .11  11   6.1 150 470 38   22   950 590
email_spec7_product33_false-unreach-call_true-termination.cil.c 1 23    23    260    300 .012  .10  11   5.9 130 460 35   19   360 580
email_spec7_product34_false-unreach-call_true-termination.cil.c 1 38    38    330    520 .012  0     11   5.8 200 450 37   21   500 610
email_spec7_product35_false-unreach-call_true-termination.cil.c 1 40    40    370    560 .012  0     11   5.8 140 450 37   21   320 600
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c 1 150    150    1300    7200 .012  0     12   6.5 240 500 12   6.4 180 460
email_spec8_product15_false-unreach-call_true-termination.cil.c 1 19    19    250    230 .012  0     12   6.6 170 560 12   6.4 230 440
email_spec8_product16_false-unreach-call_true-termination.cil.c 1 18    18    190    240 .012  0     13   6.8 240 690 11   6.1 240 440
email_spec8_product20_false-unreach-call_true-termination.cil.c 1 37    37    350    400 .012  0     12   6.5 260 600 12   6.5 160 450
email_spec8_product21_false-unreach-call_true-termination.cil.c 1 35    35    310    440 .012  .27  14   7.2 180 680 13   6.8 200 480
email_spec8_product22_false-unreach-call_true-termination.cil.c 1 19    19    190    260 .012  0     12   6.6 140 580 12   6.5 170 450
email_spec8_product26_false-unreach-call_true-termination.cil.c 1 37    37    370    480 .012  0     14   7.5 220 610 12   6.3 210 480
email_spec8_product30_false-unreach-call_true-termination.cil.c 1 18    18    160    250 .012  0     14   7.6 280 720 13   6.8 240 470
email_spec8_product31_false-unreach-call_true-termination.cil.c 1 22    22    240    280 .012  0     14   7.5 210 680 12   6.3 220 490
email_spec8_product32_false-unreach-call_true-termination.cil.c 1 36    36    470    460 .012  0     14   7.5 310 700 13   6.7 200 500
email_spec8_product33_false-unreach-call_true-termination.cil.c 1 26    26    240    300 .012  0     15   7.7 230 660 12   6.6 250 490
email_spec8_product34_false-unreach-call_true-termination.cil.c 1 37    37    370    530 .012  0     15   7.9 290 700 13   7.1 240 520
email_spec8_product35_false-unreach-call_true-termination.cil.c 1 41    41    350    570 .012  .14  13   7.1 180 700 12   6.7 250 490
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c 1 140    140    990    7200 .012  0     13   6.8 150 670 12   6.5 210 460
email_spec9_product15_false-unreach-call_true-termination.cil.c 1 21    21    240    230 .012  0     12   6.3 200 530 11   5.9 220 430
email_spec9_product16_false-unreach-call_true-termination.cil.c 1 20    20    190    240 .012  0     13   7.0 190 670 12   6.5 230 460
email_spec9_product20_false-unreach-call_true-termination.cil.c 1 34    34    420    400 .012  0     15   7.7 280 660 11   5.8 180 470
email_spec9_product21_false-unreach-call_true-termination.cil.c 1 36    36    400    440 .012  .20  14   7.5 270 700 12   6.6 240 490
email_spec9_product22_false-unreach-call_true-termination.cil.c 1 19    19    190    260 .012  0     12   6.6 270 610 12   6.5 220 440
email_spec9_product26_false-unreach-call_true-termination.cil.c 1 37    37    390    480 .012  0     13   6.6 160 610 13   7.1 220 480
email_spec9_product30_false-unreach-call_true-termination.cil.c 1 22    22    200    260 .012  0     14   7.4 240 690 12   6.4 230 470
email_spec9_product31_false-unreach-call_true-termination.cil.c 1 19    19    170    270 .012  .10  15   7.8 180 700 11   6.1 190 490
email_spec9_product32_false-unreach-call_true-termination.cil.c 1 38    38    360    470 .012  0     14   7.4 270 690 12   6.5 250 480
email_spec9_product33_false-unreach-call_true-termination.cil.c 1 24    24    200    300 .012  0     14   7.6 220 720 14   7.2 260 510
email_spec9_product34_false-unreach-call_true-termination.cil.c 1 35    35    340    530 .012  0     14   7.6 200 700 13   6.8 260 490
email_spec9_product35_false-unreach-call_true-termination.cil.c 1 44    44    520    570 .012  0     15   7.9 150 710 12   6.6 240 490
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 150    150    1100    7200 .012  0     15   7.9 270 710 12   6.5 190 460
email_spec0_product05_true-unreach-call_true-termination.cil.c 2 .43 .42 4.0  49 .012  0     14    7.1  150   490 13   6.9 240 370
email_spec0_product09_true-unreach-call_true-termination.cil.c 2 .64 .64 5.8  110 .012  0     18    9.5  280   520 15   7.7 310 410
email_spec0_product10_true-unreach-call_true-termination.cil.c 2 .45 .44 4.2  55 .012  0     16    8.5  190   450 13   6.8 220 390
email_spec0_product11_true-unreach-call_true-termination.cil.c 2 .59 .58 4.9  88 .012  0     22    11    220   510 14   7.5 190 440
email_spec0_product19_true-unreach-call_true-termination.cil.c 2 .72 .71 7.3  120 .012  0     25    13    260   590 22   11   220 570
email_spec0_product24_true-unreach-call_true-termination.cil.c 2 .74 .73 7.0  130 .012  0     23    12    410   660 20   11   220 580
email_spec0_product25_true-unreach-call_true-termination.cil.c 2 1.1  1.1  12    240 .012  0     32    16    310   680 22   12   360 630
email_spec0_product27_true-unreach-call_true-termination.cil.c 2 1.2  1.2  12    270 .012  0     28    14    400   690 24   12   370 610
email_spec0_product36_true-unreach-call_true-termination.cil.c 2 .76 .75 7.0  130 .012  0     19    9.7  350   480 14   7.4 240 430
email_spec0_product37_true-unreach-call_true-termination.cil.c 2 .61 .60 6.0  98 .012  0     18    9.6  280   500 31   16   500 710
email_spec0_product38_true-unreach-call_true-termination.cil.c 2 .80 .80 10    160 .012  .19  20    10    330   640 18   9.4 330 500
email_spec0_product40_true-unreach-call_true-termination.cil.c 2 .94 .94 8.6  180 .012  0     23    12    420   630 36   19   590 720
email_spec11_product03_true-unreach-call_true-termination.cil.c 2 .38 .37 3.4  45 .012  0     17    8.6  180   470 12   6.3 210 370
email_spec11_product07_true-unreach-call_true-termination.cil.c 2 .59 .59 5.4  95 .012  0     17    8.9  340   490 14   7.3 260 390
email_spec11_product08_true-unreach-call_true-termination.cil.c 2 .59 .58 5.2  81 .012  0     18    9.2  270   500 19   10   150 650
email_spec11_product10_true-unreach-call_true-termination.cil.c 2 .45 .44 4.4  56 .012  0     17    8.7  250   490 13   6.9 280 380
email_spec11_product18_true-unreach-call_true-termination.cil.c 2 .66 .66 5.6  110 .012  0     26    13    290   550 21   11   340 580
email_spec11_product23_true-unreach-call_true-termination.cil.c 2 1.0  1.0  9.3  200 .012  .16  22    11    320   650 23   12   340 810
email_spec11_product24_true-unreach-call_true-termination.cil.c 2 .76 .75 6.7  130 .012  0     22    11    310   640 21   11   340 570
email_spec11_product27_true-unreach-call_true-termination.cil.c 2 1.2  1.2  11    270 .012  0     25    13    480   680 24   12   340 600
email_spec11_product36_true-unreach-call_true-termination.cil.c 2 .75 .74 6.7  130 .012  0     27    14    260   460 17   8.8 240 440
email_spec11_product37_true-unreach-call_true-termination.cil.c 2 .63 .62 5.7  97 .012  0     19    9.6  320   490 21   11   320 610
email_spec11_product39_true-unreach-call_true-termination.cil.c 2 .80 .79 7.4  140 .012  0     29    15    280   650 21   11   350 600
email_spec11_product40_true-unreach-call_true-termination.cil.c 2 .98 .97 9.5  180 .012  0     27    14    330   640 21   11   310 590
email_spec1_product12_true-unreach-call_true-termination.cil.c 2 .60 .60 5.8  95 .012  0     25    14    500   760 100   62   800 6300
email_spec1_product28_true-unreach-call_true-termination.cil.c 2 .75 .74 6.4  120 .012  0     38    22    470   940 220   140   2500 7000
email_spec27_product13_true-unreach-call_true-termination.cil.c 2 .64 .63 6.1  100 .012  0     43    25    420   880 240   160   5100 7000
email_spec27_product28_true-unreach-call_true-termination.cil.c 2 .72 .71 8.3  130 .012  0     34    20    720   990 200   130   3500 7000
email_spec4_product13_true-unreach-call_true-termination.cil.c 2 .63 .66 6.2  110 .012  11     31    18    580   940 250   170   3000 7000
email_spec4_product17_true-unreach-call_true-termination.cil.c 2 .96 .95 8.6  180 .012  0     35    22    400   1100 280   210   2800 7000
email_spec4_product28_true-unreach-call_true-termination.cil.c 2 .70 .69 6.7  120 .012  0     32    19    720   920 150   93   1600 7000
email_spec4_product29_true-unreach-call_true-termination.cil.c 2 1.1  1.1  14    250 .012  0     52    34    810   1400 200   130   1900 7000
email_spec7_product13_true-unreach-call_true-termination.cil.c 2 .64 .63 5.6  93 .012  0     19    10    310   510 15   7.8 260 430
email_spec7_product17_true-unreach-call_true-termination.cil.c 2 .91 .91 8.7  170 .012  0     27    14    380   650 21   11   270 500
email_spec7_product18_true-unreach-call_true-termination.cil.c 2 .65 .64 6.5  100 .012  0     26    13    270   540 19   10   330 590
email_spec7_product19_true-unreach-call_true-termination.cil.c 2 .70 .69 7.9  120 .012  0     21    11    380   540 17   8.8 190 460
email_spec7_product23_true-unreach-call_true-termination.cil.c 2 1.0  1.0  8.6  200 .012  0     27    14    300   660 22   11   250 610
email_spec7_product24_true-unreach-call_true-termination.cil.c 2 .74 .73 7.8  130 .012  0     19    9.9  240   610 20   10   350 540
email_spec7_product25_true-unreach-call_true-termination.cil.c 2 1.2  1.2  11    240 .012  0     25    13    190   660 20   10   320 520
email_spec7_product27_true-unreach-call_true-termination.cil.c 2 1.2  1.2  12    260 .012  0     27    14    490   660 22   12   320 690
email_spec8_product12_true-unreach-call_true-termination.cil.c 2 .60 .60 7.3  96 .012  0     32    18    440   850 99   58   1200 5500
email_spec8_product14_true-unreach-call_true-termination.cil.c 2 87    87    860    580 .012  .28  48    30    800   1200 160   99   2400 7000
email_spec8_product28_true-unreach-call_true-termination.cil.c 2 .75 .74 6.5  120 .012  0     39    23    380   930 160   97   1900 7000
email_spec8_product29_true-unreach-call_true-termination.cil.c 2 95    95    930    650 .012  0     50    33    1100   1300 170   100   1900 7000
email_spec9_product12_true-unreach-call_true-termination.cil.c 2 .64 .63 5.7  95 .012  0     37    20    400   830 100   62   1200 5700
email_spec9_product14_true-unreach-call_true-termination.cil.c 2 100    100    990    570 .012  0     40    25    890   1200 190   120   2700 7000
email_spec9_product28_true-unreach-call_true-termination.cil.c 2 .74 .73 6.9  120 .012  0     34    19    600   930 120   76   1500 7000
email_spec9_product29_true-unreach-call_true-termination.cil.c 2 99    99    860    650 .012  0     45    30    550   1400 150   93   2000 7000
minepump_spec1_product33_false-unreach-call_false-termination.cil.c 1 .18 .17 1.1  26 .0041 0     6.6 3.6 94 290 8.1 4.4 120 320
minepump_spec1_product34_false-unreach-call_false-termination.cil.c 1 .16 .15 1.3  27 .0041 0     5.9 3.2 130 290 9.2 4.9 170 330
minepump_spec1_product35_false-unreach-call_false-termination.cil.c 1 .16 .15 1.3  27 .0041 0     6.4 3.4 130 330 8.1 4.3 140 330
minepump_spec1_product36_false-unreach-call_false-termination.cil.c 1 .18 .17 1.2  27 .0041 0     6.0 3.3 110 310 8.3 4.4 150 320
minepump_spec1_product37_false-unreach-call_false-termination.cil.c 1 .17 .16 1.2  27 .0041 0     5.9 3.2 110 320 8.4 4.5 190 320
minepump_spec1_product38_false-unreach-call_false-termination.cil.c 1 .17 .16 1.3  27 .0041 0     6.0 3.2 71 340 8.0 4.3 160 320
minepump_spec1_product39_false-unreach-call_false-termination.cil.c 1 .18 .17 1.3  29 .0041 0     5.8 3.2 100 290 7.5 4.1 130 320
minepump_spec1_product40_false-unreach-call_false-termination.cil.c 1 .19 .18 1.2  29 .0041 0     6.0 3.3 94 330 8.0 4.3 160 320
minepump_spec1_product41_false-unreach-call_false-termination.cil.c 1 .40 .40 5.1  31 .0041 0     6.1 3.3 120 300 8.2 4.4 150 320
minepump_spec1_product42_false-unreach-call_false-termination.cil.c 1 .36 .36 4.3  31 .0041 0     6.8 3.6 140 300 9.7 5.1 180 330
minepump_spec1_product43_false-unreach-call_false-termination.cil.c 1 .49 .48 5.5  32 .0041 0     5.9 3.2 80 290 8.5 4.5 140 330
minepump_spec1_product44_false-unreach-call_false-termination.cil.c 1 .42 .41 5.3  32 .0041 0     6.9 3.7 150 340 13   6.8 220 400
minepump_spec1_product49_false-unreach-call_false-termination.cil.c 1 .17 .16 1.4  27 .0041 0     5.8 3.1 100 330 8.1 4.3 170 330
minepump_spec1_product50_false-unreach-call_false-termination.cil.c 1 .20 .19 1.3  27 .0041 0     5.8 3.1 60 320 9.2 4.8 180 330
minepump_spec1_product51_false-unreach-call_false-termination.cil.c 1 .19 .18 1.5  27 .0041 0     5.7 3.1 95 290 8.6 4.6 160 330
minepump_spec1_product52_false-unreach-call_false-termination.cil.c 1 .19 .19 1.3  27 .0041 0     5.8 3.1 78 290 9.2 4.9 100 320
minepump_spec1_product53_false-unreach-call_false-termination.cil.c 1 .19 .19 1.8  28 .0041 0     6.2 3.4 120 350 8.5 4.5 170 320
minepump_spec1_product54_false-unreach-call_false-termination.cil.c 1 .20 .19 2.2  29 .0041 0     6.0 3.2 46 350 7.9 4.3 170 320
minepump_spec1_product55_false-unreach-call_false-termination.cil.c 1 .20 .19 1.7  28 .0041 0     5.9 3.2 110 300 8.5 4.6 160 320
minepump_spec1_product56_false-unreach-call_false-termination.cil.c 1 .21 .20 1.7  30 .0041 0     6.2 3.4 140 340 8.2 4.4 160 320
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c 1 .34 .33 3.1  44 .0041 0     6.8 3.6 140 310 9.1 4.9 190 330
minepump_spec2_product33_false-unreach-call_false-termination.cil.c 1 .49 .48 4.5  31 .0041 0     6.3 3.4 130 290 7.8 4.2 160 330
minepump_spec2_product34_false-unreach-call_false-termination.cil.c 1 .45 .44 4.7  32 .0041 0     7.0 3.8 130 350 12   6.4 250 410
minepump_spec2_product35_false-unreach-call_false-termination.cil.c 1 .45 .44 4.9  32 .0041 .17  6.2 3.3 130 290 9.0 4.8 130 320
minepump_spec2_product36_false-unreach-call_false-termination.cil.c 1 .45 .44 6.0  32 .0041 0     7.0 3.7 120 330 9.3 5.0 170 340
minepump_spec2_product41_false-unreach-call_false-termination.cil.c 1 .81 .80 10    36 .0041 0     6.7 3.6 90 320 8.3 4.4 140 330
minepump_spec2_product42_false-unreach-call_false-termination.cil.c 1 .83 .83 9.9  36 .0041 0     7.0 3.8 110 320 13   6.8 210 410
minepump_spec2_product43_false-unreach-call_false-termination.cil.c 1 .77 .77 9.5  38 .0041 0     6.6 3.5 91 300 8.3 4.4 150 320
minepump_spec2_product44_false-unreach-call_false-termination.cil.c 1 .89 .88 11    38 .0041 0     7.3 3.9 140 330 8.3 4.4 150 320
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c 1 .62 .61 7.6  60 .0041 0     8.1 4.3 160 370 8.0 4.4 160 310
minepump_spec3_product01_false-unreach-call_false-termination.cil.c 1 .15 .15 1.1  26 .0041 0     5.8 3.2 66 340 8.6 4.7 160 330
minepump_spec3