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