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