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