Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-ProductLines
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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 0 480    480    6300   370 1.0  0      10    5.3  160   460 10   5.5 180 370
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 0 480    480    4300   520 1.0  0      12    6.3  100   460 13   7.2 130 400
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 0 480    480    5200   450 1.0  34      9.9  5.2  180   450 15   7.8 120 400
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 0 6.1  6.1  57   540 1.0  .29   12    6.5  140   520 12   6.5 160 400
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 0 530    530    5400   1400 1.1  .37   9.2  4.9  130   380 11   6.1 180 430
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 0 490    490    5900   180 6.2  0      11    6.0  140   500 9.4 5.2 88 390
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 0 490    490    5600   200 6.3  0      9.6  5.1  180   470 12   6.6 180 420
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 0 500    500    5700   240 6.3  0      11    5.6  160   460 11   6.2 190 420
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 0 500    500    5800   330 6.3  0      12    6.5  99   480 13   6.9 140 420
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 0 490    490    5700   200 6.2  .34   10    5.4  160   500 14   7.3 180 410
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 0 490    490    6100   210 6.3  0      13    6.8  190   560 14   7.4 160 410
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 0 500    500    6000   330 6.3  0      12    6.5  150   540 11   6.2 200 410
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 0 500    500    5900   340 6.3  0      15    7.7  140   480 12   6.5 160 430
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 700    700    7700   760 6.4  0      8.7  4.6  190   340 12   6.8 180 460
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 0 490    490    6100   180 6.2  0      12    6.2  140   460 10   5.6 180 390
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 0 490    490    6000   200 6.2  0      13    6.6  140   490 13   7.0 120 420
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 0 500    500    5500   240 6.4  0      11    6.0  160   470 13   7.2 150 410
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 0 500    500    6000   330 6.3  0      11    5.8  130   460 10   5.6 190 410
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 0 490    490    6500   200 6.2  0      11    5.8  160   460 14   7.7 130 390
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 0 490    490    6000   220 6.3  0      13    6.6  140   470 11   6.0 190 400
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 0 500    500    6000   320 6.3  0      12    6.3  140   460 12   6.6 190 420
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 0 500    500    6500   340 6.3  0      10    5.4  160   500 15   8.0 130 400
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 0 700    700    9400   730 6.4  0      9.0  4.7  160   380 12   6.7 190 450
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 0 480    480    6700   250 1.0  0      15    7.6  130   490 14   7.2 130 450
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 0 480    480    5700   270 1.0  0      13    6.7  190   490 13   6.7 190 470
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 0 480    480    6100   420 1.0  0      13    7.0  170   490 12   6.3 180 460
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 0 480    480    4500   390 1.0  0      18    9.3  180   530 14   7.3 190 470
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 0 480    480    5500   320 1.0  0      15    8.0  190   570 15   7.9 160 470
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 0 480    480    4900   540 1.0  0      12    6.4  220   550 11   6.2 220 480
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 0 480    480    6000   430 1.0  0      12    6.0  220   530 13   7.0 150 480
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 0 480    480    5600   420 1.0  0      15    7.8  160   520 15   8.2 130 460
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 0 480    480    5500   330 1.0  0      16    8.4  180   520 16   8.6 190 490
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 0 480    480    5500   560 1.0  0      15    7.9  190   520 12   6.4 190 490
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 620    620    4200   1400 1.1  0      13    6.8  190   420 13   6.8 250 480
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 0 490    490    6500   190 6.2  0      12    6.2  130   460 12   6.3 180 410
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 0 490    490    5400   220 6.3  0      13    7.0  140   510 12   6.4 170 410
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 0 500    500    5800   320 6.3  0      11    5.8  200   510 11   6.2 190 400
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 0 500    500    5100   340 6.3  0      12    6.5  150   480 14   7.4 150 410
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 700    700    7300   720 6.4  0      12    6.1  130   380 17   9.1 110 430
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 890    900    11000   1500 16    0      .53 .33 12   39 6.4 3.4 120 300
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 890    900    11000   2100 16    0      .65 .42 8.7 40 7.5 3.9 130 310
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 890    900    12000   660 16    0      .56 .36 8.2 39 6.6 3.5 95 300
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 890    900    13000   2400 16    0      .50 .33 10   39 6.0 3.2 89 300
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 890    900    11000   1700 16    0      .60 .38 7.4 40 5.8 3.1 88 300
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 890    900    9000   770 16    35      .52 .34 11   39 7.2 3.8 100 300
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 890    900    12000   670 16    0      .67 .43 7.7 42 6.5 3.4 67 320
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 890    900    10000   750 16    .21   .49 .31 10   39 6.2 3.3 98 310
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c 0 890    900    9100   1500 8.2  34      .52 .34 12   40 6.0 3.1 77 300
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 2 540    540    6700   290 21    0      25    14    510   900 230   160   2500 7000
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 2 550    540    6500   290 21    .0041 27    15    600   1000 290   200   4700 7000
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 2 550    540    6600   300 21    0      32    17    400   930 300   210   2600 7000
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 2 660    650    7400   350 29    34      34    19    540   1300 270   190   4300 7000
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 2 550    550    6300   290 22    0      31    17    390   970 320   230   5000 7000
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 2 660    660    8600   330 29    0      35    20    740   1300 250   170   3100 7000
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 2 520    510    6100   280 22    0      69    55    1300   1500 220   150   2500 7000
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 2 540    540    5600   290 21    0      80    64    900   1700 260   180   2900 7000
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 2 540    540    7000   290 22    0      83    66    1100   1600 260   180   3100 7000
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 2 550    540    6900   300 25    0      89    73    1200   1700 250   170   5200 7000
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 2 530    520    6600   290 21    0      68    54    1200   2000 210   140   3100 7000
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 2 550    540    7200   300 21    0      73    59    1500   1700 240   150   3200 7000
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 2 570    570    6600   300 21    0      150    130    2600   2000 190   120   1800 7000
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 2 580    580    7600   290 21    0      130    120    2800   2100 210   150   2400 7000
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 2 550    540    7700   300 21    .0041 84    67    1000   1700 300   200   4400 7000
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 2 550    550    6000   290 21    0      110    92    1000   1800 230   160   3900 7000
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 2 580    570    7000   310 21    0      200    180    2400   2100 170   110   2100 7000
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 2 590    580    6800   300 21    0      170    150    1900   2300 250   170   4000 7000
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 2 440    440    5200   280 11    0      37    22    520   1100 180   110   1600 7000
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 2 500    500    7200   280 11    0      46    28    400   1100 170   110   3300 7000
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 2 500    500    5500   280 11    0      35    22    510   1100 150   95   2900 7000
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 2 500    500    5800   290 11    .13   40    26    720   1200 240   150   2200 7000
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 2 480    480    6000   280 11    0      38    24    730   1200 140   89   1400 7000
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 2 500    500    6900   290 11    0      37    24    800   1200 180   110   2300 7000
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 2 510    510    6300   280 11    .13   45    33    400   1300 180   110   2300 7000
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 2 510    510    6300   320 11    34      51    35    850   1300 240   160   4000 7000
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 2 500    500    7200   280 11    0      41    25    580   1100 150   92   2300 7000
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 2 510    500    6100   290 11    0      42    27    750   1300 170   110   2100 7000
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 2 510    510    6400   280 11    0      49    35    660   1400 130   79   990 7000
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 2 510    510    6100   280 11    0      56    37    710   1400 220   140   2000 7000
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 2 490    490    6000   300 3.5  .0041 25    14    260   990 190   120   1500 7000
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 2 490    490    6900   330 3.6  .0041 28    15    360   930 170   110   2300 7000
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 2 490    490    5800   290 3.5  .0041 30    16    500   900 150   97   1400 7000
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 2 490    490    5200   350 3.6  .0041 35    19    530   1400 150   98   2700 7000
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 2 490    490    6400   610 3.6  0      39    21    450   1100 150   97   1300 7000
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 2 500    490    4800   460 3.6  0      43    25    400   1500 170   110   2400 7000
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 2 490    490    6200   330 3.6  0      29    16    360   960 190   120   3200 7000
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 2 490    490    5400   400 3.6  0      32    18    540   1500 170   110   2200 7000
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 2 490    490    5800   320 3.6  .0041 30    17    490   1200 180   120   1500 7000
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 2 500    490    6800   520 3.6  0      37    21    730   1500 180   120   1800 7000
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 2 500    500    6800   280 11    .13   43    27    530   1000 140   88   1000 7000
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 2 500    500    6800   290 11    .0041 39    25    790   1100 210   130   1900 7000
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 2 500    500    5500   280 11    0      44    27    310   1100 170   99   1900 7000
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 2 510    500    7200   280 11    0      38    24    790   1200 180   110   3200 7000
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 2 510    510    6200   280 11    0      49    34    450   1400 180   110   2100 7000
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 2 510    510    5700   280 11    0      53    37    930   1400 150   97   1300 7000
email_spec0_product16_false-unreach-call_true-termination.cil.c 0 490    490    5100   150 8.7  0      20    10    240   790 13   6.7 130 450
email_spec0_product21_false-unreach-call_true-termination.cil.c 0 500    500    5900   170 9.0  0      25    14    300   1100 14   7.6 150 500
email_spec0_product22_false-unreach-call_true-termination.cil.c 0 490    490    5600   150 8.7  0      19    10    280   790 13   7.2 140 450
email_spec0_product26_false-unreach-call_true-termination.cil.c 0 500    500    5900   320 8.7  0      27    15    510   940 15   8.1 170 500
email_spec0_product31_false-unreach-call_true-termination.cil.c 0 490    490    5300   160 8.8  0      26    14    330   790 15   8.2 140 490
email_spec0_product33_false-unreach-call_true-termination.cil.c 0 490    490    5200   200 8.8  0      28    15    290   790 14   7.5 160 470
email_spec0_product34_false-unreach-call_true-termination.cil.c 0 500    500    5800   260 8.8  0      33    18    320   1700 14   7.3 220 510
email_spec0_product35_false-unreach-call_true-termination.cil.c 0 500    500    5200   310 8.8  0      34    19    480   1100 12   6.6 150 500
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 890    900    9000   1600 7.8  0      .54 .34 13   43 6.9 3.6 130 310
email_spec11_product15_false-unreach-call_true-termination.cil.c 0 490    490    5100   130 8.7  0      15    8.0  300   760 11   6.1 210 450
email_spec11_product20_false-unreach-call_true-termination.cil.c 0 490    490    6400   220 8.7  0      25    13    320   1100 12   6.3 220 470
email_spec11_product22_false-unreach-call_true-termination.cil.c 0 490    490    6900   280 8.7  0      23    12    250   760 13   6.9 200 470
email_spec11_product26_false-unreach-call_true-termination.cil.c 0 500    500    6400   410 8.7  0      35    19    330   950 15   7.7 140 480
email_spec11_product30_false-unreach-call_true-termination.cil.c 0 490    490    5700   190 8.7  0      21    11    370   770 12   6.5 200 460
email_spec11_product32_false-unreach-call_true-termination.cil.c 0 500    500    5400   200 8.7  0      28    15    400   1000 11   6.2 120 480
email_spec11_product33_false-unreach-call_true-termination.cil.c 0 490    490    5800   260 8.7  0      25    13    260   1100 15   7.6 220 500
email_spec11_product35_false-unreach-call_true-termination.cil.c 0 500    500    5100   240 8.8  0      28    16    430   1600 16   8.5 220 500
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 890    900    10000   1600 7.8  34      .63 .39 8.5 40 6.3 3.3 130 300
email_spec1_product14_false-unreach-call_true-termination.cil.c 0 490    490    5400   260 6.2  0      18    9.4  350   730 13   7.0 160 460
email_spec1_product15_false-unreach-call_true-termination.cil.c 0 490    490    5800   170 6.2  .17   18    9.6  190   760 15   8.1 140 420
email_spec1_product16_false-unreach-call_true-termination.cil.c 0 490    490    5700   370 6.2  0      15    8.2  310   780 14   7.3 220 460
email_spec1_product20_false-unreach-call_true-termination.cil.c 0 490    490    5500   240 6.2  0      27    14    290   1100 14   7.4 150 470
email_spec1_product21_false-unreach-call_true-termination.cil.c 0 490    490    5400   210 6.2  0      24    13    390   1100 13   6.7 280 470
email_spec1_product22_false-unreach-call_true-termination.cil.c 0 490    490    5300   180 6.2  0      21    11    310   780 13   7.1 150 440
email_spec1_product26_false-unreach-call_true-termination.cil.c 0 490    490    6000   230 6.2  0      24    13    350   1200 14   7.3 210 510
email_spec1_product29_false-unreach-call_true-termination.cil.c 0 490    490    6400   210 6.2  34      22    12    450   770 15   8.1 150 490
email_spec1_product30_false-unreach-call_true-termination.cil.c 0 490    490    5300   250 6.2  0      23    12    360   800 13   7.0 200 450
email_spec1_product31_false-unreach-call_true-termination.cil.c 0 490    490    4700   190 6.3  34      27    14    290   800 12   6.4 230 500
email_spec1_product32_false-unreach-call_true-termination.cil.c 0 490    490    5000   440 6.3  0      25    13    400   1200 12   6.7 200 480
email_spec1_product33_false-unreach-call_true-termination.cil.c 0 490    490    4900   190 6.3  0      25    13    270   1100 12   6.4 190 500
email_spec1_product34_false-unreach-call_true-termination.cil.c 0 490    490    5400   360 6.3  0      34    19    440   980 13   7.2 140 510
email_spec1_product35_false-unreach-call_true-termination.cil.c 0 490    490    5600   320 6.3  0      33    18    500   1100 14   7.2 160 500
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 620    620    7400   1600 6.4  0      13    6.9  160   420 12   6.6 200 480
email_spec27_product17_false-unreach-call_true-termination.cil.c 0 490    490    4800   190 6.2  0      20    10    360   710 14   7.2 130 500
email_spec27_product18_false-unreach-call_true-termination.cil.c 0 490    490    6600   130 6.2  0      18    9.4  330   690 16   8.4 140 440
email_spec27_product19_false-unreach-call_true-termination.cil.c 0 490    490    6200   240 6.3  0      22    11    240   800 15   7.9 160 450
email_spec27_product23_false-unreach-call_true-termination.cil.c 0 490    490    5600   240 6.3  0      24    13    420   1100 13   7.2 200 470
email_spec27_product24_false-unreach-call_true-termination.cil.c 0 490    490    4600   180 6.3  0      20    11    330   780 12   6.2 160 490
email_spec27_product25_false-unreach-call_true-termination.cil.c 0 490    490    5900   210 6.3  0      28    15    490   920 11   6.1 150 490
email_spec27_product27_false-unreach-call_true-termination.cil.c 0 490    490    4900   180 6.3  0      31    17    340   1200 13   6.8 190 490
email_spec27_product29_false-unreach-call_true-termination.cil.c 0 490    490    5500   190 6.3  0      29    15    300   800 14   7.4 190 490
email_spec27_product30_false-unreach-call_true-termination.cil.c 0 490    490    5300   320 6.3  0      22    11    420   800 15   7.7 160 440
email_spec27_product31_false-unreach-call_true-termination.cil.c 0 490    490    5800   170 6.3  0      21    11    300   1100 15   8.1 130 510
email_spec27_product32_false-unreach-call_true-termination.cil.c 0 490    490    6600   280 6.5  0      29    16    400   1400 13   6.9 130 500
email_spec27_product33_false-unreach-call_true-termination.cil.c 0 490    490    5700   150 6.3  0      29    15    260   800 14   7.2 160 510
email_spec27_product34_false-unreach-call_true-termination.cil.c 0 490    490    5500   440 6.3  0      31    17    580   1100 13   6.8 150 500
email_spec27_product35_false-unreach-call_true-termination.cil.c 0 500    500    4700   390 6.4  0      29    16    570   1700 15   7.8 190 500
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c 0 740    740    6600   1600 6.5  0      10    5.4  200   410 16   8.5 160 490
email_spec3_product13_false-unreach-call_true-termination.cil.c 0 480    480    4400   170 1.0  35      14    7.6  190   670 30   17   430 550
email_spec3_product17_false-unreach-call_true-termination.cil.c 0 480    480    5500   220 1.0  0      16    8.5  210   760 31   17   310 550
email_spec3_product18_false-unreach-call_true-termination.cil.c 0 480    480    4700   150 1.0  0      20    11    190   770 12   6.5 160 420
email_spec3_product19_false-unreach-call_true-termination.cil.c 0 480    480    4900   170 1.0  0      21    11    190   780 11   5.9 200 430
email_spec3_product23_false-unreach-call_true-termination.cil.c 0 480    480    5700   330 1.0  0      26    14    380   1100 10   5.6 130 450
email_spec3_product24_false-unreach-call_true-termination.cil.c 0 480    480    5000   150 1.0  0      18    9.4  350   830 15   7.8 150 430
email_spec3_product25_false-unreach-call_true-termination.cil.c 0 480    480    5200   420 1.0  0      28    15    380   1100 17   9.1 160 490
email_spec3_product27_false-unreach-call_true-termination.cil.c 0 480    480    5300   220 1.0  0      29    16    270   1400 15   8.1 170 460
email_spec3_product28_false-unreach-call_true-termination.cil.c 0 480    480    5300   140 1.0  0      14    7.5  210   790 38   21   420 560
email_spec3_product29_false-unreach-call_true-termination.cil.c 0 480    480    6300   300 1.0  0      24    13    310   1300 41   23   380 580
email_spec3_product30_false-unreach-call_true-termination.cil.c 0 480    480    5500   210 1.0  .29   23    12    250   850 11   5.8 160 430
email_spec3_product31_false-unreach-call_true-termination.cil.c 0 480    480    5200   240 1.0  0      23    12    310   810 13   7.2 140 450
email_spec3_product32_false-unreach-call_true-termination.cil.c 0 480    480    5800   200 1.0  0      30    16    450   980 14   7.5 180 470
email_spec3_product33_false-unreach-call_true-termination.cil.c 0 480    480    5100   280 1.0  0      23    12    300   1100 12   6.3 170 450
email_spec3_product34_false-unreach-call_true-termination.cil.c 0 480    480    5000   200 1.0  0      32    18    450   1100 15   8.2 180 480
email_spec3_product35_false-unreach-call_true-termination.cil.c 0 480    480    5900   260 1.0  0      30    17    570   1100 16   8.4 140 480
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 510    510    4300   1600 1.1  0      8.4  4.4  130   370 15   8.0 150 460
email_spec4_product18_false-unreach-call_true-termination.cil.c 0 490    490    5500   190 6.2  0      20    10    230   780 12   6.4 180 430
email_spec4_product19_false-unreach-call_true-termination.cil.c 0 490    490    5100   140 6.2  0      22    11    220   780 13   7.0 140 450
email_spec4_product23_false-unreach-call_true-termination.cil.c 0 490    490    6000   270 6.2  34      27    14    260   1100 14   7.5 110 450
email_spec4_product24_false-unreach-call_true-termination.cil.c 0 490    490    5000   220 6.2  0      20    10    260   790 11   6.1 190 450
email_spec4_product25_false-unreach-call_true-termination.cil.c 0 490    490    5400   200 6.2  0      30    16    310   1100 12   6.3 210 480
email_spec4_product27_false-unreach-call_true-termination.cil.c 0 490    490    5600   360 6.3  0      25    13    540   1200 12   6.3 180 480
email_spec4_product30_false-unreach-call_true-termination.cil.c 0 490    490    6500   230 6.2  0      17    9.0  370   790 11   6.0 150 450
email_spec4_product31_false-unreach-call_true-termination.cil.c 0 490    490    5300   510 6.3  0      25    13    390   820 13   6.9 140 480
email_spec4_product32_false-unreach-call_true-termination.cil.c 0 490    490    5400   210 6.2  0      24    13    410   1200 11   6.1 190 470
email_spec4_product33_false-unreach-call_true-termination.cil.c 0 490    490    6500   150 6.3  0      24    12    410   840 12   6.3 180 470
email_spec4_product34_false-unreach-call_true-termination.cil.c 0 490    490    5600   340 6.3  0      32    18    430   970 12   6.4 180 500
email_spec4_product35_false-unreach-call_true-termination.cil.c 0 490    490    6100   280 6.3  0      36    19    400   1000 12   6.3 190 490
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c 0 620    620    5900   1600 6.3  0      12    6.2  200   400 13   7.0 200 480
email_spec6_product12_false-unreach-call_true-termination.cil.c 0 490    490    6600   160 6.2  0      15    7.8  220   670 34   19   500 560
email_spec6_product14_false-unreach-call_true-termination.cil.c 0 490    490    6000   170 6.2  0      18    9.5  230   790 36   21   310 580
email_spec6_product15_false-unreach-call_true-termination.cil.c 0 490    490    6300   150 6.2  0      18    9.6  190   760 12   6.4 170 440
email_spec6_product16_false-unreach-call_true-termination.cil.c 0 490    490    5400   140 6.2  0      21    11    240   790 14   7.4 160 450
email_spec6_product20_false-unreach-call_true-termination.cil.c 0 490    490    6800   360 6.2  0      25    13    490   900 11   5.8 210 450
email_spec6_product21_false-unreach-call_true-termination.cil.c 0 490    490    5400   190 6.2  0      25    13    430   1200 16   8.4 180 490
email_spec6_product22_false-unreach-call_true-termination.cil.c 0 490    490    5600   170 6.2  0      19    10    230   770 11   5.7 98 440
email_spec6_product26_false-unreach-call_true-termination.cil.c 0 490    490    5000   220 6.2  0      26    14    390   1400 12   6.4 170 470
email_spec6_product28_false-unreach-call_true-termination.cil.c 0 490    490    5600   180 6.2  0      17    8.8  220   650 41   24   480 590
email_spec6_product29_false-unreach-call_true-termination.cil.c 0 490    490    5400   240 6.2  .17   24    13    330   790 53   30   540 620
email_spec6_product30_false-unreach-call_true-termination.cil.c 0 490    490    5100   270 6.3  0      18    9.7  360   840 14   7.5 180 470
email_spec6_product31_false-unreach-call_true-termination.cil.c 0 490    490    5100   300 6.2  0      25    13    280   1000 13   7.0 240 480
email_spec6_product32_false-unreach-call_true-termination.cil.c 0 490    490    5200   230 6.2  .85   26    14    470   1000 13   7.2 200 500
email_spec6_product33_false-unreach-call_true-termination.cil.c 0 490    490    6000   260 6.2  0      19    10    340   1100 12   6.3 200 490
email_spec6_product34_false-unreach-call_true-termination.cil.c 0 490    490    6300   420 6.2  0      31    17    520   1000 12   6.4 200 490
email_spec6_product35_false-unreach-call_true-termination.cil.c 0 500    500    5300   260 6.2  0      29    16    540   1600 16   8.5 160 500
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c 0 630    630    5400   1500 6.3  0      9.3  4.9  170   370 14   7.7 150 470
email_spec7_product28_false-unreach-call_true-termination.cil.c 0 480    490    5000   330 6.2  0      14    7.6  190   670 37   21   470 570
email_spec7_product29_false-unreach-call_true-termination.cil.c 0 490    490    6400   360 6.2  0      22    12    300   1000 41   23   400 590
email_spec7_product30_false-unreach-call_true-termination.cil.c 0 490    490    5200   200 6.3  0      20    10    300   770 11   6.0 120 450
email_spec7_product31_false-unreach-call_true-termination.cil.c 0 490    490    6500   140 6.2  0      21    11    390   1000 14   7.6 160 470
email_spec7_product32_false-unreach-call_true-termination.cil.c 0 490    490    5500   180 6.2  0      23    13    460   1100 12   6.3 220 480
email_spec7_product33_false-unreach-call_true-termination.cil.c 0 490    490    6900   190 6.2  0      22    11    330   1100 15   8.1 150 470
email_spec7_product34_false-unreach-call_true-termination.cil.c 0 490    490    6000   250 6.3  0      30    16    380   1600 15   7.9 170 500
email_spec7_product35_false-unreach-call_true-termination.cil.c 0 490    490    6600   230 6.2  0      31    17    460   1100 16   8.7 190 500
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c 0 640    640    6500   1600 6.3  0      12    6.3  210   380 13   6.8 210 470
email_spec8_product15_false-unreach-call_true-termination.cil.c 0 490    490    5700   190 6.2  0      19    10    300   670 14   7.3 140 440
email_spec8_product16_false-unreach-call_true-termination.cil.c 0 490    490    6000   310 6.2  0      16    8.5  310   800 11   5.9 150 460
email_spec8_product20_false-unreach-call_true-termination.cil.c 0 490    490    4800   220 6.2  0      26    14    340   960 12   6.6 140 470
email_spec8_product21_false-unreach-call_true-termination.cil.c 0 490    490    5600   240 6.2  0      30    16    310   1100 13   6.7 200 480
email_spec8_product22_false-unreach-call_true-termination.cil.c 0 490    490    6400   150 6.2  .30   22    11    350   740 12   6.3 230 450
email_spec8_product26_false-unreach-call_true-termination.cil.c 0 490    490    5100   350 6.5  0      27    14    510   980 14   7.7 150 480
email_spec8_product30_false-unreach-call_true-termination.cil.c 0 490    490    4600   200 6.2  0      23    12    320   800 12   6.6 150 450
email_spec8_product31_false-unreach-call_true-termination.cil.c 0 490    490    5400   190 6.3  0      23    12    360   810 15   7.9 180 500
email_spec8_product32_false-unreach-call_true-termination.cil.c 0 490    490    5600   450 6.3  0      31    17    410   930 12   6.7 240 490
email_spec8_product33_false-unreach-call_true-termination.cil.c 0 490    490    5800   220 6.3  0      23    12    320   1000 13   6.8 220 480
email_spec8_product34_false-unreach-call_true-termination.cil.c 0 490    490    4900   280 6.3  0      33    18    530   1000 14   7.3 220 500
email_spec8_product35_false-unreach-call_true-termination.cil.c 0 490    500    5300   250 6.3  0      32    17    500   1600 13   7.0 200 500
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c 0 620    630    6800   1600 6.3  0      12    6.3  130   390 12   6.6 200 460
email_spec9_product15_false-unreach-call_true-termination.cil.c 0 490    490    6100   210 6.2  0      17    8.9  270   670 12   6.4 190 440
email_spec9_product16_false-unreach-call_true-termination.cil.c 0 490    490    6100   200 6.2  0      19    10    330   730 12   6.6 170 460
email_spec9_product20_false-unreach-call_true-termination.cil.c 0 490    490    5500   280 6.2  0      27    14    290   1100 13   6.8 200 480
email_spec9_product21_false-unreach-call_true-termination.cil.c 0 490    490    5400   390 6.2  0      25    13    530   1100 13   7.1 130 480
email_spec9_product22_false-unreach-call_true-termination.cil.c 0 490    490    5300   230 6.2  0      27    14    230   740 12   6.3 200 460
email_spec9_product26_false-unreach-call_true-termination.cil.c 0 490    490    5800   240 6.4  0      26    14    470   1100 12   6.8 200 470
email_spec9_product30_false-unreach-call_true-termination.cil.c 0 490    490    5000   230 6.2  .13   29    15    270   830 11   6.1 160 450
email_spec9_product31_false-unreach-call_true-termination.cil.c 0 490    490    6300   160 6.3  0      25    13    340   820 16   8.4 190 490
email_spec9_product32_false-unreach-call_true-termination.cil.c 0 490    490    5700   210 6.3  0      29    16    420   1200 12   6.7 210 490
email_spec9_product33_false-unreach-call_true-termination.cil.c 0 490    490    5900   200 6.3  .30   29    15    310   800 15   8.1 170 480
email_spec9_product34_false-unreach-call_true-termination.cil.c 0 490    490    6300   370 6.3  0      37    20    410   1000 14   7.2 200 510
email_spec9_product35_false-unreach-call_true-termination.cil.c 0 490    500    5500   310 6.3  0      35    19    480   1000 12   6.6 190 480
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 620    620    6900   1500 6.3  0      10    5.2  170   400 16   8.3 180 470
email_spec0_product05_true-unreach-call_true-termination.cil.c 2 520    510    5300   650 3.5  0      14    7.5  180   500 12   6.6 190 370
email_spec0_product09_true-unreach-call_true-termination.cil.c 2 510    500    6500   1500 3.5  0      22    11    220   510 14   7.2 180 400
email_spec0_product10_true-unreach-call_true-termination.cil.c 2 520    510    5600   1400 3.5  0      14    7.3  270   480 13   7.1 230 410
email_spec0_product11_true-unreach-call_true-termination.cil.c 2 510    500    5100   1600 3.5  .0041 15    8.0  310   480 16   8.7 210 470
email_spec0_product19_true-unreach-call_true-termination.cil.c 2 520    510    6200   2700 3.5  0      20    10    410   560 18   9.3 140 590
email_spec0_product24_true-unreach-call_true-termination.cil.c 2 530    510    5500   2700 3.5  0      19    10    300   600 20   10   220 600
email_spec0_product25_true-unreach-call_true-termination.cil.c 2 530    510    6400   2800 3.6  0      26    13    380   660 23   12   320 610
email_spec0_product27_true-unreach-call_true-termination.cil.c 2 530    520    6000   2900 3.6  0      26    13    280   670 22   12   290 610
email_spec0_product36_true-unreach-call_true-termination.cil.c 2 520    510    5200   1600 3.5  .0041 21    11    310   530 13   7.0 140 430
email_spec0_product37_true-unreach-call_true-termination.cil.c 2 520    510    5900   1800 3.5  34      17    8.9  340   510 31   17   390 700
email_spec0_product38_true-unreach-call_true-termination.cil.c 2 520    510    5300   2000 3.5  .0041 20    10    350   640 17   8.8 230 490
email_spec0_product40_true-unreach-call_true-termination.cil.c 2 520    510    6300   2700 3.5  .0041 19    10    240   650 31   16   250 710
email_spec11_product03_true-unreach-call_true-termination.cil.c 2 510    510    5100   620 3.5  .30   13    6.5  280   480 13   6.6 190 360
email_spec11_product07_true-unreach-call_true-termination.cil.c 2 510    500    6400   1500 3.5  .0041 20    10    190   490 16   8.3 120 410
email_spec11_product08_true-unreach-call_true-termination.cil.c 2 510    500    5400   1600 3.5  .0041 20    10    260   520 17   9.1 230 590
email_spec11_product10_true-unreach-call_true-termination.cil.c 2 510    510    5600   1500 3.5  0      14    7.3  180   480 13   6.8 200 380
email_spec11_product18_true-unreach-call_true-termination.cil.c 2 520    510    6100   2400 3.5  34      22    11    250   520 21   11   250 590
email_spec11_product23_true-unreach-call_true-termination.cil.c 2 520    510    5700   2700 3.6  0      27    14    220   640 25   13   250 610
email_spec11_product24_true-unreach-call_true-termination.cil.c 2 530    510    5800   2800 3.6  0      19    9.6  290   610 21   11   260 600
email_spec11_product27_true-unreach-call_true-termination.cil.c 2 530    520    3000   2900 3.6  0      24    12    460   670 22   12   280 570
email_spec11_product36_true-unreach-call_true-termination.cil.c 2 520    510    5900   1600 3.5  0      19    9.7  270   520 13   7.1 240 400
email_spec11_product37_true-unreach-call_true-termination.cil.c 2 520    510    6900   1800 3.5  0      16    8.5  250   510 18   9.3 120 600
email_spec11_product39_true-unreach-call_true-termination.cil.c 2 520    510    5100   1900 3.5  0      21    11    300   610 19   9.9 310 630
email_spec11_product40_true-unreach-call_true-termination.cil.c 2 520    510    5400   2700 3.5  0      24    12    210   640 20   10   290 580
email_spec1_product12_true-unreach-call_true-termination.cil.c 2 520    500    5800   1600 3.5  0      33    18    430   800 100   61   750 6100
email_spec1_product28_true-unreach-call_true-termination.cil.c 2 520    510    5500   2500 3.6  0      34    20    490   920 180   110   3300 7000
email_spec27_product13_true-unreach-call_true-termination.cil.c 2 520    500    6000   1800 3.5  .13   29    17    480   950 210   140   2700 7000
email_spec27_product28_true-unreach-call_true-termination.cil.c 2 520    510    5100   2600 3.6  0      33    20    580   1000 170   110   1400 7000
email_spec4_product13_true-unreach-call_true-termination.cil.c 2 520    510    5900   1800 3.5  0      31    18    270   890 230   150   3100 7000
email_spec4_product17_true-unreach-call_true-termination.cil.c 2 520    510    5700   2700 3.5  0      39    24    440   1100 270   200   2900 7000
email_spec4_product28_true-unreach-call_true-termination.cil.c 2 520    510    6200   2700 3.6  0      30    18    480   940 140   89   1200 7000
email_spec4_product29_true-unreach-call_true-termination.cil.c 2 530    510    5500   2800 3.6  0      39    26    520   1400 200   130   1900 7000
email_spec7_product13_true-unreach-call_true-termination.cil.c 2 520    500    5700   1700 3.5  .0041 19    9.6  230   510 16   8.4 250 450
email_spec7_product17_true-unreach-call_true-termination.cil.c 2 520    510    5900   2500 3.6  0      24    12    330   670 17   8.9 190 470
email_spec7_product18_true-unreach-call_true-termination.cil.c 2 520    510    5000   2500 3.5  0      19    9.8  190   540 18   9.7 210 630
email_spec7_product19_true-unreach-call_true-termination.cil.c 2 520    510    6900   2700 3.5  0      21    11    240   540 17   9.1 190 440
email_spec7_product23_true-unreach-call_true-termination.cil.c 2 530    510    5700   2800 3.6  .17   27    14    360   650 20   10   260 590
email_spec7_product24_true-unreach-call_true-termination.cil.c 2 520    510    6700   2800 3.5  .0041 19    9.9  270   610 18   9.4 160 590
email_spec7_product25_true-unreach-call_true-termination.cil.c 2 530    510    5200   2800 3.6  .0041 29    15    290   660 15   8.2 220 480
email_spec7_product27_true-unreach-call_true-termination.cil.c 2 530    520    5700   2900 3.6  0      26    13    200   660 18   9.5 160 600
email_spec8_product12_true-unreach-call_true-termination.cil.c 2 520    500    6500   1600 3.5  0      29    16    590   850 110   66   1100 5500
email_spec8_product14_true-unreach-call_true-termination.cil.c 2 530    520    5900   2400 11    0      44    28    520   1100 230   150   2300 7000
email_spec8_product28_true-unreach-call_true-termination.cil.c 2 520    510    5200   2600 3.6  0      30    17    530   1000 130   80   1000 7000
email_spec8_product29_true-unreach-call_true-termination.cil.c 2 540    520    6000   2800 11    .0041 46    31    1000   1300 130   80   1400 7000
email_spec9_product12_true-unreach-call_true-termination.cil.c 2 520    500    6200   1600 3.5  0      28    16    550   880 98   58   810 5400
email_spec9_product14_true-unreach-call_true-termination.cil.c 2 530    520    5100   2400 11    0      38    24    420   1200 170   110   1500 7000
email_spec9_product28_true-unreach-call_true-termination.cil.c 2 520    510    5700   2600 3.6  0      35    20    360   890 140   89   1100 7000
email_spec9_product29_true-unreach-call_true-termination.cil.c 2 540    520    6500   2800 11    0      42    28    660   1400 140   83   1600 7000
minepump_spec1_product33_false-unreach-call_false-termination.cil.c 1 .56 .56 6.9 78 .91 0      6.1  3.3  94   290 9.2 4.9 150 330
minepump_spec1_product34_false-unreach-call_false-termination.cil.c 1 .57 .57 6.6 77 .91 0      5.7  3.1  110   300 7.3 3.9 110 320
minepump_spec1_product35_false-unreach-call_false-termination.cil.c 1 .63 .62 6.7 78 .92 .13   6.9  3.7  100   320 8.5 4.6 130 330
minepump_spec1_product36_false-unreach-call_false-termination.cil.c 1 .75 .75 8.4 79 .91 0      5.6  3.1  110   320 7.3 4.0 110 330
minepump_spec1_product37_false-unreach-call_false-termination.cil.c 1 .61 .61 8.2 78 .91 0      7.8  4.2  74   330 9.8 5.2 110 330
minepump_spec1_product38_false-unreach-call_false-termination.cil.c 1 .65 .65 8.5 78 .91 0      7.4  4.0  100   340 7.8 4.2 140 320
minepump_spec1_product39_false-unreach-call_false-termination.cil.c 1 .77 .77 8.9 79 .91 0      7.4  4.0  85   320 8.6 4.5 130 320
minepump_spec1_product40_false-unreach-call_false-termination.cil.c 1 .80 .80 9.9 79 .91 0      7.4  4.0  85   320 8.9 4.7 110 320
minepump_spec1_product41_false-unreach-call_false-termination.cil.c 1 1.3  1.3  16   78 3.5  0      8.1  4.4  92   330 10   5.5 110 320
minepump_spec1_product42_false-unreach-call_false-termination.cil.c 1 1.3  1.3  16   78 3.5  0      5.9  3.2  91   300 7.3 4.1 150 310
minepump_spec1_product43_false-unreach-call_false-termination.cil.c 1 1.5  1.5  20   79 3.5  0      6.2  3.4  93   330 7.8 4.2 150 320
minepump_spec1_product44_false-unreach-call_false-termination.cil.c 1 1.6  1.6  18   79 3.5  0      7.6  4.0  66   290 11   5.6 110 330
minepump_spec1_product49_false-unreach-call_false-termination.cil.c 1 .55 .55 7.1 78 .91 0      6.2  3.3  95   300 9.3 5.1 98 330
minepump_spec1_product50_false-unreach-call_false-termination.cil.c 1 .52 .52 6.1 78 .91 0      6.8  3.6  89   330 8.9 4.7 170 330
minepump_spec1_product51_false-unreach-call_false-termination.cil.c 1 .58 .58 7.7 78 .92 0      6.9  3.7  97   310 8.2 4.4 140 320
minepump_spec1_product52_false-unreach-call_false-termination.cil.c 1 .61 .60 7.1 79 .92 0      6.8  3.7  88   300 8.2 4.4 160 310
minepump_spec1_product53_false-unreach-call_false-termination.cil.c 1 .69 .82 6.7 110 .92 34      7.2  3.9  86   320 8.4 4.5 120 320
minepump_spec1_product54_false-unreach-call_false-termination.cil.c 1 .57 .56 6.2 79 .92 0      8.1  4.3  89   340 8.9 4.7 170 320
minepump_spec1_product55_false-unreach-call_false-termination.cil.c 1 .63 .63 7.5 80 .93 0      7.7  4.1  89   340 8.2 4.4 140 320
minepump_spec1_product56_false-unreach-call_false-termination.cil.c 1 .65 .64 6.5 80 .93 0      7.3  3.9  88   300 10   5.3 130 320
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c 0 1.5  1.5  18   88 .93 0      5.8  3.1  110   340 11   5.8 130 320
minepump_spec2_product33_false-unreach-call_false-termination.cil.c 1 1.3  1.3  16   78 3.5  0      7.9  4.3  80   300 8.0 4.3 150 320
minepump_spec2_product34_false-unreach-call_false-termination.cil.c 1 1.3  1.3  14   78 3.5  0      8.0  4.3  89   290 9.6 5.0 160 330
minepump_spec2_product35_false-unreach-call_false-termination.cil.c 1 1.5  1.5  19   79 3.5  0      7.9  4.2  87   340 8.4 4.5 140 330
minepump_spec2_product36_false-unreach-call_false-termination.cil.c 1 1.6  1.6  20   79 3.5  0      6.9  3.7  130   320 9.5 5.1 120 330
minepump_spec2_product41_false-unreach-call_false-termination.cil.c 1 2.1  2.1  26   77 6.0  0      7.9  4.3  110   330 7.4 4.0 120 330
minepump_spec2_product42_false-unreach-call_false-termination.cil.c 1 2.1  2.1  31   79 6.0  0      7.8  4.2  95   300 9.8 5.2 120 330
minepump_spec2_product43_false-unreach-call_false-termination.cil.c 1 2.2  2.2  31   78 6.0  0      8.4  4.5  94   300 9.2 4.9 81 320
minepump_spec2_product44_false-unreach-call_false-termination.cil.c 1 2.4  2.4  26   79 6.0  0      8.8  4.7  98   310 7.7 4.2 160 320
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c 0 2.8  2.8  32   87 3.7  0      7.4  3.9  75   340 8.6 4.6 180 320
minepump_spec3_product01_false-unreach-call_false-termination.cil.c 1 .51 .50 6.1 77 .91 0      7.2  4.0  79   330 8.2 4.4 150 330
minepump_spec3_product02_false-unreach-call_false-termination.cil.c 1 .52 .51 6.6 77 .91 0      7.2  3.9  86   320 9.4 5.2 130 360
minepump_spec3_product03_false-unreach-call_false-termination.cil.c 1 .54 .54 6.7 77 .91 0      6.1  3.3  110   320 8.8 4.7 170 320
minepump_spec3_product04_false-unreach-call_false-termination.cil.c 1 .72 .72 11   77 1.7  0      6.1  3.4  110   340 12   6.7 130 350
minepump_spec3_product05_false-unreach-call_false-termination.cil.c 1 .53 .53 6.0 77 .91 0      7.4  4.0  86   340 11   5.6 120 360
minepump_spec3_product06_false-unreach-call_false-termination.cil.c 1 .52 .52 5.9 77 .91 0      5.7  3.1  110   290 11   5.6 190 350
minepump_spec3_product07_false-unreach-call_false-termination.cil.c 1 .52 .52 7.6 77 .91 0      5.6  3.1  110   290 9.4 5.0 180 350
minepump_spec3_product08_false-unreach-call_false-termination.cil.c 1 .55 .54 6.1 77 .91 0      6.4  3.5  110   340 9.4 5.0 150 350
minepump_spec3_product09_false-unreach-call_false-termination.cil.c 1 .52 .51 5.4 77 .91 0      6.2  3.4  89   290 8.3 4.4 110 330
minepump_spec3_product10_false-unreach-call_false-termination.cil.c 1 .53 .52 6.2 77 .92 0      5.8  3.1  110   310 9.6 5.2 110 360
minepump_spec3_product11_false-unreach-call_false-termination.cil.c 1 .54 .54 6.5 77 .91 0      5.4  2.9  69   290 8.6 4.6 110 330
minepump_spec3_product12_false-unreach-call_false-termination.cil.c 1 .75 .75 9.3 77 1.8  0      6.0  3.2  120   340 11   5.7 160 350
minepump_spec3_product13_false-unreach-call_false-termination.cil.c 1 .52 .52 6.3 77 .91 0      7.1  3.8  81   300 9.6 5.1 140 350
minepump_spec3_product14_false-unreach-call_false-termination.cil.c 1 .50 .50 5.9 77 .91 0      5.7  3.1  120   290 9.2 4.9 170 340
minepump_spec3_product15_false-unreach-call_false-termination.cil.c 1 .55 .55 6.4 78 .91 0      6.1  3.3  110   320 8.9 4.7 160 340
minepump_spec3_product16_false-unreach-call_false-termination.cil.c 1 .58 .57 6.4 78 .91 0      7.2  3.9  96   340 9.0 4.9 180 360
minepump_spec3_product17_false-unreach-call_false-termination.cil.c 1 .53 .53 6.0 77 .91 0      5.5  3.0  110   310 12   6.3 110 360
minepump_spec3_product18_false-unreach-call_false-termination.cil.c 1 .53 .53 5.7 78 .91 .13   6.1  3.3  93   310 10   5.5 170 350
minepump_spec3_product19_false-unreach-call_false-termination.cil.c 1 .56 .55 6.6 77 .92 0      7.4  4.0  67   340 12   6.4 130 360
minepump_spec3_product20_false-unreach-call_false-termination.cil.c 1 .55 .55 6.5 77 .92 .23   7.9  4.3  72   320 11   5.9 120 350
minepump_spec3_product21_false-unreach-call_false-termination.cil.c 1 .54 .54 6.3 78 .91 0      6.3  3.4  87   330 8.9 4.8 150 360
minepump_spec3_product22_false-unreach-call_false-termination.cil.c 1 .52 .52 6.4 78 1.1  0      7.6  4.1  88   320 9.0 4.9 140 350
minepump_spec3_product23_false-unreach-call_false-termination.cil.c 1 .56 .55 6.5 78 .91 0      7.3  3.9  96   340 9.7 5.3 170 340
minepump_spec3_product24_false-unreach-call_false-termination.cil.c 1 .56 .56 6.3 79 .91 .47   5.8  3.2  120   320 11   5.9 96 350
minepump_spec3_product25_false-unreach-call_false-termination.cil.c 1 .52 .52 6.1 77 .92 0      7.2  3.9  86   320 9.8 5.2 160 350
minepump_spec3_product26_false-unreach-call_false-termination.cil.c 1 .51 .51 6.9 78 .91 0      7.2  3.9  92   290 12   6.4 100 360
minepump_spec3_product27_false-unreach-call_false-termination.cil.c 1 .57 .57 6.9 77 .91 0      5.7  3.0  110   290 11   5.7 140 340
minepump_spec3_product28_false-unreach-call_false-termination.cil.c 1 .56 .56 6.3 78 .91 0      7.1  3.8  88   330 8.4 4.6 140 340
minepump_spec3_product29_false-unreach-call_false-termination.cil.c 1 .53 .53 6.4 78 .91 0      7.2  3.9  76   290 10   5.5 130 350
minepump_spec3_product30_false-unreach-call_false-termination.cil.c 1 .52 .52 5.6 78 .91 0      8.0  4.3  94   340 9.3 5.0 140 350
minepump_spec3_product31_false-unreach-call_false-termination.cil.c 1 .58 .57 7.0 78 .91 0      5.6  3.0  100   300 8.7 4.7 130 350
minepump_spec3_product32_false-unreach-call_false-termination.cil.c 1 .60 .59 6.9 78 .91 0      7.2  3.9  94   340 11   6.0 120 360
minepump_spec3_product35_false-unreach-call_false-termination.cil.c 1 .75 .74 9.1 79 .91 0      6.3  3.4  79   290 8.4 4.5 160 320
minepump_spec3_product36_false-unreach-call_false-termination.cil.c 1 .85 .85 10   79 .91 0      6.8  3.6  99   330 8.3 4.4 120 330
minepump_spec3_product39_false-unreach-call_false-termination.cil.c 1 .85 .85 13   80 .91 0      5.6  3.0  120   290 10   5.6 110 310
minepump_spec3_product40_false-unreach-call_false-termination.cil.c 1 .76 .77 9.9 79 .91 0      6.7  3.6  100   340 10   5.5 150 330
minepump_spec3_product43_false-unreach-call_false-termination.cil.c 1 .71 .71 9.6 78 .91 0      5.7  3.1  67   320 11   5.7 100 320
minepump_spec3_product44_false-unreach-call_false-termination.cil.c 1 .75 .74 9.0 78 .91 0      6.9  3.7  100   340 10   5.4 120 330
minepump_spec3_product47_false-unreach-call_false-termination.cil.c 1 .87 .87 12   80 .92 0      6.6  3.6  85   310 8.1 4.3 94 330
minepump_spec3_product48_false-unreach-call_false-termination.cil.c 1 .75 .75 9.4 79 .92 0      6.8  3.7  110   310 12   6.1 120 330
minepump_spec3_product51_false-unreach-call_false-termination.cil.c 1 .60 .60 7.5 79 .92 0      6.2  3.3  98   320 9.7 5.3 130 330
minepump_spec3_product52_false-unreach-call_false-termination.cil.c 1 .58 .58 7.5 78 .91 0      5.9  3.2  120   290 11   5.9 140 330
minepump_spec3_product55_false-unreach-call_false-termination.cil.c 1 .67 .66 7.9 80 .92 0      6.6  3.6  81   290 11   5.8 130 320
minepump_spec3_product56_false-unreach-call_false-termination.cil.c 1 .62 .61 7.3 79 .92 0      7.1  3.8  61   290 9.2 5.0 170 340
minepump_spec3_product59_false-unreach-call_false-termination.cil.c 1 .61 .60 7.8 79 .92 0      7.4  4.0  82   320 9.5 5.0 180 330
minepump_spec3_product60_false-unreach-call_false-termination.cil.c 1 .61 .61 8.8 79 1.0  0      7.1  3.9  84   290 11   6.1 110 330
minepump_spec3_product63_false-unreach-call_false-termination.cil.c 1 .68 .68 7.6 81 .92 0      6.6  3.6  90   290 8.7 4.7 130 330
minepump_spec3_product64_false-unreach-call_false-termination.cil.c 1 .66 .65 7.8 81 .92 0      6.2  3.4  88   290 10   5.4 110 330
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c 1 1.6  1.6  18   88 .93 0      6.5  3.5  75   290 11   5.9 190 360
minepump_spec4_product33_false-unreach-call_false-termination.cil.c 1 2.0  2.0  26   78 6.0  0      8.0  4.3  85   290 14   7.4 100 350
minepump_spec4_product34_false-unreach-call_false-termination.cil.c 1 2.0  2.0  24   77 6.0  0      8.4  4.5  91   290 10   5.3 100 320
minepump_spec4_product35_false-unreach-call_false-termination.cil.c 1 2.1  2.1  33   78 6.0  .13   7.9  4.2  85   290 7.3 4.0 79 320
minepump_spec4_product36_false-unreach-call_false-termination.cil.c 1 2.1  2.1  26   78 6.0  0      7.1  3.8  110   290 7.7 4.2 160 310
minepump_spec4_product37_false-unreach-call_false-termination.cil.c 1 2.2  2.2  32   79 6.0  .13   7.8  4.2  110   330 9.5 5.1 87 310
minepump_spec4_product38_false-unreach-call_false-termination.cil.c 1 2.2  2.2  27   79 6.0  0      8.1  4.3  110   340 9.8 5.2 120 320
minepump_spec4_product39_false-unreach-call_false-termination.cil.c 1 2.4  2.4  34   79 6.0  .13   7.0  3.7  150   310 8.1 4.4 94 310
minepump_spec4_product40_false-unreach-call_false-termination.cil.c 1 2.3  2.3  29   79 6.0  0      8.8  4.7  96   300 9.0 4.9 80 310
minepump_spec4_product41_false-unreach-call_false-termination.cil.c 1 2.0  2.0  29   77 6.0  0      7.3  3.9  110   300 8.0 4.3 130 330
minepump_spec4_product42_false-unreach-call_false-termination.cil.c 1 2.1  2.1  27   78 6.0  0      7.7  4.2  110   350 7.6 4.1 140 320
minepump_spec4_product43_false-unreach-call_false-termination.cil.c 1 2.2  2.2  33   78 6.0  0      7.8  4.2  100   320 7.9 4.3 160 320
minepump_spec4_product44_false-unreach-call_false-termination.cil.c 1 2.3  2.3  31   78 6.0  0      6.9  3.7  110   350 8.9 4.8 150 340
minepump_spec4_product45_false-unreach-call_false-termination.cil.c 1 2.2  2.2  24   79 6.0  0      7.1  3.8  150   330 8.7 4.6 150 320
minepump_spec4_product46_false-unreach-call_false-termination.cil.c 1 2.2  2.2  29   80 6.0  .58   7.6  4.1  130   330 9.1 4.9 120 320
minepump_spec4_product47_false-unreach-call_false-termination.cil.c 1 2.4  2.4  37   79 6.0  0      6.9  3.7  150   300 8.4 4.5 110 320
minepump_spec4_product48_false-unreach-call_false-termination.cil.c 1 2.3  2.2  31   79 6.0  0      7.8  4.1  140   340 8.7 4.7 95 320
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c 0 3.7  3.7  52   87 6.1  0      6.9  3.7  63   290 9.9 5.3 130 320
minepump_spec1_product01_true-unreach-call_false-termination.cil.c 2 5.2  2.5  48   280 3.4  0      370    360    8500   7000 10   5.7 150 360
minepump_spec1_product02_true-unreach-call_false-termination.cil.c 2 5.3  2.5  41   270 3.4  0      310    290    5300   7000 14   7.8 73 360
minepump_spec1_product03_true-unreach-call_false-termination.cil.c 0 420    420    5100   160 260    0      .66 .42 7.4 39 5.9 3.1 68 300
minepump_spec1_product04_true-unreach-call_false-termination.cil.c 0 430    430    5900   160 260    .13   .49 .32 12   40 5.5 2.9 40 300
minepump_spec1_product05_true-unreach-call_false-termination.cil.c 2 5.3  2.5  47   280 3.4  0      310    300    3400   7000 10   5.4 74 360
minepump_spec1_product06_true-unreach-call_false-termination.cil.c 0 400    400    4800   150 260    0      .66 .43 7.1 42 5.6 3.0 83 300
minepump_spec1_product07_true-unreach-call_false-termination.cil.c 0 520    510    6500   180 260    0      .54 .34 11   40 5.9 3.1 93 300
minepump_spec1_product08_true-unreach-call_false-termination.cil.c 0 490    490    5800   180 260    0      .65 .41 9.1 39 6.5 3.4 100 300
minepump_spec1_product09_true-unreach-call_false-termination.cil.c 2 5.2  2.5  47   280 3.4  0      340    330    7100   7000 11   5.9 180 370
minepump_spec1_product10_true-unreach-call_false-termination.cil.c 2 5.3  2.5  46   280 3.4  0      380    360    4100   7000 12   6.5 210 370
minepump_spec1_product11_true-unreach-call_false-termination.cil.c 0 420    420    5900   160 260    0      .52 .33 11   41 5.6 3.0 71 310
minepump_spec1_product12_true-unreach-call_false-termination.cil.c 0 440    430    5500   170 260    0      .63 .40 6.7 39 6.0 3.2 97 300
minepump_spec1_product13_true-unreach-call_false-termination.cil.c 2 5.4  2.5  46   280 3.4  0      380    360    5900   7000 9.9 5.4 170 360
minepump_spec1_product14_true-unreach-call_false-termination.cil.c 0 400    400    5400   150 260    0      .53 .35 11   42 5.6 3.0 72 300
minepump_spec1_product15_true-unreach-call_false-termination.cil.c 0 510    510    6600   180 260    .0041 .52 .34 14   40 6.4 3.4 120 300
minepump_spec1_product16_true-unreach-call_false-termination.cil.c 0 490    490    6200   180 260    0      .62 .40 9.0 40 5.8 3.1 120 300
minepump_spec1_product17_true-unreach-call_false-termination.cil.c 0 250    250    3200   130 260    .0041 .63 .38 8.3 40 5.8 3.0 96 300
minepump_spec1_product18_true-unreach-call_false-termination.cil.c 0 410    410    5300   160 260    0      .64 .43 7.9 39 6.9 3.6 91 320
minepump_spec1_product19_true-unreach-call_false-termination.cil.c 0 460    460    5300   190 260    0      .47 .31 8.5 40 6.0 3.2 88 300
minepump_spec1_product20_true-unreach-call_false-termination.cil.c 0 480    480    5300   190 260    0      .53 .35 13   42 5.7 3.0 73 300
minepump_spec1_product21_true-unreach-call_false-termination.cil.c 2 5.4  2.6  47   280 3.4  0      450    430    8400   7000 11   5.6 130 370
minepump_spec1_product22_true-unreach-call_false-termination.cil.c 0 440    440    5700   210 260    0      .63 .41 7.7 40 5.8 3.1 110 300
minepump_spec1_product23_true-unreach-call_false-termination.cil.c 0 630    630    9500   240 260    0      .53 .33 10   42 6.2 3.3 120 290
minepump_spec1_product24_true-unreach-call_false-termination.cil.c 0 550    550    6800   240 260    0      .53 .35 13   40 6.6 3.5 93 310
minepump_spec1_product25_true-unreach-call_false-termination.cil.c 0 260    260    3200   130 260    0      .50 .31 9.5 39 5.7 3.0 69 300
minepump_spec1_product26_true-unreach-call_false-termination.cil.c 0 410    410    5800   160 260    0      .61 .39 8.0 39 5.8 3.1 90 290
minepump_spec1_product27_true-unreach-call_false-termination.cil.c 0 460    460    6200   190 260    0      .64 .41 8.9 44 5.4 2.9 88 300
minepump_spec1_product28_true-unreach-call_false-termination.cil.c 0 470    470    5700   200 260    0      .67 .44 7.2 39 5.6 3.1 64 300
minepump_spec1_product29_true-unreach-call_false-termination.cil.c 2 5.6  2.7  52   280 3.4  0      350    340    7100   7000 13   7.1 110 360
minepump_spec1_product30_true-unreach-call_false-termination.cil.c 0 460    460    6100   240 260    34      .64 .40 6.5 39 5.9 3.1 95 300
minepump_spec1_product31_true-unreach-call_false-termination.cil.c 0 620    620    8100   240 260    0      .49 .32 11   40 6.5 3.4 52 320
minepump_spec1_product32_true-unreach-call_false-termination.cil.c 0 560    560    7000   250 260    0      .63 .40 8.4 41 5.6 3.0 80 300
minepump_spec1_product45_true-unreach-call_false-termination.cil.c 2 8.2  3.6  78   330 3.4  0      290    270    4800   7000 20   11   260 560
minepump_spec1_product46_true-unreach-call_false-termination.cil.c 0 900    900    11000   230 240    0      .65 .41 7.1 40 6.1 3.2 87 300
minepump_spec1_product47_true-unreach-call_false-termination.cil.c 0 900    900    12000   220 220    .13   .64 .40 7.6 43 5.2 2.8 69 280
minepump_spec1_product48_true-unreach-call_false-termination.cil.c 0 900    900    11000   240 220    0      .57 .35 9.0 39 5.8 3.1 49 300
minepump_spec1_product57_true-unreach-call_false-termination.cil.c 0 900    900    12000   170 210    0      .51 .32 14   40 5.4 2.9 81 290
minepump_spec1_product58_true-unreach-call_false-termination.cil.c 0 900    900    12000   180 200    0      .49 .32 14   39 6.0 3.1 110 300
minepump_spec1_product59_true-unreach-call_false-termination.cil.c 0 900    900    7000   160 170    0      .60 .38 8.3 40 5.7 3.0 89 290
minepump_spec1_product60_true-unreach-call_false-termination.cil.c 0 900    900    11000   200 190    .13   .52 .34 12   40 6.3 3.4 72 300
minepump_spec1_product61_true-unreach-call_false-termination.cil.c 2 6.9  3.6  63   290 3.5  0      310    290    11000   7000 27   15   310 670
minepump_spec1_product62_true-unreach-call_false-termination.cil.c 0 900    900    11000   290 210    0      .53 .34 13   40 7.1 3.8 45 300
minepump_spec1_product63_true-unreach-call_false-termination.cil.c 0 900    900    12000   290 190    0      .60 .38 9.2 40 7.6 4.0 66 300
minepump_spec1_product64_true-unreach-call_false-termination.cil.c 0 900    900    11000   290 190    0      .56 .36 9.0 40 5.2 2.8 67 290
minepump_spec2_product01_true-unreach-call_false-termination.cil.c 2 5.3  2.5  50   280 3.4  0      910    880    15000   6400 13   7.1 160 480
minepump_spec2_product02_true-unreach-call_false-termination.cil.c 2 5.6  2.7  50   280 4.3  0      880    850    15000   7000 14   7.6 240 490
minepump_spec2_product03_true-unreach-call_false-termination.cil.c 0 430    430    5500   170 260    0      .54 .34 14   42 5.6 3.0 72 300
minepump_spec2_product04_true-unreach-call_false-termination.cil.c 0 430    430    5800   180 260    0      .52 .32 10   40 5.8 3.1 94 300
minepump_spec2_product05_true-unreach-call_false-termination.cil.c 2 5.4  2.5  48   280 3.4  0      300    290    4100   7000 10   5.6 150 370
minepump_spec2_product06_true-unreach-call_false-termination.cil.c 0 420    410    5400   160 260    0      .50 .32 12   40 6.5 3.4 99 310
minepump_spec2_product07_true-unreach-call_false-termination.cil.c 0 530    530    7500   190 260    .13   .46 .31 5.5 40 5.9 3.1 86 300
minepump_spec2_product08_true-unreach-call_false-termination.cil.c 0 490    490    6100   190 260    0      .64 .41 7.8 40 5.8 3.1 84 280
minepump_spec2_product09_true-unreach-call_false-termination.cil.c 2 5.2  2.5  47   270 3.4  .0041 910    890    18000   6800 13   7.3 220 490
minepump_spec2_product10_true-unreach-call_false-termination.cil.c 2 5.3  2.5  49   280 3.4  0      740    720    18000   7000 19   10   160 490
minepump_spec2_product11_true-unreach-call_false-termination.cil.c 0 430    430    4900   170 260    0      .52 .34 13   43 5.7 3.1 70 300
minepump_spec2_product12_true-unreach-call_false-termination.cil.c 0 420    420    5000   170 260    0      .58 .37 8.0 39 6.0 3.2 120 280
minepump_spec2_product13_true-unreach-call_false-termination.cil.c 2 5.4  2.6  43   280 3.4  .23   320    300    5400   7000 9.8 5.3 120 350
minepump_spec2_product14_true-unreach-call_false-termination.cil.c 0 420    420    4800   170 260    0      .50 .32 13   40 5.5 2.9 65 300
minepump_spec2_product15_true-unreach-call_false-termination.cil.c 0 530    530    5700   190 260    0      .63 .39 7.3 42 6.0 3.2 130 300
minepump_spec2_product16_true-unreach-call_false-termination.cil.c 0 490    490    6900   190 260    0      .49 .32 10   39 5.7 3.1 92 300
minepump_spec2_product17_true-unreach-call_false-termination.cil.c 0 270    270    2900   150 260    0      .50 .34 14   40 5.8 3.1 66 310
minepump_spec2_product18_true-unreach-call_false-termination.cil.c 0 420    420    5300   170 260    0      .53 .34 11   40 6.7 3.5 100 310
minepump_spec2_product19_true-unreach-call_false-termination.cil.c 0 480    480    5700   200 260    0      .51 .32 11   40 6.5 3.5 110 310
minepump_spec2_product20_true-unreach-call_false-termination.cil.c 0 460    460    6500   200 260    0      .52 .35 13   40 6.0 3.2 88 300
minepump_spec2_product21_true-unreach-call_false-termination.cil.c 2 5.4  2.6  57   280 3.4  0      330    310    6000   7000 11   5.7 120 360
minepump_spec2_product22_true-unreach-call_false-termination.cil.c 0 490    490    6900   220 260    0      .65 .41 8.0 39 6.8 3.5 150 310
minepump_spec2_product23_true-unreach-call_false-termination.cil.c 0 640    640    7900   250 260    0      .62 .39 9.2 40 6.0 3.2 73 310
minepump_spec2_product24_true-unreach-call_false-termination.cil.c 0 560    560    7700   260 270    0      .56 .35 12   40 5.6 3.0 62 300
minepump_spec2_product25_true-unreach-call_false-termination.cil.c 0 260    260    3400   150 260    0      .61 .38 9.6 40 6.0 3.2 86 300
minepump_spec2_product26_true-unreach-call_false-termination.cil.c 0 450    450    6200   180 260    0      .58 .37 16   42 5.7 3.0 86 300
minepump_spec2_product27_true-unreach-call_false-termination.cil.c 0 460    460    5600   200 260    0      .53 .35 7.9 39 6.6 3.5 81 310
minepump_spec2_product28_true-unreach-call_false-termination.cil.c 0 470    470    5700   210 260    0      .65 .42 9.2 39 5.5 2.9 68 300
minepump_spec2_product29_true-unreach-call_false-termination.cil.c 2 5.4  2.6  52   280 3.4  0      440    430    10000   7000 10   5.5 170 360
minepump_spec2_product30_true-unreach-call_false-termination.cil.c 0 480    480    6000   250 260    34      .62 .38 9.2 40 6.4 3.4 110 310
minepump_spec2_product31_true-unreach-call_false-termination.cil.c 0 650    640    8000   260 260    0      .61 .38 8.0 40 6.2 3.3 120 310
minepump_spec2_product32_true-unreach-call_false-termination.cil.c 0 560    560    7400   260 260    0      .53 .33 11   43 5.9 3.1 87 290
minepump_spec2_product37_true-unreach-call_false-termination.cil.c 0 810    810    11000   200 260    0      .69 .44 8.4 42 6.1 3.3 100 300
minepump_spec2_product38_true-unreach-call_false-termination.cil.c 0 900    900    10000   230 250    0      .56 .34 10   42 6.4 3.3 72 310
minepump_spec2_product39_true-unreach-call_false-termination.cil.c 0 900    900    13000   220 220    0      .59 .38 8.9 41 5.9 3.1 69 300
minepump_spec2_product40_true-unreach-call_false-termination.cil.c 0 900    900    10000   230 230    0      .53 .33 11   41 5.6 3.0 85 300
minepump_spec2_product45_true-unreach-call_false-termination.cil.c 2 7.6  3.5  74   320 3.4  0      360    340    5000   7000 23   13   320 640
minepump_spec2_product46_true-unreach-call_false-termination.cil.c 0 900    900    11000   240 250    .30   .57 .37 10   41 5.6 3.0 67 300
minepump_spec2_product47_true-unreach-call_false-termination.cil.c 0 900    900    13000   240 220    0      .54 .35 8.6 39 6.3 3.3 96 300
minepump_spec2_product48_true-unreach-call_false-termination.cil.c 0 900    900    11000   250 230    0      .62 .39 7.5 39 5.5 2.9 77 290
minepump_spec2_product49_true-unreach-call_false-termination.cil.c 0 900    900    11000   170 220    .13   .60 .38 8.7 40 5.6 3.0 66 300
minepump_spec2_product50_true-unreach-call_false-termination.cil.c 0 900    900    12000   190 210    0      .64 .41 8.5 39 5.7 3.0 97 300
minepump_spec2_product51_true-unreach-call_false-termination.cil.c 0 900    900    11000   200 200    0      .67 .42 9.0 41 6.0 3.1 95 300
minepump_spec2_product52_true-unreach-call_false-termination.cil.c 0 900    900    11000   200 200    0      .51 .33 10   39 5.8 3.1 110 300
minepump_spec2_product53_true-unreach-call_false-termination.cil.c 0 900    900    13000   270 230    0      .56 .36 9.8 40 8.5 4.4 95 330
minepump_spec2_product54_true-unreach-call_false-termination.cil.c 0 900    900    13000   290 220    .13   .63 .40 8.4 39 7.2 3.8 64 300
minepump_spec2_product55_true-unreach-call_false-termination.cil.c 0 900    900    11000   290 220    0      .62 .40 9.6 41 6.0 3.1 100 290
minepump_spec2_product56_true-unreach-call_false-termination.cil.c 0 900    900    11000   290 200    0      .55 .34 12   39 6.4 3.4 110 300
minepump_spec2_product57_true-unreach-call_false-termination.cil.c 0 900    900    12000   180 220    0      .64 .40 11   42 6.3 3.3 110 300
minepump_spec2_product58_true-unreach-call_false-termination.cil.c 0 900    900    11000   200 210    0      .56 .37 10   40 5.7 3.1 64 300
minepump_spec2_product59_true-unreach-call_false-termination.cil.c 0 900    900    12000   220 200    0      .53 .33 12   39 7.3 3.8 57 320
minepump_spec2_product60_true-unreach-call_false-termination.cil.c 0 900    900    12000   210 200    .13   .49 .31 12   39 5.9 3.1 79 300
minepump_spec2_product61_true-unreach-call_false-termination.cil.c 2 7.0  3.7  72   290 3.5  .0041 360    340    8100   7000 22   12   260 610
minepump_spec2_product62_true-unreach-call_false-termination.cil.c 0 900    900    11000   310 210    .39   .55 .35 11   40 7.0 3.7 61 300
minepump_spec2_product63_true-unreach-call_false-termination.cil.c 0 900    900    9800   300 190    0      .64 .42 7.7 40 5.7 3.0 89 290
minepump_spec2_product64_true-unreach-call_false-termination.cil.c 0 900    900    13000   320 200    .13   .51 .32 11   40 5.9 3.1 73 300
minepump_spec3_product33_true-unreach-call_false-termination.cil.c 2 7.2  3.2  63   320 3.6  0      310    300    5000   7000 13   7.0 100 460
minepump_spec3_product34_true-unreach-call_false-termination.cil.c 0 690    680    8500   190 260    0      .58 .37 10   40 6.3 3.3 110 300
minepump_spec3_product37_true-unreach-call_false-termination.cil.c 2 8.0  3.6  64   330 3.4  .0041 340    320    8100   7000 21   12   270 580
minepump_spec3_product38_true-unreach-call_false-termination.cil.c 0 900    900    11000   220 250    0      .55 .34 11   40 6.9 3.6 78 310
minepump_spec3_product41_true-unreach-call_false-termination.cil.c 2 7.5  3.4  58   330 3.4  0      360    350    4700   7000 15   8.0 230 520
minepump_spec3_product42_true-unreach-call_false-termination.cil.c 0 830    830    9700   200 260    0      .56 .37 8.7 40 5.9 3.1 88 300
minepump_spec3_product45_true-unreach-call_false-termination.cil.c 2 7.9  3.6  68   330 3.4  0      300    290    6300   7000 23   13   390 570
minepump_spec3_product46_true-unreach-call_false-termination.cil.c 0 900    900    13000   230 240    0      .58 .37 11   46 6.1 3.2 120 300
minepump_spec3_product49_true-unreach-call_false-termination.cil.c 0 900    900    12000   120 160    0      .66 .43 8.4 41 5.5 2.9 61 300
minepump_spec3_product50_true-unreach-call_false-termination.cil.c 0 900    900    13000   130 160    0      .53 .34 11   41 6.2 3.3 120 300
minepump_spec3_product53_true-unreach-call_false-termination.cil.c 0 900    900    13000   150 160    0      .59 .36 7.8 39 5.2 2.8 72 290
minepump_spec3_product54_true-unreach-call_false-termination.cil.c 0 900    900    11000   180 160    0      .59 .36 9.8 39 5.5 2.9 76 290
minepump_spec3_product57_true-unreach-call_false-termination.cil.c 0 900    900    13000   110 140    0      .55 .36 10   42 6.4 3.3 98 300
minepump_spec3_product58_true-unreach-call_false-termination.cil.c 0 900    900    12000   120 140    0      .53 .34 11   39 5.7 3.0 80 300
minepump_spec3_product61_true-unreach-call_false-termination.cil.c 0 900    900    11000   150 140    0      .53 .33 13   40 6.8 3.5 75 310
minepump_spec3_product62_true-unreach-call_false-termination.cil.c 0 900    900    12000   170 140    0      .58 .37 11   40 5.6 3.0 44 300
minepump_spec4_product01_true-unreach-call_false-termination.cil.c 2 5.0  2.5  52   270 3.4  0      390    370    5700   7000 9.4 5.1 89 350
minepump_spec4_product02_true-unreach-call_false-termination.cil.c 2 5.1  2.5  42   270 3.4  0      320    310    5100   7000 10   5.4 200 350
minepump_spec4_product03_true-unreach-call_false-termination.cil.c 0 430    430    5500   160 260    0      .63 .40 8.3 40 5.9 3.1 77 300
minepump_spec4_product04_true-unreach-call_false-termination.cil.c 0 440    430    5100   160 260    0      .59 .38 11   42 5.6 3.0 70 290
minepump_spec4_product05_true-unreach-call_false-termination.cil.c 0 370    370    5100   130 260    0      .57 .35 8.8 40 6.0 3.2 110 300
minepump_spec4_product06_true-unreach-call_false-termination.cil.c 0 420    420    5300   150 260    .13   .61 .39 11   45 5.5 2.9 89 300
minepump_spec4_product07_true-unreach-call_false-termination.cil.c 0 540    540    6100   180 260    0      .49 .32 9.5 41 6.0 3.2 98 310
minepump_spec4_product08_true-unreach-call_false-termination.cil.c 0 540    540    6400   180 260    .13   .56 .35 11   42 5.9 3.1 79 300
minepump_spec4_product09_true-unreach-call_false-termination.cil.c 2 5.4  2.7  48   280 4.3  0      310    300    7100   7000 9.1 4.9 67 350
minepump_spec4_product10_true-unreach-call_false-termination.cil.c 0 140    140    1800   110 170    35      .63 .41 8.9 40 6.4 3.4 130 310
minepump_spec4_product11_true-unreach-call_false-termination.cil.c 0 430    430    6000   150 260    0      .50 .32 10   39 6.5 3.4 72 290
minepump_spec4_product12_true-unreach-call_false-termination.cil.c 0 580    580    7800   300 260    0      .48 .30 9.9 39 5.7 3.0 67 300
minepump_spec4_product13_true-unreach-call_false-termination.cil.c 0 370    370    4800   130 260    0      .63 .40 8.5 40 6.2 3.3 98 320
minepump_spec4_product14_true-unreach-call_false-termination.cil.c 0 420    420    5200   150 260    0      .51 .32 11   40 5.8 3.1 81 300
minepump_spec4_product15_true-unreach-call_false-termination.cil.c 0 540    540    6900   180 260    0      .66 .42 7.8 41 6.4 3.4 100 310
minepump_spec4_product16_true-unreach-call_false-termination.cil.c 0 540    540    6400   190 260    0      .65 .40 6.2 39 5.5 2.9 58 290
minepump_spec4_product17_true-unreach-call_false-termination.cil.c 0 270    270    3200   130 260    .0041 .52 .33 13   41 5.5 2.9 60 300
minepump_spec4_product18_true-unreach-call_false-termination.cil.c 0 450    450    5800   160 260    0      .66 .42 8.0 41 6.7 3.6 75 300
minepump_spec4_product19_true-unreach-call_false-termination.cil.c 0 460    460    5700   190 260    0      .65 .41 8.9 42 7.5 3.9 67 300
minepump_spec4_product20_true-unreach-call_false-termination.cil.c 0 450    450    5600   220 260    34      .53 .33 13   41 5.7 3.1 100 300
minepump_spec4_product21_true-unreach-call_false-termination.cil.c 0 270    260    3300   170 260    0      .61 .40 9.0 40 5.7 3.1 70 300
minepump_spec4_product22_true-unreach-call_false-termination.cil.c 0 470    470    5700   210 260    0      .55 .34 10   40 7.8 4.1 84 310
minepump_spec4_product23_true-unreach-call_false-termination.cil.c 0 520    520    5900   240 260    0      .52 .34 8.5 39 5.7 3.0 64 300
minepump_spec4_product24_true-unreach-call_false-termination.cil.c 0 550    540    6000   240 260    0      .49 .32 10   39 5.9 3.2 66 310
minepump_spec4_product25_true-unreach-call_false-termination.cil.c 0 240    240    3000   140 260    0      .50 .32 11   39 5.7 3.0 92 290
minepump_spec4_product26_true-unreach-call_false-termination.cil.c 0 460    460    6400   170 260    0      .63 .40 6.6 39 5.9 3.1 86 290
minepump_spec4_product27_true-unreach-call_false-termination.cil.c 0 460    460    6500   190 260    0      .52 .33 12   40 6.0 3.2 68 300
minepump_spec4_product28_true-unreach-call_false-termination.cil.c 0 450    450    5500   190 260    0      .50 .33 11   40 5.8 3.1 120 290
minepump_spec4_product29_true-unreach-call_false-termination.cil.c 0 270    260    3100   170 260    .39   .59 .37 12   41 5.2 2.8 78 290
minepump_spec4_product30_true-unreach-call_false-termination.cil.c 0 450    450    5100   210 260    0      .50 .33 12   40 6.4 3.4 93 300
minepump_spec4_product31_true-unreach-call_false-termination.cil.c 0 530    530    6700   240 260    0      .54 .35 12   42 5.7 3.1 70 300
minepump_spec4_product32_true-unreach-call_false-termination.cil.c 0 560    560    7300   240 260    0      .48 .32 8.5 40 6.6 3.5 60 310
minepump_spec4_product49_true-unreach-call_false-termination.cil.c 0 900    900    11000   170 230    0      .69 .44 8.5 40 5.9 3.1 86 300
minepump_spec4_product50_true-unreach-call_false-termination.cil.c 0 900    900    11000   190 220    0      .61 .40 7.7 40 5.2 2.8 56 280
minepump_spec4_product51_true-unreach-call_false-termination.cil.c 0 900    900    11000   210 230    0      .62 .38 8.2 39 6.6 3.5 90 330
minepump_spec4_product52_true-unreach-call_false-termination.cil.c 0 900    900    12000   190 200    0      .55 .34 13   43 5.7 3.0 90 290
minepump_spec4_product53_true-unreach-call_false-termination.cil.c 0 900    900    11000   230 220    0      .64 .39 7.7 39 5.7 3.0 59 300
minepump_spec4_product54_true-unreach-call_false-termination.cil.c 0 900    900    12000   250 210    0      .64 .41 8.2 41 6.4 3.4 100 300
minepump_spec4_product55_true-unreach-call_false-termination.cil.c 0 900    900    11000   270 200    0      .64 .41 7.5 40 5.4 2.8 52 300
minepump_spec4_product56_true-unreach-call_false-termination.cil.c 0 900    900    12000   250 190    0      .61 .38 8.6 39 5.8 3.1 79 290
minepump_spec4_product57_true-unreach-call_false-termination.cil.c 0 900    900    9900   180 220    0      .53 .34 12   41 6.0 3.2 91 290
minepump_spec4_product58_true-unreach-call_false-termination.cil.c 0 900    900    9900   190 210    0      .63 .40 6.4 41 5.7 3.1 82 310
minepump_spec4_product59_true-unreach-call_false-termination.cil.c 0 900    900    10000   210 200    0      .52 .33 11   40 6.7 3.5 93 290
minepump_spec4_product60_true-unreach-call_false-termination.cil.c 0 900    900    13000   200 190    0      .50 .33 11   42 6.1 3.2 110 300
minepump_spec4_product61_true-unreach-call_false-termination.cil.c 0 900    900    11000   250 210    0      .50 .32 14   39 5.4 2.9 83 290
minepump_spec4_product62_true-unreach-call_false-termination.cil.c 0 900    900    12000   260 200    0      .51 .33 13   41 6.4 3.3 130 310
minepump_spec4_product63_true-unreach-call_false-termination.cil.c 0 900    900    11000   280 190    0      .51 .34 9.5 40 6.4 3.4 78 330
minepump_spec4_product64_true-unreach-call_false-termination.cil.c 0 900    900    11000   260 180    0      .60 .39 9.1 40 5.9 3.1 69 300
minepump_spec5_product01_true-unreach-call_false-termination.cil.c 0 130    130    1700   77 170    0      .65 .40 9.0 39 6.8 3.6 110 320
minepump_spec5_product02_true-unreach-call_false-termination.cil.c 2 5.3  2.5  52   270 3.4  0      8.2  4.4  160   330 11   5.9 210 350
minepump_spec5_product03_true-unreach-call_false-termination.cil.c 2 6.2  2.8  54   290 3.4  0      9.5  5.1  110   310 9.9 5.3 190 350
minepump_spec5_product04_true-unreach-call_false-termination.cil.c 0 160    160    1900   99 170    0      .67 .43 7.8 44 5.9 3.1 74 300
minepump_spec5_product05_true-unreach-call_false-termination.cil.c 2 5.6  2.8  48   320 3.4  34      9.9  5.2  160   350 10   5.6 180 370
minepump_spec5_product06_true-unreach-call_false-termination.cil.c 2 5.3  2.6  49   280 3.4  0      8.0  4.2  87   340 11   5.8 170 360
minepump_spec5_product07_true-unreach-call_false-termination.cil.c 2 6.2  2.8  60   300 3.4  .47   9.0  4.7  120   340 10   5.6 130 360
minepump_spec5_product08_true-unreach-call_false-termination.cil.c 2 5.8  2.7  48   290 3.4  0      9.9  5.2  110   340 10   5.4 140 360
minepump_spec5_product09_true-unreach-call_false-termination.cil.c 2 5.2  2.5  53   280 3.4  0      9.4  5.0  120   310 10   5.6 160 360
minepump_spec5_product10_true-unreach-call_false-termination.cil.c 2 5.6  2.8  49   280 4.3  0      8.6  4.6  120   330 10   5.6 76 360
minepump_spec5_product11_true-unreach-call_false-termination.cil.c 2 6.0  2.7  53   290 3.4  0      9.4  4.9  120   340 9.4 5.1 120 340
minepump_spec5_product12_true-unreach-call_false-termination.cil.c 0 160    160    2200   99 170    0      .58 .37 11   40 5.6 3.0 91 290
minepump_spec5_product13_true-unreach-call_false-termination.cil.c 2 5.4  2.6  46   280 3.4  0      8.5  4.5  93   340 9.9 5.4 120 350
minepump_spec5_product14_true-unreach-call_false-termination.cil.c 2 5.5  2.6  46   280 3.4  0      10    5.4  140   380 11   6.0 130 370
minepump_spec5_product15_true-unreach-call_false-termination.cil.c 2 6.0  2.8  57   300 3.4  .23   9.0  4.7  150   330 13   7.0 130 380
minepump_spec5_product16_true-unreach-call_false-termination.cil.c 2 5.9  2.8  51   280 3.4  .0041 12    6.1  130   370 9.7 5.2 120 350
minepump_spec5_product17_true-unreach-call_false-termination.cil.c 2 5.4  2.6  48   290 3.4  0      9.8  5.2  150   360 9.9 5.3 100 350
minepump_spec5_product18_true-unreach-call_false-termination.cil.c 2 5.6  2.6  53   280 3.4  0      8.7  4.6  150   350 11   5.9 170 380
minepump_spec5_product19_true-unreach-call_false-termination.cil.c 2 6.1  2.8  58   290 3.4  0      9.4  5.0  120   340 11   6.0 190 370
minepump_spec5_product20_true-unreach-call_false-termination.cil.c 2 5.8  2.7  56   280 3.4  0      11    5.7  140   350 9.5 5.1 120 350
minepump_spec5_product21_true-unreach-call_false-termination.cil.c 2 6.0  2.8  51   290 3.4  .14   10    5.2  95   400 10   5.5 120 360
minepump_spec5_product22_true-unreach-call_false-termination.cil.c 2 5.6  2.7  56   280 3.4  0      13    6.6  170   430 10   5.7 190 360
minepump_spec5_product23_true-unreach-call_false-termination.cil.c 2 6.6  3.0  55   300 3.4  .30   12    6.2  93   420 13   7.2 120 360
minepump_spec5_product24_true-unreach-call_false-termination.cil.c 2 5.8  2.8  47   290 3.4  0      13    6.7  140   430 9.4 5.1 92 340
minepump_spec5_product25_true-unreach-call_false-termination.cil.c 2 5.7  2.6  49   280 3.4  .0041 9.9  5.2  210   380 10   5.5 190 360
minepump_spec5_product26_true-unreach-call_false-termination.cil.c 2 5.5  2.6  47   280 3.4  0      10    5.5  150   350 10   5.5 170 370
minepump_spec5_product27_true-unreach-call_false-termination.cil.c 2 6.0  2.8  61   290 3.4  0      12    6.2  120   360 11   6.2 120 350
minepump_spec5_product28_true-unreach-call_false-termination.cil.c 2 5.9  2.7  52   280 3.4  0      11    5.8  90   370 9.5 5.1 170 350
minepump_spec5_product29_true-unreach-call_false-termination.cil.c 2 5.6  2.6  55   280 3.4  0      10    5.5  210   410 10   5.6 100 360
minepump_spec5_product30_true-unreach-call_false-termination.cil.c 2 5.7  2.7  47   290 3.4  0      12    6.4  87   390 11   5.8 200 360
minepump_spec5_product31_true-unreach-call_false-termination.cil.c 2 6.6  3.0  49   290 3.4  0      11    6.0  160   390 11   5.8 130 360
minepump_spec5_product32_true-unreach-call_false-termination.cil.c 2 5.9  2.8  51   290 3.4  .13   10    5.3  140   390 9.6 5.2 110 350
minepump_spec5_product33_true-unreach-call_false-termination.cil.c 0 890    890    11000   150 260    0      .58 .37 11   44 5.5 2.9 91 290
minepump_spec5_product34_true-unreach-call_false-termination.cil.c 0 770    770    9100   190 260    0      .54 .35 11   41 7.8 4.1 78 310
minepump_spec5_product35_true-unreach-call_false-termination.cil.c 0 900    900    11000   180 230    0      .58 .38 8.1 39 6.0 3.2 110 300
minepump_spec5_product36_true-unreach-call_false-termination.cil.c 0 900    900    12000   110 160    0      .62 .38 9.3 42 6.0 3.2 100 300
minepump_spec5_product37_true-unreach-call_false-termination.cil.c 0 900    900    11000   160 170    34      .54 .35 7.4 40 6.6 3.5 100 310
minepump_spec5_product38_true-unreach-call_false-termination.cil.c 0 900    900    13000   130 170    0      .58 .36 11   41 5.3 2.8 55 290
minepump_spec5_product39_true-unreach-call_false-termination.cil.c 0 900    900    12000   150 170    0      .49 .32 8.8 39 7.1 3.8 78 330
minepump_spec5_product40_true-unreach-call_false-termination.cil.c 0 900    900    12000   140 160    0      .48 .31 7.0 40 5.8 3.1 64 300
minepump_spec5_product41_true-unreach-call_false-termination.cil.c 0 900    900    13000   150 240    0      .62 .40 7.9 40 5.8 3.1 66 300
minepump_spec5_product42_true-unreach-call_false-termination.cil.c 0 900    900    12000   170 240    1.1    .60 .39 7.9 40 5.8 3.1 77 300
minepump_spec5_product43_true-unreach-call_false-termination.cil.c 0 900    900    9900   170 210    0      .52 .33 11   40 6.3 3.3 86 310
minepump_spec5_product44_true-unreach-call_false-termination.cil.c 0 900    900    12000   120 160    0      .54 .34 9.7 39 5.4 2.9 60 290
minepump_spec5_product45_true-unreach-call_false-termination.cil.c 0 900    900    12000   130 160    0      .50 .33 8.8 40 5.9 3.1 94 300
minepump_spec5_product46_true-unreach-call_false-termination.cil.c 0 900    900    10000   140 160    0      .47 .31 9.4 39 5.8 3.1 93 300
minepump_spec5_product47_true-unreach-call_false-termination.cil.c 0 900    900    11000   150 160    0      .52 .34 13   41 5.6 3.0 40 300
minepump_spec5_product48_true-unreach-call_false-termination.cil.c 0 900    900    11000   150 160    0      .56 .37 7.4 40 5.9 3.1 110 310
minepump_spec5_product49_true-unreach-call_false-termination.cil.c 0 900    900    11000   140 180    0      .51 .33 11   41 6.3 3.3 110 290
minepump_spec5_product50_true-unreach-call_false-termination.cil.c 0 900    900    14000   150 180    0      .52 .34 8.0 41 6.8 3.6 110 320
minepump_spec5_product51_true-unreach-call_false-termination.cil.c 0 900    900    13000   170 180    0      .65 .41 8.6 41 5.3 2.8 92 290
minepump_spec5_product52_true-unreach-call_false-termination.cil.c 0 900    900    11000   140 150    0      .53 .33 11   40 5.3 2.8 61 300
minepump_spec5_product53_true-unreach-call_false-termination.cil.c 0 900    900    11000   180 180    0      .55 .35 11   41 6.0 3.2 95 300
minepump_spec5_product54_true-unreach-call_false-termination.cil.c 0 900    900    12000   200 170    .13   .64 .41 7.5 40 5.8 3.1 90 300
minepump_spec5_product55_true-unreach-call_false-termination.cil.c 0 900    900    11000   220 170    0      .50 .33 12   40 6.0 3.2 96 300
minepump_spec5_product56_true-unreach-call_false-termination.cil.c 0 900    900    10000   190 150    0      .65 .41 10   41 6.2 3.3 90 310
minepump_spec5_product57_true-unreach-call_false-termination.cil.c 0 900    900    11000   130 170    0      .54 .34 9.2 40 6.1 3.2 77 310
minepump_spec5_product58_true-unreach-call_false-termination.cil.c 0 900    900    11000   140 170    0      .56 .36 13   42 5.3 2.8 61 290
minepump_spec5_product59_true-unreach-call_false-termination.cil.c 0 900    900    10000   170 160    0      .52 .34 11   40 5.1 2.8 61 290
minepump_spec5_product60_true-unreach-call_false-termination.cil.c 0 900    900    11000   140 150    1.0    .61 .38 11   42 5.9 3.1 69 300
minepump_spec5_product61_true-unreach-call_false-termination.cil.c 0 900    900    13000   180 160    0      .47 .31 9.2 40 5.7 3.0 99 300
minepump_spec5_product62_true-unreach-call_false-termination.cil.c 0 900    900    11000   200 160    0      .67 .43 9.7 45 6.8 3.6 97 310
minepump_spec5_product63_true-unreach-call_false-termination.cil.c 0 900    900    11000   220 160    0      .67 .44 7.4 40 6.0 3.2 97 300
minepump_spec5_product64_true-unreach-call_false-termination.cil.c 0 900    900    12000   190 140    0      .59 .37 9.9 40 6.4 3.4 120 300
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c 0 890    900    12000   250 120    0      .50 .32 9.6 39 6.3 3.3 120 300
../../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)
total 597 393 260000 260000 3100000 250000 41000 660 597 4200 2200 59000 170000   597 3400 1800 44000 110000   597 16000 14000 270000 300000   597 14000 9100 180000 520000  
    correct results 243 393 50000 49000 580000 140000 1200 210 93 650 350 9000 29000   93 870 470 12000 31000   123 15000 14000 270000 300000   91 13000 8500 160000 470000  
        correct true 150 300 49000 49000 570000 140000 1000 170 1 0 0 0 0   68 0 0 0 0   123 15000 14000 270000 300000   91 13000 8500 160000 470000  
        correct false 93 93 96 96 1200 7300 210 36 92 650 350 9000 29000   25 870 470 12000 31000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 170 0 83000 83000 940000 58000 920 170 170 3500 1900 50000 140000   160 2500 1300 32000 79000   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 170 0 83000 83000 940000 58000 920 170 0 3500 1900 50000 140000   0 2500 1300 32000 79000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 393
Run set sv-comp17.ReachSafety-ProductLines