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 - -
minepump_spec1_product53_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  .71 27 .84 0   false(unreach-call) 5.8  3.2  100   310 true 7.9 4.3 170 320 - -
minepump_spec1_product54_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  .94 27 .99 0   false(unreach-call) 6.3  3.4  110   340 true 8.0 4.3 140 320 - -
minepump_spec1_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.0  27 .84 0   false(unreach-call) 6.0  3.2  96   340 true 7.7 4.1 88 320 - -
minepump_spec1_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .096 .095 1.4  27 .84 0   false(unreach-call) 5.7  3.1  96   300 true 7.7 4.2 140 310 - -
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .13  .13  1.2  27 .84 0   true 5.0  2.7  88   280 true 8.8 4.7 160 310 - -
minepump_spec2_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.0  26 .84 0   false(unreach-call) 5.8  3.1  97   310 true 7.8 4.1 130 330 - -
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .14  .14  1.2  27 .84 0   false(unreach-call) 6.1  3.3  67   300 true 7.8 4.2 150 320 - -
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.2  27 .84 0   false(unreach-call) 6.7  3.5  150   320 true 7.5 4.0 140 320 - -
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.3  26 .84 0   false(unreach-call) 8.0  4.3  77   300 true 7.7 4.2 150 320 - -
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.6  26 .87 0   false(unreach-call) 6.9  3.7  75   350 true 8.3 4.4 160 320 - -
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .14  .13  1.8  27 .84 0   false(unreach-call) 6.7  3.6  75   330 true 7.3 4.0 130 320 - -
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .14  .14  1.7  27 .84 0   false(unreach-call) 8.3  4.4  44   300 true 8.2 4.4 150 320 - -
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .16  .15  1.7  27 .84 0   false(unreach-call) 7.4  4.0  100   330 true 8.1 4.3 160 330 - -
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .16  .16  2.1  27 .84 0   true 5.6  3.0  81   330 true 8.5 4.6 150 320 - -
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .12  .92 26 .84 0   false(unreach-call) 5.7  3.1  95   300 true 7.3 3.9 110 320 - -
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  .83 26 .84 0   false(unreach-call) 5.1  2.8  59   290 true 7.5 4.0 150 320 - -
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .10  .10  1.0  26 .84 0   false(unreach-call) 5.6  3.0  82   300 true 6.9 3.8 140 310 - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  .93 26 .84 0   false(unreach-call) 5.6  3.0  83   320 true 7.6 4.1 140 320 - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  .95 26 .84 0   false(unreach-call) 6.7  3.6  65   300 true 7.3 4.0 110 320 - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.0  26 .99 0   false(unreach-call) 5.4  2.9  72   290 true 8.7 4.6 130 320 - -
minepump_spec3_product07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35  .35  .98 26 .84 0   false(unreach-call) 5.4  2.9  79   300 true 8.4 4.5 140 330 - -
minepump_spec3_product08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.1  26 .84 0   false(unreach-call) 6.0  3.2  96   340 true 7.3 3.9 110 320 - -
minepump_spec3_product09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35  .35  .99 26 .84 0   false(unreach-call) 5.7  3.1  96   320 true 7.7 4.2 130 320 - -
minepump_spec3_product10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .096 .095 1.0  26 .84 0   false(unreach-call) 6.1  3.3  98   340 true 7.1 3.8 140 320 - -
minepump_spec3_product11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.0  26 .84 0   false(unreach-call) 5.3  2.9  64   300 true 7.6 4.1 130 320 - -
minepump_spec3_product12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.1  26 .84 0   false(unreach-call) 5.3  2.9  65   310 true 7.6 4.1 140 320 - -
minepump_spec3_product13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .093 .093 1.0  26 .84 0   false(unreach-call) 5.7  3.1  87   330 true 7.8 4.2 140 330 - -
minepump_spec3_product14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  .99 26 .84 0   false(unreach-call) 5.5  3.0  69   320 true 7.6 4.1 140 320 - -
minepump_spec3_product15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.0  26 .84 0   false(unreach-call) 5.5  3.0  89   310 true 7.9 4.2 140 320 - -
minepump_spec3_product16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.0  26 .84 0   false(unreach-call) 5.5  2.9  66   300 true 8.1 4.4 140 320 - -
minepump_spec3_product17_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.0  26 .84 0   false(unreach-call) 5.7  3.1  69   330 true 7.9 4.2 120 320 - -
minepump_spec3_product18_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  .86 26 .84 0   false(unreach-call) 7.0  3.8  88   310 true 8.8 4.7 180 330 - -
minepump_spec3_product19_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .093 .093 1.1  26 .84 0   false(unreach-call) 5.8  3.2  100   340 true 7.2 3.9 140 320 - -
minepump_spec3_product20_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .10  .099 1.1  27 .84 0   false(unreach-call) 5.4  2.9  59   310 true 7.9 4.2 130 320 - -
minepump_spec3_product21_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .094 .094 1.1  27 .91 0   false(unreach-call) 6.2  3.4  91   320 true 8.1 4.3 150 320 - -
minepump_spec3_product22_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .094 .093 .98 27 .84 0   false(unreach-call) 5.5  3.0  92   320 true 7.7 4.2 130 320 - -
minepump_spec3_product23_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .097 .097 1.0  27 .84 0   false(unreach-call) 6.0  3.2  130   320 true 8.0 4.3 150 320 - -
minepump_spec3_product24_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .092 .092 1.3  27 .84 0   false(unreach-call) 6.1  3.3  140   320 true 8.8 4.7 140 340 - -
minepump_spec3_product25_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.1  26 .84 0   false(unreach-call) 6.1  3.2  110   310 true 8.0 4.3 140 320 - -
minepump_spec3_product26_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.0  27 .84 0   false(unreach-call) 6.5  3.5  55   330 true 7.9 4.2 140 320 - -
minepump_spec3_product27_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.1  26 .84 0   false(unreach-call) 5.4  2.9  84   290 true 7.6 4.1 150 320 - -
minepump_spec3_product28_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.1  27 .84 0   false(unreach-call) 5.7  3.1  94   320 true 8.1 4.3 150 320 - -
minepump_spec3_product29_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .095 .094 1.1  27 .84 0   false(unreach-call) 6.1  3.2  140   320 true 7.7 4.2 96 320 - -
minepump_spec3_product30_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .096 .095 .97 27 .84 0   false(unreach-call) 7.0  3.8  60   300 true 8.2 4.4 150 330 - -
minepump_spec3_product31_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.0  27 .84 0   false(unreach-call) 5.9  3.2  67   340 true 7.9 4.3 170 320 - -
minepump_spec3_product32_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  .88 27 .84 0   false(unreach-call) 5.5  3.0  67   300 true 7.7 4.2 160 320 - -
minepump_spec3_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.2  27 .84 0   false(unreach-call) 5.3  2.9  60   290 true 7.7 4.1 150 330 - -
minepump_spec3_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.2  27 .84 0   false(unreach-call) 5.6  3.0  110   290 true 8.3 4.4 120 320 - -
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.0  27 .84 0   false(unreach-call) 5.9  3.2  120   290 true 7.9 4.2 140 320 - -
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.0  27 .84 0   false(unreach-call) 6.0  3.3  120   320 true 7.8 4.2 120 320 - -
minepump_spec3_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.0  27 .84 0   false(unreach-call) 5.6  3.0  120   300 true 7.8 4.2 99 320 - -
minepump_spec3_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12  .12  1.1  27 .84 0   false(unreach-call) 5.8  3.2  130   330 true 8.4 4.5 170 320 - -
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.1  27 .84 0   false(unreach-call) 5.4  2.9  90   280 true 8.1 4.3 140 330 - -
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.2  27 .84 0   false(unreach-call) 5.4  3.0  79   290 true 7.9 4.3 150 320 - -
minepump_spec3_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .14  .14  1.0  27 .84 0   false(unreach-call) 6.1  3.3  92   330 true 8.5 4.5 160 330 - -
minepump_spec3_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .099 .099 1.1  27 .84 0   false(unreach-call) 6.0  3.2  95   330 true 8.1 4.4 160 330 - -
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.1  27 .84 0   false(unreach-call) 5.8  3.1  100   310 true 7.9 4.2 120 320 - -
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.0  27 .84 0   false(unreach-call) 5.6  3.0  83   290 true 8.5 4.5 140 320 - -
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  1.2  27 .84 0   false(unreach-call) 5.6  3.1  63   320 true 8.5 4.6 170 320 - -
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .097 .097 1.2  27 .84 0   false(unreach-call) 5.8  3.2  120   320 true 8.1 4.4 160 320 - -
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .11  .11  1.1  27 .84 0   false(unreach-call) 6.4  3.5  65   290 true 8.3 4.5 170 320 - -
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .10  .099 1.1  27 .84 0   false(unreach-call) 6.0  3.3  100   340 true 8.5 4.5 150 320 - -
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .12  .12  1.3  27 .84 0   true 5.4  2.9  68   330 true 9.0 4.8 130 330 - -
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.5  26 .84 0   false(unreach-call) 6.6  3.6  120   300 true 7.4 4.1 140 310 - -
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.4  26 .84 0   false(unreach-call) 6.6  3.6  100   320 true 8.1 4.3 160 320 - -
minepump_spec4_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .54  .54  1.1  26 .84 0   false(unreach-call) 6.2  3.4  100   330 true 7.7 4.1 120 330 - -
minepump_spec4_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.7  26 .84 0   false(unreach-call) 8.1  4.3  71   300 true 7.7 4.1 100 320 - -
minepump_spec4_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .16  .16  1.6  27 .84 0   false(unreach-call) 6.7  3.6  76   310 true 7.8 4.2 160 320 - -
minepump_spec4_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .55  .55  1.6  27 .98 0   false(unreach-call) 6.4  3.4  70   290 true 7.8 4.2 150 320 - -
minepump_spec4_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .15  .15  1.8  26 .84 0   false(unreach-call) 6.4  3.5  55   310 true 8.3 4.5 150 340 - -
minepump_spec4_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .18  .18  1.7  27 .84 0   false(unreach-call) 6.8  3.6  66   330 true 8.5 4.5 170 330 - -
minepump_spec4_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .15  .14  1.5  26 .84 0   false(unreach-call) 7.0  3.8  120   330 true 7.6 4.0 110 320 - -
minepump_spec4_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13  .13  1.6  26 .84 0   false(unreach-call) 6.6  3.5  74   330 true 8.3 4.4 150 320 - -
minepump_spec4_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .17  .17  1.7  27 .84 0   false(unreach-call) 6.9  3.7  88   310 true 7.8 4.3 160 320 - -
minepump_spec4_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .18  .18  1.8  27 .84 0   false(unreach-call) 7.0  3.8  82   320 true 8.5 4.5 150 330 - -
minepump_spec4_product45_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .18  .18  1.7  26 .84 0   false(unreach-call) 7.0  3.7  130   310 true 8.3 4.4 150 320 - -
minepump_spec4_product46_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .16  .16  1.9  27 .84 0   false(unreach-call) 7.1  3.8  120   330 true 7.6 4.2 140 320 - -
minepump_spec4_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .17  .17  1.7  27 .84 0   false(unreach-call) 6.9  3.7  85   310 true 8.1 4.4 150 320 - -
minepump_spec4_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .16  .16  1.9  27 .84 0   false(unreach-call) 6.9  3.7  130   310 true 9.3 4.9 180 330 - -
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .34  .33  4.2  30 .99 0   true 5.2  2.8  86   290 true 8.6 4.6 130 330 - -
minepump_spec1_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .10  1.3  26 .84 0   - - out of memory 360    340    6200   7000 true 11   6.1 180 380
minepump_spec1_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.1  26 .84 0   - - out of memory 320    300    3100   7000 true 11   6.0 180 370
minepump_spec1_product03_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 890     890     13000    15000 .84 0   - - error (invalid witness file) .51 .32 9.5 41 error (invalid witness file) 6.7 3.6 120 320
minepump_spec1_product04_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     11000    15000 .84 0   - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 5.9 3.2 110 300
minepump_spec1_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.1  26 .95 0   - - out of memory 270    260    3200   7000 true 11   5.9 140 360
minepump_spec1_product06_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 860     860     13000    15000 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.1 3.3 140 300
minepump_spec1_product07_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    14000 .84 0   - - error (invalid witness file) .50 .33 10   40 error (invalid witness file) 5.6 3.0 110 280
minepump_spec1_product08_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     11000    15000 .84 0   - - error (invalid witness file) .47 .30 9.9 39 error (invalid witness file) 6.1 3.2 130 300
minepump_spec1_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.3  26 .84 0   - - out of memory 360    340    4000   7000 true 12   6.7 160 370
minepump_spec1_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  .97 26 .84 0   - - out of memory 340    320    7700   7000 true 11   6.0 170 370
minepump_spec1_product11_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 890     890     9700    15000 .84 0   - - error (invalid witness file) .52 .33 9.7 42 error (invalid witness file) 6.0 3.2 98 300
minepump_spec1_product12_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     10000    15000 .84 0   - - error (invalid witness file) .51 .33 9.2 42 error (invalid witness file) 5.9 3.2 110 300
minepump_spec1_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .10  1.2  26 .84 0   - - out of memory 290    270    4900   7000 true 9.9 5.4 190 360
minepump_spec1_product14_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 890     890     11000    15000 .84 0   - - error (invalid witness file) .52 .34 9.0 39 error (invalid witness file) 5.6 3.0 100 290
minepump_spec1_product15_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.5 3.4 110 320
minepump_spec1_product16_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     12000    15000 .84 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.5 3.4 120 310
minepump_spec1_product17_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 410     410     5300    15000 .84 0   - - error (invalid witness file) .59 .39 6.5 39 error (invalid witness file) 6.6 3.5 100 290
minepump_spec1_product18_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 810     810     11000    15000 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.9 3.2 110 300
minepump_spec1_product19_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 840     840     12000    15000 .84 0   - - error (invalid witness file) .51 .33 9.4 41 error (invalid witness file) 6.4 3.4 110 300
minepump_spec1_product20_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760     760     8300    15000 .84 0   - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 5.7 3.0 100 300
minepump_spec1_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.4  26 .84 0   - - out of memory 240    230    4200   7000 true 10   5.7 150 370
minepump_spec1_product22_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 680     670     8600    15000 .84 0   - - error (invalid witness file) .51 .34 7.6 40 error (invalid witness file) 5.6 3.0 120 290
minepump_spec1_product23_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 870     870     10000    15000 .99 0   - - error (invalid witness file) .47 .31 7.9 39 error (invalid witness file) 6.1 3.2 120 300
minepump_spec1_product24_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 710     710     9000    15000 .84 0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 7.2 3.8 100 310
minepump_spec1_product25_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 410     410     5700    15000 .84 0   - - error (invalid witness file) .52 .35 7.0 40 error (invalid witness file) 6.0 3.2 110 300
minepump_spec1_product26_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 800     800     10000    15000 .84 0   - - error (invalid witness file) .58 .37 12   44 error (invalid witness file) 5.7 3.1 110 290
minepump_spec1_product27_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 870     870     11000    15000 .84 0   - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 6.4 3.4 120 300
minepump_spec1_product28_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 780     780     9300    15000 .84 0   - - error (invalid witness file) .48 .31 7.1 41 error (invalid witness file) 6.3 3.3 110 300
minepump_spec1_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  27 .84 0   - - out of memory 220    210    3400   7000 true 11   6.1 180 370
minepump_spec1_product30_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 680     680     8600    15000 .84 0   - - error (invalid witness file) .50 .32 8.9 40 error (invalid witness file) 6.0 3.2 110 300
minepump_spec1_product31_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     9800    15000 .84 0   - - error (invalid witness file) .47 .30 8.4 39 error (invalid witness file) 6.1 3.2 110 310
minepump_spec1_product32_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 710     710     8900    15000 .84 0   - - error (invalid witness file) .50 .31 10   40 error (invalid witness file) 6.6 3.4 130 310
minepump_spec1_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect .16  .16  1.5  27 .84 0   - - out of memory 340    320    5600   7000 true 20   11   220 520
minepump_spec1_product46_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 650     650     8200    15000 .84 0   - - error (invalid witness file) .50 .33 11   42 error (invalid witness file) 5.9 3.1 110 300
minepump_spec1_product47_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 810     810     11000    15000 .84 0   - - error (invalid witness file) .55 .35 8.5 39 error (invalid witness file) 6.2 3.3 120 300
minepump_spec1_product48_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 720     720     7800    15000 .84 0   - - error (invalid witness file) .50 .32 9.9 39 error (invalid witness file) 6.0 3.2 110 300
minepump_spec1_product57_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    11000 .84 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.6 3.5 110 310
minepump_spec1_product58_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     9600    10000 .84 0   - - error (invalid witness file) .52 .35 7.8 43 error (invalid witness file) 6.9 3.7 130 310
minepump_spec1_product59_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    14000 .84 0   - - error (invalid witness file) .47 .32 4.5 39 error (invalid witness file) 6.6 3.5 130 320
minepump_spec1_product60_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    12000 .84 0   - - error (invalid witness file) .52 .34 7.0 40 error (invalid witness file) 6.0 3.2 100 300
minepump_spec1_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.9  27 .84 0   - - out of memory 280    260    3300   7000 true 31   17   420 640
minepump_spec1_product62_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 480     480     5800    15000 .84 0   - - error (invalid witness file) .51 .32 8.6 39 error (invalid witness file) 6.1 3.2 120 310
minepump_spec1_product63_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     1900    6600 .84 0   - - error (invalid witness file) .52 .34 6.8 40 error (invalid witness file) 6.1 3.2 90 300
minepump_spec1_product64_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 600     600     7500    15000 .84 0   - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.3 3.4 120 300
minepump_spec2_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.2  26 .84 0   - - out of memory 750    730    8700   7000 true 13   7.2 200 490
minepump_spec2_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  26 .84 0   - - out of memory 700    690    8400   7000 true 14   7.9 210 490
minepump_spec2_product03_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 770     770     10000    15000 .84 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.0 3.2 110 300
minepump_spec2_product04_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760     760     9600    15000 .84 0   - - error (invalid witness file) .48 .31 8.7 39 error (invalid witness file) 6.2 3.3 110 290
minepump_spec2_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.4  26 .84 0   - - out of memory 290    270    4100   7000 true 11   5.9 190 370
minepump_spec2_product06_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 860     860     10000    15000 .84 0   - - error (invalid witness file) .61 .38 8.2 39 error (invalid witness file) 5.7 3.0 85 300
minepump_spec2_product07_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     8200    11000 .84 0   - - error (invalid witness file) .65 .41 9.4 42 error (invalid witness file) 6.0 3.2 120 300
minepump_spec2_product08_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2200    5000 .99 0   - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.8 3.1 100 290
minepump_spec2_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.2  26 .84 0   - - out of memory 760    740    6900   7000 true 13   7.4 160 480
minepump_spec2_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .099 1.4  26 .84 0   - - out of memory 800    780    8300   7000 true 15   8.0 250 520
minepump_spec2_product11_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 790     790     9200    15000 .84 0   - - error (invalid witness file) .50 .32 9.3 39 error (invalid witness file) 5.8 3.1 93 300
minepump_spec2_product12_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 790     790     9900    15000 .84 0   - - error (invalid witness file) .60 .38 5.1 39 error (invalid witness file) 6.2 3.3 110 300
minepump_spec2_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.3  26 .84 0   - - out of memory 280    260    3400   7000 true 11   5.7 200 360
minepump_spec2_product14_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 860     860     13000    15000 .84 0   - - error (invalid witness file) .56 .37 9.1 39 error (invalid witness file) 6.1 3.3 110 300
minepump_spec2_product15_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    15000 .84 0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.0 3.2 120 300
minepump_spec2_product16_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 810     810     11000    15000 .84 0   - - error (invalid witness file) .55 .36 12   43 error (invalid witness file) 6.4 3.3 120 310
minepump_spec2_product17_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 440     440     5200    15000 .84 0   - - error (invalid witness file) .51 .33 6.8 39 error (invalid witness file) 6.4 3.5 89 290
minepump_spec2_product18_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 820     820     9800    15000 .84 0   - - error (invalid witness file) .49 .32 6.8 39 error (invalid witness file) 6.1 3.3 120 300
minepump_spec2_product19_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 790     790     9700    15000 .84 0   - - error (invalid witness file) .58 .38 8.0 39 error (invalid witness file) 6.1 3.2 110 300
minepump_spec2_product20_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 690     690     8800    15000 .84 0   - - error (invalid witness file) .50 .33 8.5 39 error (invalid witness file) 6.3 3.3 120 310
minepump_spec2_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.4  27 .84 0   - - out of memory 210    200    3400   7000 true 11   5.8 160 360
minepump_spec2_product22_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 690     680     8000    15000 .84 0   - - error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.3 3.3 100 310
minepump_spec2_product23_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 820     820     9700    15000 .84 0   - - error (invalid witness file) .54 .36 13   40 error (invalid witness file) 6.8 3.6 130 320
minepump_spec2_product24_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     8800    15000 .84 0   - - error (invalid witness file) .59 .38 5.2 42 error (invalid witness file) 7.1 3.7 93 310
minepump_spec2_product25_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 450     450     5400    15000 .84 0   - - error (invalid witness file) .53 .34 13   44 error (invalid witness file) 6.6 3.5 110 320
minepump_spec2_product26_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 780     780     9100    15000 .84 0   - - error (invalid witness file) .57 .36 11   43 error (invalid witness file) 5.4 2.9 100 290
minepump_spec2_product27_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750     750     9300    15000 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.4 2.9 92 290
minepump_spec2_product28_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 720     720     10000    15000 .84 0   - - error (invalid witness file) .54 .36 9.5 42 error (invalid witness file) 6.1 3.2 120 300
minepump_spec2_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.1  27 .84 0   - - out of memory 230    220    5300   7000 true 11   5.8 200 370
minepump_spec2_product30_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     8400    15000 .84 0   - - error (invalid witness file) .53 .34 11   39 error (invalid witness file) 6.4 3.3 120 300
minepump_spec2_product31_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 860     860     11000    15000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.2 110 300
minepump_spec2_product32_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 660     660     8400    15000 .84 0   - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.9 3.6 140 320
minepump_spec2_product37_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760     750     9400    15000 .84 0   - - error (invalid witness file) .56 .36 10   42 error (invalid witness file) 6.0 3.2 110 300
minepump_spec2_product38_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     9500    15000 .84 0   - - error (invalid witness file) .62 .40 4.8 40 error (invalid witness file) 6.4 3.4 120 300
minepump_spec2_product39_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 830     830     11000    15000 .84 0   - - error (invalid witness file) .62 .41 7.7 40 error (invalid witness file) 5.8 3.1 120 290
minepump_spec2_product40_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760     760     12000    15000 .84 0   - - error (invalid witness file) .54 .35 13   43 error (invalid witness file) 6.0 3.2 100 300
minepump_spec2_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.7  27 .84 0   - - out of memory 320    300    4100   7000 true 24   13   300 630
minepump_spec2_product46_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 630     630     7800    15000 .84 0   - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.2 3.3 93 300
minepump_spec2_product47_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 790     790     12000    15000 .84 0   - - error (invalid witness file) .47 .32 11   39 error (invalid witness file) 5.6 3.0 100 290
minepump_spec2_product48_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 720     720     11000    15000 .84 0   - - error (invalid witness file) .46 .32 3.9 40 error (invalid witness file) 6.4 3.4 120 310
minepump_spec2_product49_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    11000 .84 0   - - error (invalid witness file) .51 .33 6.6 40 error (invalid witness file) 5.8 3.1 89 300
minepump_spec2_product50_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    12000 .84 0   - - error (invalid witness file) .57 .36 7.8 43 error (invalid witness file) 6.6 3.5 120 310
minepump_spec2_product51_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .71 .44 7.6 42 error (invalid witness file) 6.5 3.4 100 330
minepump_spec2_product52_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     10000    12000 .84 0   - - error (invalid witness file) .59 .37 12   42 error (invalid witness file) 5.5 3.0 84 290
minepump_spec2_product53_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 520     520     5800    15000 .84 0   - - error (invalid witness file) .48 .32 9.0 40 error (invalid witness file) 6.7 3.5 130 300
minepump_spec2_product54_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 500     500     6000    15000 .84 0   - - error (invalid witness file) .50 .32 6.2 41 error (invalid witness file) 6.0 3.2 130 300
minepump_spec2_product55_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 630     630     8200    15000 .99 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.2 3.3 110 300
minepump_spec2_product56_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 580     580     8200    15000 .84 0   - - error (invalid witness file) .50 .33 9.2 39 error (invalid witness file) 6.2 3.3 130 300
minepump_spec2_product57_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .50 .33 12   41 error (invalid witness file) 6.2 3.3 140 300
minepump_spec2_product58_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .48 .30 7.4 39 error (invalid witness file) 5.5 3.0 120 290
minepump_spec2_product59_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    14000 .87 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.1 3.2 90 290
minepump_spec2_product60_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    14000 .84 0   - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.1 3.2 120 300
minepump_spec2_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.9  27 .84 0   - - out of memory 240    230    2200   7000 true 22   12   270 630
minepump_spec2_product62_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 480     480     5900    15000 .84 0   - - error (invalid witness file) .54 .35 4.6 41 error (invalid witness file) 5.9 3.2 130 300
minepump_spec2_product63_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 590     590     8100    15000 .84 0   - - error (invalid witness file) .48 .30 8.9 39 error (invalid witness file) 6.0 3.2 110 300
minepump_spec2_product64_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 540     540     8200    15000 .84 0   - - error (invalid witness file) .47 .31 9.7 39 error (invalid witness file) 6.2 3.3 120 300
minepump_spec3_product33_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  26 .84 0   - - out of memory 320    300    4100   7000 true 13   7.2 200 460
minepump_spec3_product34_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 690     690     11000    15000 .92 0   - - error (invalid witness file) .56 .35 12   40 error (invalid witness file) 6.6 3.5 130 300
minepump_spec3_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.7  26 .84 0   - - out of memory 270    250    4400   7000 true 23   12   370 590
minepump_spec3_product38_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 640     640     8100    15000 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.2 3.3 110 300
minepump_spec3_product41_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.5  27 .84 0   - - out of memory 320    310    4600   7000 true 15   8.0 230 540
minepump_spec3_product42_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 780     780     9200    15000 .84 0   - - error (invalid witness file) .51 .33 7.4 41 error (invalid witness file) 6.4 3.3 120 300
minepump_spec3_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.5  27 .84 0   - - out of memory 300    290    2700   7000 true 23   12   300 550
minepump_spec3_product46_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2500    6400 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.4 3.4 87 300
minepump_spec3_product49_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    5200 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.8 3.1 110 290
minepump_spec3_product50_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     1800    2200 .84 0   - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 6.2 3.3 110 300
minepump_spec3_product53_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    8200 .84 0   - - error (invalid witness file) .50 .33 9.3 39 error (invalid witness file) 6.2 3.3 130 300
minepump_spec3_product54_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2500    3100 .84 0   - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 5.8 3.1 95 300
minepump_spec3_product57_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    4200 .84 0   - - error (invalid witness file) .52 .35 12   40 error (invalid witness file) 6.4 3.4 130 300
minepump_spec3_product58_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    4900 .84 0   - - error (invalid witness file) .58 .37 8.6 41 error (invalid witness file) 5.9 3.1 100 300
minepump_spec3_product61_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    7200 .84 0   - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.1 3.2 110 290
minepump_spec3_product62_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    8000 .84 0   - - error (invalid witness file) .54 .34 8.0 42 error (invalid witness file) 5.9 3.1 100 290
minepump_spec4_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .099 1.2  26 .84 0   - - out of memory 310    290    3900   7000 true 10   5.4 160 350
minepump_spec4_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  26 .99 0   - - out of memory 320    310    3800   7000 true 10   5.4 150 350
minepump_spec4_product03_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    15000 .84 0   - - error (invalid witness file) .54 .36 4.1 41 error (invalid witness file) 6.3 3.3 120 300
minepump_spec4_product04_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 890     890     12000    15000 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.8 3.1 130 290
minepump_spec4_product05_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    14000 .84 0   - - error (invalid witness file) .50 .34 4.3 41 error (invalid witness file) 7.0 3.7 140 310
minepump_spec4_product06_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     9900    15000 .84 0   - - error (invalid witness file) .53 .35 12   40 error (invalid witness file) 6.1 3.2 100 300
minepump_spec4_product07_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     10000    13000 .84 0   - - error (invalid witness file) .58 .36 6.9 40 error (invalid witness file) 5.6 3.0 87 290
minepump_spec4_product08_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .54 .35 9.3 40 error (invalid witness file) 5.9 3.1 97 300
minepump_spec4_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .10  1.1  26 .84 0   - - out of memory 310    290    3600   7000 true 10   5.4 150 360
minepump_spec4_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .10  1.1  26 .84 0   - - out of memory 340    320    4300   7000 true 9.9 5.3 160 350
minepump_spec4_product11_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    15000 .84 0   - - error (invalid witness file) .56 .36 11   43 error (invalid witness file) 6.2 3.3 110 290
minepump_spec4_product12_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2000    4500 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.1 3.2 120 300
minepump_spec4_product13_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .57 .37 9.5 39 error (invalid witness file) 6.1 3.2 120 300
minepump_spec4_product14_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     1800    4400 .84 0   - - error (invalid witness file) .51 .32 9.3 43 error (invalid witness file) 6.2 3.3 130 290
minepump_spec4_product15_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .56 .37 5.8 39 error (invalid witness file) 5.6 3.0 130 290
minepump_spec4_product16_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    15000 .84 0   - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.0 3.2 120 300
minepump_spec4_product17_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 560     550     7200    15000 .92 0   - - error (invalid witness file) .49 .31 10   40 error (invalid witness file) 5.9 3.1 91 290
minepump_spec4_product18_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    15000 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.7 3.1 92 300
minepump_spec4_product19_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 800     790     11000    15000 .84 0   - - error (invalid witness file) .52 .33 7.6 39 error (invalid witness file) 6.1 3.2 95 300
minepump_spec4_product20_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 730     730     9700    15000 .84 0   - - error (invalid witness file) .52 .35 4.4 43 error (invalid witness file) 6.0 3.2 110 300
minepump_spec4_product21_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 340     330     4100    15000 .84 0   - - error (invalid witness file) .53 .33 12   41 error (invalid witness file) 6.5 3.4 120 300
minepump_spec4_product22_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 660     660     8400    15000 .84 0   - - error (invalid witness file) .61 .39 9.5 41 error (invalid witness file) 5.7 3.0 99 300
minepump_spec4_product23_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 680     680     9200    15000 .84 0   - - error (invalid witness file) .51 .35 5.4 39 error (invalid witness file) 6.2 3.3 120 300
minepump_spec4_product24_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     7700    15000 .84 0   - - error (invalid witness file) .62 .39 7.7 39 error (invalid witness file) 5.7 3.0 120 290
minepump_spec4_product25_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 530     530     6300    15000 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.6 3.0 100 290
minepump_spec4_product26_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.2 3.2 130 300
minepump_spec4_product27_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 780     780     9700    15000 .84 0   - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 5.6 3.0 110 290
minepump_spec4_product28_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750     750     9000    15000 .84 0   - - error (invalid witness file) .59 .38 6.8 40 error (invalid witness file) 6.2 3.3 110 300
minepump_spec4_product29_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 340     330     4500    15000 .84 0   - - error (invalid witness file) .48 .30 4.0 42 error (invalid witness file) 6.0 3.2 110 300
minepump_spec4_product30_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     8200    15000 .84 0   - - error (invalid witness file) .53 .34 6.6 40 error (invalid witness file) 6.2 3.3 110 310
minepump_spec4_product31_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 680     680     9800    15000 .84 0   - - error (invalid witness file) .47 .30 8.2 39 error (invalid witness file) 5.9 3.2 120 300
minepump_spec4_product32_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 660     660     9700    15000 .84 0   - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 6.6 3.5 130 310
minepump_spec4_product49_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .52 .33 9.1 40 error (invalid witness file) 6.0 3.2 120 300
minepump_spec4_product50_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    14000 .84 0   - - error (invalid witness file) .51 .33 12   42 error (invalid witness file) 6.4 3.4 110 310
minepump_spec4_product51_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    15000 .84 0   - - error (invalid witness file) .49 .33 6.4 39 error (invalid witness file) 6.3 3.4 100 300
minepump_spec4_product52_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    13000 .84 0   - - error (invalid witness file) .52 .33 7.7 43 error (invalid witness file) 6.0 3.2 110 300
minepump_spec4_product53_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 630     620     9000    15000 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.2 130 290
minepump_spec4_product54_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 630     630     8000    15000 .84 0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.0 3.2 84 310
minepump_spec4_product55_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 670     670     7900    15000 .84 0   - - error (invalid witness file) .48 .31 9.4 39 error (invalid witness file) 5.9 3.1 110 310
minepump_spec4_product56_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 800     800     10000    15000 .84 0   - - error (invalid witness file) .48 .31 8.5 40 error (invalid witness file) 6.1 3.2 110 290
minepump_spec4_product57_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    13000 .84 0   - - error (invalid witness file) .60 .38 6.6 41 error (invalid witness file) 6.1 3.2 130 300
minepump_spec4_product58_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     10000    13000 .84 0   - - error (invalid witness file) .59 .38 6.0 41 error (invalid witness file) 7.3 3.8 120 320
minepump_spec4_product59_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    15000 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.7 3.5 120 310
minepump_spec4_product60_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     10000    13000 .84 0   - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.4 3.3 110 300
minepump_spec4_product61_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 600     600     7200    15000 .84 0   - - error (invalid witness file) .53 .36 8.7 39 error (invalid witness file) 5.8 3.1 93 290
minepump_spec4_product62_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 600     600     7000    15000 .84 0   - - error (invalid witness file) .49 .31 9.9 39 error (invalid witness file) 6.2 3.3 100 310
minepump_spec4_product63_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 640     630     8300    15000 .84 0   - - error (invalid witness file) .49 .31 6.9 40 error (invalid witness file) 6.8 3.5 130 310
minepump_spec4_product64_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 740     740     8800    15000 .84 0   - - error (invalid witness file) .57 .38 8.6 40 error (invalid witness file) 7.0 3.7 120 330
minepump_spec5_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.1  26 .84 0   - - true 10    5.4  190   400 true 12   6.3 150 370
minepump_spec5_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect .10  .10  1.1  26 .84 0   - - true 11    5.7  170   430 true 11   5.9 170 370
minepump_spec5_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.2  26 .84 0   - - true 13    6.7  130   440 true 9.3 5.1 150 350
minepump_spec5_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect .41  .40  .82 26 .84 0   - - true 12    6.1  250   460 true 9.7 5.2 170 340
minepump_spec5_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.4  27 .84 0   - - true 12    6.2  110   480 true 11   5.7 170 360
minepump_spec5_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.3  26 .84 0   - - true 13    7.0  120   520 true 10   5.7 160 360
minepump_spec5_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.3  26 .84 0   - - true 16    8.5  120   520 true 11   6.0 180 370
minepump_spec5_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.2  26 .84 0   - - true 12    6.3  150   490 true 9.8 5.3 170 360
minepump_spec5_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.3  26 .84 0   - - true 9.7  5.1  140   380 true 10   5.6 160 350
minepump_spec5_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.3  27 .84 0   - - true 11    6.0  160   420 true 11   5.8 200 360
minepump_spec5_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .10  1.2  26 .84 0   - - true 11    5.8  150   460 true 9.7 5.2 130 350
minepump_spec5_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.0  26 .84 0   - - true 13    6.9  190   450 true 11   5.7 180 350
minepump_spec5_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.2  26 .84 0   - - true 13    6.5  190   480 true 10   5.6 170 370
minepump_spec5_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.3  26 .84 0   - - true 13    7.0  140   490 true 10   5.6 160 370
minepump_spec5_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  26 .84 0   - - true 13    6.8  190   510 true 11   5.8 170 370
minepump_spec5_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.4  26 .84 0   - - true 17    9.0  170   520 true 11   5.7 160 360
minepump_spec5_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.2  26 .84 0   - - true 14    7.5  170   530 true 11   5.7 160 370
minepump_spec5_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.1  27 .84 0   - - true 13    7.1  210   560 true 11   5.9 170 360
minepump_spec5_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect .13  .13  1.5  27 .84 0   - - true 13    7.0  150   530 true 11   5.8 170 360
minepump_spec5_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.4  27 .84 0   - - true 15    8.0  180   530 true 9.5 5.1 150 340
minepump_spec5_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.4  27 .84 0   - - true 16    9.2  220   1100 true 10   5.6 160 360
minepump_spec5_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .12  1.4  27 .84 0   - - true 21    12    320   1300 true 11   5.8 150 370
minepump_spec5_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect .45  .45  1.0  27 .84 0   - - true 21    12    220   1200 true 11   5.9 150 360
minepump_spec5_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.1  27 .84 0   - - true 17    9.7  200   1200 true 10   5.4 160 350
minepump_spec5_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.5  27 .84 0   - - true 13    6.6  120   510 true 10   5.6 170 370
minepump_spec5_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect .12  .11  1.3  27 .84 0   - - true 13    7.2  140   550 true 11   5.7 190 370
minepump_spec5_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect .14  .14  1.2  27 .84 0   - - true 14    7.5  190   520 true 11   6.1 190 370
minepump_spec5_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.1  27 .84 0   - - true 12    6.6  140   550 true 10   5.5 190 350
minepump_spec5_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect .11  .11  1.6  27 .84 0   - - true 16    9.1  170   1100 true 10   5.6 210 360
minepump_spec5_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect .45  .45  .87 27 .84 0   - - true 21    12    230   1300 true 11   5.9 190 360
minepump_spec5_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.4  27 .84 0   - - true 16    9.4  220   1200 true 13   6.8 140 360
minepump_spec5_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect .15  .15  1.5  27 .84 0   - - true 18    10    290   1200 true 10   5.4 140 360
minepump_spec5_product33_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    12000 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.3 3.3 120 300
minepump_spec5_product34_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 850     850     10000    15000 .84 0   - - error (invalid witness file) .50 .33 9.0 40 error (invalid witness file) 5.5 3.0 110 290
minepump_spec5_product35_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    13000 .84 0   - - error (invalid witness file) .51 .34 12   39 error (invalid witness file) 5.9 3.1 91 310
minepump_spec5_product36_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    5200 .84 0   - - error (invalid witness file) .59 .38 7.9 39 error (invalid witness file) 5.9 3.1 110 300
minepump_spec5_product37_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    5400 .84 0   - - error (invalid witness file) .47 .31 6.2 40 error (invalid witness file) 5.8 3.1 120 300
minepump_spec5_product38_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2700    2100 .84 0   - - error (invalid witness file) .48 .31 8.9 39 error (invalid witness file) 5.9 3.1 100 300
minepump_spec5_product39_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    7400 .84 0   - - error (invalid witness file) .58 .38 7.1 40 error (invalid witness file) 5.6 3.0 120 290
minepump_spec5_product40_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    6700 .84 0   - - error (invalid witness file) .63 .40 12   45 error (invalid witness file) 6.9 3.6 120 300
minepump_spec5_product41_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    11000 .84 0   - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 6.2 3.3 120 310
minepump_spec5_product42_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    13000 .84 0   - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.3 3.3 130 300
minepump_spec5_product43_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    11000 .99 0   - - error (invalid witness file) .65 .41 8.6 40 error (invalid witness file) 6.0 3.2 130 300
minepump_spec5_product44_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    4800 .84 0   - - error (invalid witness file) .49 .32 7.1 40 error (invalid witness file) 6.2 3.3 130 300
minepump_spec5_product45_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    5600 .84 0   - - error (invalid witness file) .54 .35 13   43 error (invalid witness file) 5.9 3.2 110 310
minepump_spec5_product46_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    6600 .84 0   - - error (invalid witness file) .54 .34 9.2 43 error (invalid witness file) 5.6 3.0 110 290
minepump_spec5_product47_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    7000 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 8.4 4.4 100 300
minepump_spec5_product48_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     2600    2300 .84 0   - - error (invalid witness file) .55 .36 8.7 39 error (invalid witness file) 6.1 3.2 110 300
minepump_spec5_product49_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    7300 .84 0   - - error (invalid witness file) .58 .38 11   40 error (invalid witness file) 5.6 3.0 80 310
minepump_spec5_product50_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    8400 .84 0   - - error (invalid witness file) .58 .37 5.5 40 error (invalid witness file) 6.5 3.4 130 300
minepump_spec5_product51_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    9700 .84 0   - - error (invalid witness file) .58 .37 11   43 error (invalid witness file) 6.2 3.3 140 310
minepump_spec5_product52_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    6000 .84 0   - - error (invalid witness file) .58 .36 8.7 39 error (invalid witness file) 6.0 3.1 120 310
minepump_spec5_product53_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    11000 .84 0   - - error (invalid witness file) .50 .32 6.9 40 error (invalid witness file) 7.2 3.8 120 320
minepump_spec5_product54_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .48 .32 8.0 40 error (invalid witness file) 5.7 3.1 110 300
minepump_spec5_product55_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    14000 .84 0   - - error (invalid witness file) .47 .31 12   40 error (invalid witness file) 5.9 3.1 130 300
minepump_spec5_product56_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    8800 .84 0   - - error (invalid witness file) .63 .40 8.3 41 error (invalid witness file) 6.5 3.4 110 300
minepump_spec5_product57_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    6200 .84 0   - - error (invalid witness file) .50 .32 5.8 40 error (invalid witness file) 5.9 3.2 130 300
minepump_spec5_product58_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    7400 .84 0   - - error (invalid witness file) .49 .31 9.5 40 error (invalid witness file) 6.0 3.2 130 300
minepump_spec5_product59_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    8100 .84 0   - - error (invalid witness file) .63 .40 6.7 40 error (invalid witness file) 6.4 3.4 140 300
minepump_spec5_product60_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     12000    6300 .84 0   - - error (invalid witness file) .52 .34 7.1 40 error (invalid witness file) 6.2 3.2 120 300
minepump_spec5_product61_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     13000    9900 .84 0   - - error (invalid witness file) .48 .31 6.8 39 error (invalid witness file) 6.4 3.3 110 300
minepump_spec5_product62_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    11000 .84 0   - - error (invalid witness file) .53 .34 8.6 39 error (invalid witness file) 6.4 3.4 120 310
minepump_spec5_product63_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     10000    12000 .84 0   - - error (invalid witness file) .52 .34 9.2 40 error (invalid witness file) 6.8 3.6 130 310
minepump_spec5_product64_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    9300 .84 0   - - error (invalid witness file) .59 .37 8.7 41 error (invalid witness file) 6.1 3.2 120 300
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     11000    12000 .84 0   - - error (invalid witness file) .48 .32 8.6 40 error (invalid witness file) 6.1 3.3 100 300
../../sv-benchmarks/c/product-lines/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 597 437 150000 150000 1800000 2200000 510 0   597 6800 4800 100000 340000   597 2500 1400 42000 96000   597 15000 13000 200000 380000   597 14000 9000 150000 520000  
    correct results 283 437 1800 1800 22000 23000 240 0   129 1000 550 15000 47000   129 1100 600 19000 44000   126 15000 13000 190000 370000   95 13000 8400 130000 470000  
        correct true 154 308 1700 1700 21000 18000 130 0   0 0 0 0 0   129 0 0 0 0   126 15000 13000 190000 370000   95 13000 8400 130000 470000  
        correct false 129 129 140 140 1500 5100 110 0   129 1000 550 15000 47000   0 1100 600 19000 44000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 134 0 4700 4700 53000 26000 110 0   97 5700 4200 88000 290000   134 1400 760 22000 52000   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 134 0 4700 4700 53000 26000 110 0   0 5700 4200 88000 290000   0 1400 760 22000 52000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 437
Run set sv-comp17.ReachSafety-ProductLines