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