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