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