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 false(unreach-call) 0 wit inspect 480    480    6300   370 1.0  0      true 10    5.3  160   460 true 10   5.5 180 370 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4300   520 1.0  0      true 12    6.3  100   460 true 13   7.2 130 400 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5200   450 1.0  34      true 9.9  5.2  180   450 true 15   7.8 120 400 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.1  6.1  57   540 1.0  .29   true 12    6.5  140   520 true 12   6.5 160 400 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 530    530    5400   1400 1.1  .37   true 9.2  4.9  130   380 true 11   6.1 180 430 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5900   180 6.2  0      true 11    6.0  140   500 true 9.4 5.2 88 390 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   200 6.3  0      true 9.6  5.1  180   470 true 12   6.6 180 420 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5700   240 6.3  0      true 11    5.6  160   460 true 11   6.2 190 420 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5800   330 6.3  0      true 12    6.5  99   480 true 13   6.9 140 420 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   200 6.2  .34   true 10    5.4  160   500 true 14   7.3 180 410 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   210 6.3  0      true 13    6.8  190   560 true 14   7.4 160 410 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    6000   330 6.3  0      true 12    6.5  150   540 true 11   6.2 200 410 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5900   340 6.3  0      true 15    7.7  140   480 true 12   6.5 160 430 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 700    700    7700   760 6.4  0      true 8.7  4.6  190   340 true 12   6.8 180 460 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   180 6.2  0      true 12    6.2  140   460 true 10   5.6 180 390 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   200 6.2  0      true 13    6.6  140   490 true 13   7.0 120 420 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5500   240 6.4  0      true 11    6.0  160   470 true 13   7.2 150 410 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    6000   330 6.3  0      true 11    5.8  130   460 true 10   5.6 190 410 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6500   200 6.2  0      true 11    5.8  160   460 true 14   7.7 130 390 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   220 6.3  0      true 13    6.6  140   470 true 11   6.0 190 400 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    6000   320 6.3  0      true 12    6.3  140   460 true 12   6.6 190 420 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    6500   340 6.3  0      true 10    5.4  160   500 true 15   8.0 130 400 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 700    700    9400   730 6.4  0      true 9.0  4.7  160   380 true 12   6.7 190 450 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6700   250 1.0  0      true 15    7.6  130   490 true 14   7.2 130 450 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5700   270 1.0  0      true 13    6.7  190   490 true 13   6.7 190 470 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6100   420 1.0  0      true 13    7.0  170   490 true 12   6.3 180 460 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4500   390 1.0  0      true 18    9.3  180   530 true 14   7.3 190 470 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   320 1.0  0      true 15    8.0  190   570 true 15   7.9 160 470 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4900   540 1.0  0      true 12    6.4  220   550 true 11   6.2 220 480 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6000   430 1.0  0      true 12    6.0  220   530 true 13   7.0 150 480 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5600   420 1.0  0      true 15    7.8  160   520 true 15   8.2 130 460 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   330 1.0  0      true 16    8.4  180   520 true 16   8.6 190 490 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   560 1.0  0      true 15    7.9  190   520 true 12   6.4 190 490 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 620    620    4200   1400 1.1  0      true 13    6.8  190   420 true 13   6.8 250 480 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6500   190 6.2  0      true 12    6.2  130   460 true 12   6.3 180 410 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   220 6.3  0      true 13    7.0  140   510 true 12   6.4 170 410 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5800   320 6.3  0      true 11    5.8  200   510 true 11   6.2 190 400 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5100   340 6.3  0      true 12    6.5  150   480 true 14   7.4 150 410 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 700    700    7300   720 6.4  0      true 12    6.1  130   380 true 17   9.1 110 430 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   1500 16    0      - - error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.4 3.4 120 300
elevator_spec13_product22_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   2100 16    0      - - error (invalid witness file) .65 .42 8.7 40 error (invalid witness file) 7.5 3.9 130 310
elevator_spec13_product23_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    12000   660 16    0      - - error (invalid witness file) .56 .36 8.2 39 error (invalid witness file) 6.6 3.5 95 300
elevator_spec13_product24_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    13000   2400 16    0      - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 6.0 3.2 89 300
elevator_spec13_product29_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   1700 16    0      - - error (invalid witness file) .60 .38 7.4 40 error (invalid witness file) 5.8 3.1 88 300
elevator_spec13_product30_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    9000   770 16    35      - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 7.2 3.8 100 300
elevator_spec13_product31_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    12000   670 16    0      - - error (invalid witness file) .67 .43 7.7 42 error (invalid witness file) 6.5 3.4 67 320
elevator_spec13_product32_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    10000   750 16    .21   - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 6.2 3.3 98 310
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 890    900    9100   1500 8.2  34      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.1 77 300
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 540    540    6700   290 21    0      - - true 25    14    510   900 out of memory 230   160   2500 7000
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    540    6500   290 21    .0041 - - true 27    15    600   1000 out of memory 290   200   4700 7000
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    540    6600   300 21    0      - - true 32    17    400   930 out of memory 300   210   2600 7000
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 660    650    7400   350 29    34      - - true 34    19    540   1300 out of memory 270   190   4300 7000
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    550    6300   290 22    0      - - true 31    17    390   970 out of memory 320   230   5000 7000
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 660    660    8600   330 29    0      - - true 35    20    740   1300 out of memory 250   170   3100 7000
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6100   280 22    0      - - true 69    55    1300   1500 out of memory 220   150   2500 7000
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 540    540    5600   290 21    0      - - true 80    64    900   1700 out of memory 260   180   2900 7000
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 540    540    7000   290 22    0      - - true 83    66    1100   1600 out of memory 260   180   3100 7000
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    540    6900   300 25    0      - - true 89    73    1200   1700 out of memory 250   170   5200 7000
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    6600   290 21    0      - - true 68    54    1200   2000 out of memory 210   140   3100 7000
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    540    7200   300 21    0      - - true 73    59    1500   1700 out of memory 240   150   3200 7000
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 570    570    6600   300 21    0      - - true 150    130    2600   2000 out of memory 190   120   1800 7000
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 580    580    7600   290 21    0      - - true 130    120    2800   2100 out of memory 210   150   2400 7000
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    540    7700   300 21    .0041 - - true 84    67    1000   1700 out of memory 300   200   4400 7000
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 550    550    6000   290 21    0      - - true 110    92    1000   1800 out of memory 230   160   3900 7000
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 580    570    7000   310 21    0      - - true 200    180    2400   2100 out of memory 170   110   2100 7000
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 590    580    6800   300 21    0      - - true 170    150    1900   2300 out of memory 250   170   4000 7000
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 440    440    5200   280 11    0      - - true 37    22    520   1100 out of memory 180   110   1600 7000
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    7200   280 11    0      - - true 46    28    400   1100 out of memory 170   110   3300 7000
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    5500   280 11    0      - - true 35    22    510   1100 out of memory 150   95   2900 7000
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    5800   290 11    .13   - - true 40    26    720   1200 out of memory 240   150   2200 7000
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 480    480    6000   280 11    0      - - true 38    24    730   1200 out of memory 140   89   1400 7000
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    6900   290 11    0      - - true 37    24    800   1200 out of memory 180   110   2300 7000
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    6300   280 11    .13   - - true 45    33    400   1300 out of memory 180   110   2300 7000
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    6300   320 11    34      - - true 51    35    850   1300 out of memory 240   160   4000 7000
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    7200   280 11    0      - - true 41    25    580   1100 out of memory 150   92   2300 7000
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    6100   290 11    0      - - true 42    27    750   1300 out of memory 170   110   2100 7000
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    6400   280 11    0      - - true 49    35    660   1400 out of memory 130   79   990 7000
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    6100   280 11    0      - - true 56    37    710   1400 out of memory 220   140   2000 7000
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    6000   300 3.5  .0041 - - true 25    14    260   990 out of memory 190   120   1500 7000
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    6900   330 3.6  .0041 - - true 28    15    360   930 out of memory 170   110   2300 7000
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    5800   290 3.5  .0041 - - true 30    16    500   900 out of memory 150   97   1400 7000
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    5200   350 3.6  .0041 - - true 35    19    530   1400 out of memory 150   98   2700 7000
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    6400   610 3.6  0      - - true 39    21    450   1100 out of memory 150   97   1300 7000
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    490    4800   460 3.6  0      - - true 43    25    400   1500 out of memory 170   110   2400 7000
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    6200   330 3.6  0      - - true 29    16    360   960 out of memory 190   120   3200 7000
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    5400   400 3.6  0      - - true 32    18    540   1500 out of memory 170   110   2200 7000
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 490    490    5800   320 3.6  .0041 - - true 30    17    490   1200 out of memory 180   120   1500 7000
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    490    6800   520 3.6  0      - - true 37    21    730   1500 out of memory 180   120   1800 7000
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    6800   280 11    .13   - - true 43    27    530   1000 out of memory 140   88   1000 7000
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    6800   290 11    .0041 - - true 39    25    790   1100 out of memory 210   130   1900 7000
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 500    500    5500   280 11    0      - - true 44    27    310   1100 out of memory 170   99   1900 7000
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    7200   280 11    0      - - true 38    24    790   1200 out of memory 180   110   3200 7000
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    6200   280 11    0      - - true 49    34    450   1400 out of memory 180   110   2100 7000
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    5700   280 11    0      - - true 53    37    930   1400 out of memory 150   97   1300 7000
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   150 8.7  0      true 20    10    240   790 true 13   6.7 130 450 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5900   170 9.0  0      true 25    14    300   1100 true 14   7.6 150 500 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   150 8.7  0      true 19    10    280   790 true 13   7.2 140 450 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5900   320 8.7  0      true 27    15    510   940 true 15   8.1 170 500 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   160 8.8  0      true 26    14    330   790 true 15   8.2 140 490 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5200   200 8.8  0      true 28    15    290   790 true 14   7.5 160 470 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5800   260 8.8  0      true 33    18    320   1700 true 14   7.3 220 510 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5200   310 8.8  0      true 34    19    480   1100 true 12   6.6 150 500 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 890    900    9000   1600 7.8  0      error (invalid witness file) .54 .34 13   43 error (invalid witness file) 6.9 3.6 130 310 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   130 8.7  0      true 15    8.0  300   760 true 11   6.1 210 450 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6400   220 8.7  0      true 25    13    320   1100 true 12   6.3 220 470 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6900   280 8.7  0      true 23    12    250   760 true 13   6.9 200 470 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    6400   410 8.7  0      true 35    19    330   950 true 15   7.7 140 480 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   190 8.7  0      true 21    11    370   770 true 12   6.5 200 460 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5400   200 8.7  0      true 28    15    400   1000 true 11   6.2 120 480 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5800   260 8.7  0      true 25    13    260   1100 true 15   7.6 220 500 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5100   240 8.8  0      true 28    16    430   1600 true 16   8.5 220 500 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 890    900    10000   1600 7.8  34      error (invalid witness file) .63 .39 8.5 40 error (invalid witness file) 6.3 3.3 130 300 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   260 6.2  0      true 18    9.4  350   730 true 13   7.0 160 460 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5800   170 6.2  .17   true 18    9.6  190   760 true 15   8.1 140 420 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   370 6.2  0      true 15    8.2  310   780 true 14   7.3 220 460 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   240 6.2  0      true 27    14    290   1100 true 14   7.4 150 470 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   210 6.2  0      true 24    13    390   1100 true 13   6.7 280 470 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   180 6.2  0      true 21    11    310   780 true 13   7.1 150 440 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   230 6.2  0      true 24    13    350   1200 true 14   7.3 210 510 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6400   210 6.2  34      true 22    12    450   770 true 15   8.1 150 490 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   250 6.2  0      true 23    12    360   800 true 13   7.0 200 450 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4700   190 6.3  34      true 27    14    290   800 true 12   6.4 230 500 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5000   440 6.3  0      true 25    13    400   1200 true 12   6.7 200 480 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4900   190 6.3  0      true 25    13    270   1100 true 12   6.4 190 500 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   360 6.3  0      true 34    19    440   980 true 13   7.2 140 510 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   320 6.3  0      true 33    18    500   1100 true 14   7.2 160 500 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 620    620    7400   1600 6.4  0      true 13    6.9  160   420 true 12   6.6 200 480 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4800   190 6.2  0      true 20    10    360   710 true 14   7.2 130 500 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6600   130 6.2  0      true 18    9.4  330   690 true 16   8.4 140 440 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6200   240 6.3  0      true 22    11    240   800 true 15   7.9 160 450 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   240 6.3  0      true 24    13    420   1100 true 13   7.2 200 470 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4600   180 6.3  0      true 20    11    330   780 true 12   6.2 160 490 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5900   210 6.3  0      true 28    15    490   920 true 11   6.1 150 490 - -
email_spec27_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4900   180 6.3  0      true 31    17    340   1200 true 13   6.8 190 490 - -
email_spec27_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   190 6.3  0      true 29    15    300   800 true 14   7.4 190 490 - -
email_spec27_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   320 6.3  0      true 22    11    420   800 true 15   7.7 160 440 - -
email_spec27_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5800   170 6.3  0      true 21    11    300   1100 true 15   8.1 130 510 - -
email_spec27_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6600   280 6.5  0      true 29    16    400   1400 true 13   6.9 130 500 - -
email_spec27_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   150 6.3  0      true 29    15    260   800 true 14   7.2 160 510 - -
email_spec27_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   440 6.3  0      true 31    17    580   1100 true 13   6.8 150 500 - -
email_spec27_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    4700   390 6.4  0      true 29    16    570   1700 true 15   7.8 190 500 - -
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 740    740    6600   1600 6.5  0      true 10    5.4  200   410 true 16   8.5 160 490 - -
email_spec3_product13_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4400   170 1.0  35      true 14    7.6  190   670 unknown 30   17   430 550 - -
email_spec3_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   220 1.0  0      true 16    8.5  210   760 unknown 31   17   310 550 - -
email_spec3_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4700   150 1.0  0      true 20    11    190   770 true 12   6.5 160 420 - -
email_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4900   170 1.0  0      true 21    11    190   780 true 11   5.9 200 430 - -
email_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5700   330 1.0  0      true 26    14    380   1100 true 10   5.6 130 450 - -
email_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5000   150 1.0  0      true 18    9.4  350   830 true 15   7.8 150 430 - -
email_spec3_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5200   420 1.0  0      true 28    15    380   1100 true 17   9.1 160 490 - -
email_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5300   220 1.0  0      true 29    16    270   1400 true 15   8.1 170 460 - -
email_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5300   140 1.0  0      true 14    7.5  210   790 unknown 38   21   420 560 - -
email_spec3_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6300   300 1.0  0      true 24    13    310   1300 unknown 41   23   380 580 - -
email_spec3_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   210 1.0  .29   true 23    12    250   850 true 11   5.8 160 430 - -
email_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5200   240 1.0  0      true 23    12    310   810 true 13   7.2 140 450 - -
email_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5800   200 1.0  0      true 30    16    450   980 true 14   7.5 180 470 - -
email_spec3_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5100   280 1.0  0      true 23    12    300   1100 true 12   6.3 170 450 - -
email_spec3_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5000   200 1.0  0      true 32    18    450   1100 true 15   8.2 180 480 - -
email_spec3_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5900   260 1.0  0      true 30    17    570   1100 true 16   8.4 140 480 - -
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 510    510    4300   1600 1.1  0      true 8.4  4.4  130   370 true 15   8.0 150 460 - -
email_spec4_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   190 6.2  0      true 20    10    230   780 true 12   6.4 180 430 - -
email_spec4_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   140 6.2  0      true 22    11    220   780 true 13   7.0 140 450 - -
email_spec4_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   270 6.2  34      true 27    14    260   1100 true 14   7.5 110 450 - -
email_spec4_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5000   220 6.2  0      true 20    10    260   790 true 11   6.1 190 450 - -
email_spec4_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   200 6.2  0      true 30    16    310   1100 true 12   6.3 210 480 - -
email_spec4_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   360 6.3  0      true 25    13    540   1200 true 12   6.3 180 480 - -
email_spec4_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6500   230 6.2  0      true 17    9.0  370   790 true 11   6.0 150 450 - -
email_spec4_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   510 6.3  0      true 25    13    390   820 true 13   6.9 140 480 - -
email_spec4_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   210 6.2  0      true 24    13    410   1200 true 11   6.1 190 470 - -
email_spec4_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6500   150 6.3  0      true 24    12    410   840 true 12   6.3 180 470 - -
email_spec4_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   340 6.3  0      true 32    18    430   970 true 12   6.4 180 500 - -
email_spec4_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   280 6.3  0      true 36    19    400   1000 true 12   6.3 190 490 - -
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 620    620    5900   1600 6.3  0      true 12    6.2  200   400 true 13   7.0 200 480 - -
email_spec6_product12_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6600   160 6.2  0      true 15    7.8  220   670 unknown 34   19   500 560 - -
email_spec6_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   170 6.2  0      true 18    9.5  230   790 unknown 36   21   310 580 - -
email_spec6_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6300   150 6.2  0      true 18    9.6  190   760 true 12   6.4 170 440 - -
email_spec6_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   140 6.2  0      true 21    11    240   790 true 14   7.4 160 450 - -
email_spec6_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6800   360 6.2  0      true 25    13    490   900 true 11   5.8 210 450 - -
email_spec6_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   190 6.2  0      true 25    13    430   1200 true 16   8.4 180 490 - -
email_spec6_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   170 6.2  0      true 19    10    230   770 true 11   5.7 98 440 - -
email_spec6_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5000   220 6.2  0      true 26    14    390   1400 true 12   6.4 170 470 - -
email_spec6_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   180 6.2  0      true 17    8.8  220   650 unknown 41   24   480 590 - -
email_spec6_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   240 6.2  .17   true 24    13    330   790 unknown 53   30   540 620 - -
email_spec6_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   270 6.3  0      true 18    9.7  360   840 true 14   7.5 180 470 - -
email_spec6_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   300 6.2  0      true 25    13    280   1000 true 13   7.0 240 480 - -
email_spec6_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5200   230 6.2  .85   true 26    14    470   1000 true 13   7.2 200 500 - -
email_spec6_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   260 6.2  0      true 19    10    340   1100 true 12   6.3 200 490 - -
email_spec6_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6300   420 6.2  0      true 31    17    520   1000 true 12   6.4 200 490 - -
email_spec6_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 500    500    5300   260 6.2  0      true 29    16    540   1600 true 16   8.5 160 500 - -
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 630    630    5400   1500 6.3  0      true 9.3  4.9  170   370 true 14   7.7 150 470 - -
email_spec7_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 480    490    5000   330 6.2  0      true 14    7.6  190   670 unknown 37   21   470 570 - -
email_spec7_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6400   360 6.2  0      true 22    12    300   1000 unknown 41   23   400 590 - -
email_spec7_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5200   200 6.3  0      true 20    10    300   770 true 11   6.0 120 450 - -
email_spec7_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6500   140 6.2  0      true 21    11    390   1000 true 14   7.6 160 470 - -
email_spec7_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   180 6.2  0      true 23    13    460   1100 true 12   6.3 220 480 - -
email_spec7_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6900   190 6.2  0      true 22    11    330   1100 true 15   8.1 150 470 - -
email_spec7_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   250 6.3  0      true 30    16    380   1600 true 15   7.9 170 500 - -
email_spec7_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6600   230 6.2  0      true 31    17    460   1100 true 16   8.7 190 500 - -
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 640    640    6500   1600 6.3  0      true 12    6.3  210   380 true 13   6.8 210 470 - -
email_spec8_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   190 6.2  0      true 19    10    300   670 true 14   7.3 140 440 - -
email_spec8_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6000   310 6.2  0      true 16    8.5  310   800 true 11   5.9 150 460 - -
email_spec8_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4800   220 6.2  0      true 26    14    340   960 true 12   6.6 140 470 - -
email_spec8_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   240 6.2  0      true 30    16    310   1100 true 13   6.7 200 480 - -
email_spec8_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6400   150 6.2  .30   true 22    11    350   740 true 12   6.3 230 450 - -
email_spec8_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5100   350 6.5  0      true 27    14    510   980 true 14   7.7 150 480 - -
email_spec8_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4600   200 6.2  0      true 23    12    320   800 true 12   6.6 150 450 - -
email_spec8_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   190 6.3  0      true 23    12    360   810 true 15   7.9 180 500 - -
email_spec8_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   450 6.3  0      true 31    17    410   930 true 12   6.7 240 490 - -
email_spec8_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5800   220 6.3  0      true 23    12    320   1000 true 13   6.8 220 480 - -
email_spec8_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    4900   280 6.3  0      true 33    18    530   1000 true 14   7.3 220 500 - -
email_spec8_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    500    5300   250 6.3  0      true 32    17    500   1600 true 13   7.0 200 500 - -
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 620    630    6800   1600 6.3  0      true 12    6.3  130   390 true 12   6.6 200 460 - -
email_spec9_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   210 6.2  0      true 17    8.9  270   670 true 12   6.4 190 440 - -
email_spec9_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   200 6.2  0      true 19    10    330   730 true 12   6.6 170 460 - -
email_spec9_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   280 6.2  0      true 27    14    290   1100 true 13   6.8 200 480 - -
email_spec9_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   390 6.2  0      true 25    13    530   1100 true 13   7.1 130 480 - -
email_spec9_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5300   230 6.2  0      true 27    14    230   740 true 12   6.3 200 460 - -
email_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5800   240 6.4  0      true 26    14    470   1100 true 12   6.8 200 470 - -
email_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5000   230 6.2  .13   true 29    15    270   830 true 11   6.1 160 450 - -
email_spec9_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6300   160 6.3  0      true 25    13    340   820 true 16   8.4 190 490 - -
email_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5700   210 6.3  0      true 29    16    420   1200 true 12   6.7 210 490 - -
email_spec9_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5900   200 6.3  .30   true 29    15    310   800 true 15   8.1 170 480 - -
email_spec9_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6300   370 6.3  0      true 37    20    410   1000 true 14   7.2 200 510 - -
email_spec9_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 490    500    5500   310 6.3  0      true 35    19    480   1000 true 12   6.6 190 480 - -
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 620    620    6900   1500 6.3  0      true 10    5.2  170   400 true 16   8.3 180 470 - -
email_spec0_product05_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5300   650 3.5  0      - - true 14    7.5  180   500 true 12   6.6 190 370
email_spec0_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    6500   1500 3.5  0      - - true 22    11    220   510 true 14   7.2 180 400
email_spec0_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5600   1400 3.5  0      - - true 14    7.3  270   480 true 13   7.1 230 410
email_spec0_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    5100   1600 3.5  .0041 - - true 15    8.0  310   480 true 16   8.7 210 470
email_spec0_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6200   2700 3.5  0      - - true 20    10    410   560 true 18   9.3 140 590
email_spec0_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    5500   2700 3.5  0      - - true 19    10    300   600 true 20   10   220 600
email_spec0_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    6400   2800 3.6  0      - - true 26    13    380   660 true 23   12   320 610
email_spec0_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    6000   2900 3.6  0      - - true 26    13    280   670 true 22   12   290 610
email_spec0_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5200   1600 3.5  .0041 - - true 21    11    310   530 true 13   7.0 140 430
email_spec0_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5900   1800 3.5  34      - - true 17    8.9  340   510 true 31   17   390 700
email_spec0_product38_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5300   2000 3.5  .0041 - - true 20    10    350   640 true 17   8.8 230 490
email_spec0_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6300   2700 3.5  .0041 - - true 19    10    240   650 true 31   16   250 710
email_spec11_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    5100   620 3.5  .30   - - true 13    6.5  280   480 true 13   6.6 190 360
email_spec11_product07_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    6400   1500 3.5  .0041 - - true 20    10    190   490 true 16   8.3 120 410
email_spec11_product08_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    500    5400   1600 3.5  .0041 - - true 20    10    260   520 true 17   9.1 230 590
email_spec11_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 510    510    5600   1500 3.5  0      - - true 14    7.3  180   480 true 13   6.8 200 380
email_spec11_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6100   2400 3.5  34      - - true 22    11    250   520 true 21   11   250 590
email_spec11_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5700   2700 3.6  0      - - true 27    14    220   640 true 25   13   250 610
email_spec11_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    5800   2800 3.6  0      - - true 19    9.6  290   610 true 21   11   260 600
email_spec11_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    3000   2900 3.6  0      - - true 24    12    460   670 true 22   12   280 570
email_spec11_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5900   1600 3.5  0      - - true 19    9.7  270   520 true 13   7.1 240 400
email_spec11_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6900   1800 3.5  0      - - true 16    8.5  250   510 true 18   9.3 120 600
email_spec11_product39_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5100   1900 3.5  0      - - true 21    11    300   610 true 19   9.9 310 630
email_spec11_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5400   2700 3.5  0      - - true 24    12    210   640 true 20   10   290 580
email_spec1_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    500    5800   1600 3.5  0      - - true 33    18    430   800 true 100   61   750 6100
email_spec1_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5500   2500 3.6  0      - - true 34    20    490   920 out of memory 180   110   3300 7000
email_spec27_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    500    6000   1800 3.5  .13   - - true 29    17    480   950 out of memory 210   140   2700 7000
email_spec27_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5100   2600 3.6  0      - - true 33    20    580   1000 out of memory 170   110   1400 7000
email_spec4_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5900   1800 3.5  0      - - true 31    18    270   890 out of memory 230   150   3100 7000
email_spec4_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5700   2700 3.5  0      - - true 39    24    440   1100 out of memory 270   200   2900 7000
email_spec4_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6200   2700 3.6  0      - - true 30    18    480   940 out of memory 140   89   1200 7000
email_spec4_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    5500   2800 3.6  0      - - true 39    26    520   1400 out of memory 200   130   1900 7000
email_spec7_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    500    5700   1700 3.5  .0041 - - true 19    9.6  230   510 true 16   8.4 250 450
email_spec7_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5900   2500 3.6  0      - - true 24    12    330   670 true 17   8.9 190 470
email_spec7_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5000   2500 3.5  0      - - true 19    9.8  190   540 true 18   9.7 210 630
email_spec7_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6900   2700 3.5  0      - - true 21    11    240   540 true 17   9.1 190 440
email_spec7_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    5700   2800 3.6  .17   - - true 27    14    360   650 true 20   10   260 590
email_spec7_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    6700   2800 3.5  .0041 - - true 19    9.9  270   610 true 18   9.4 160 590
email_spec7_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    510    5200   2800 3.6  .0041 - - true 29    15    290   660 true 15   8.2 220 480
email_spec7_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    5700   2900 3.6  0      - - true 26    13    200   660 true 18   9.5 160 600
email_spec8_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    500    6500   1600 3.5  0      - - true 29    16    590   850 true 110   66   1100 5500
email_spec8_product14_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    5900   2400 11    0      - - true 44    28    520   1100 out of memory 230   150   2300 7000
email_spec8_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5200   2600 3.6  0      - - true 30    17    530   1000 out of memory 130   80   1000 7000
email_spec8_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 540    520    6000   2800 11    .0041 - - true 46    31    1000   1300 out of memory 130   80   1400 7000
email_spec9_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    500    6200   1600 3.5  0      - - true 28    16    550   880 true 98   58   810 5400
email_spec9_product14_true-unreach-call_true-termination.cil.c true 2 wit inspect 530    520    5100   2400 11    0      - - true 38    24    420   1200 out of memory 170   110   1500 7000
email_spec9_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 520    510    5700   2600 3.6  0      - - true 35    20    360   890 out of memory 140   89   1100 7000
email_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 540    520    6500   2800 11    0      - - true 42    28    660   1400 out of memory 140   83   1600 7000
minepump_spec1_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .56 .56 6.9 78 .91 0      false(unreach-call) 6.1  3.3  94   290 true 9.2 4.9 150 330 - -
minepump_spec1_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .57 .57 6.6 77 .91 0      false(unreach-call) 5.7  3.1  110   300 true 7.3 3.9 110 320 - -
minepump_spec1_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .63 .62 6.7 78 .92 .13   false(unreach-call) 6.9  3.7  100   320 true 8.5 4.6 130 330 - -
minepump_spec1_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .75 .75 8.4 79 .91 0      false(unreach-call) 5.6  3.1  110   320 true 7.3 4.0 110 330 - -
minepump_spec1_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .61 .61 8.2 78 .91 0      false(unreach-call) 7.8  4.2  74   330 true 9.8 5.2 110 330 - -
minepump_spec1_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 8.5 78 .91 0      false(unreach-call) 7.4  4.0  100   340 true 7.8 4.2 140 320 - -
minepump_spec1_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .77 .77 8.9 79 .91 0      false(unreach-call) 7.4  4.0  85   320 true 8.6 4.5 130 320 - -
minepump_spec1_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .80 .80 9.9 79 .91 0      false(unreach-call) 7.4  4.0  85   320 true 8.9 4.7 110 320 - -
minepump_spec1_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  16   78 3.5  0      false(unreach-call) 8.1  4.4  92   330 true 10   5.5 110 320 - -
minepump_spec1_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  16   78 3.5  0      false(unreach-call) 5.9  3.2  91   300 true 7.3 4.1 150 310 - -
minepump_spec1_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.5  1.5  20   79 3.5  0      false(unreach-call) 6.2  3.4  93   330 true 7.8 4.2 150 320 -