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 inspect 230 220   2200 910 31     0      error (invalid witness file) .51 .33 3.5 40 error (invalid witness file) 6.7 3.5 120 310 - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   1800 920 31     0      error (invalid witness file) .49 .33 8.6 41 error (invalid witness file) 6.1 3.3 130 300 - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 230 220   2200 920 30     0      error (invalid witness file) .49 .31 10   40 error (invalid witness file) 5.8 3.1 110 290 - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2000 930 33     0      error (invalid witness file) .52 .34 14   40 error (invalid witness file) 6.7 3.6 140 310 - -
minepump_spec3_product07_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 210   1600 960 18     0      error (invalid witness file) .53 .32 13   40 error (invalid witness file) 6.3 3.3 130 290 - -
minepump_spec3_product08_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2200 970 33     0      error (invalid witness file) .50 .33 13   40 error (invalid witness file) 7.8 4.1 140 310 - -
minepump_spec3_product09_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 210   1700 870 27     0      error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.8 3.1 120 300 - -
minepump_spec3_product10_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 220   1800 890 30     0      error (invalid witness file) .49 .32 13   40 error (invalid witness file) 5.9 3.2 120 300 - -
minepump_spec3_product11_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 230 220   1900 910 30     0      error (invalid witness file) .48 .30 8.0 39 error (invalid witness file) 5.7 3.0 92 300 - -
minepump_spec3_product12_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2000 920 31     0      error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.1 3.2 110 300 - -
minepump_spec3_product13_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 230 220   2600 920 32     0      error (invalid witness file) .57 .36 13   43 error (invalid witness file) 5.6 3.0 97 300 - -
minepump_spec3_product14_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 210 200   2100 940 19     0      error (invalid witness file) .54 .33 12   41 error (invalid witness file) 6.2 3.3 120 300 - -
minepump_spec3_product15_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2400 950 30     0      error (invalid witness file) .53 .33 11   39 error (invalid witness file) 6.6 3.5 130 310 - -
minepump_spec3_product16_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 240   2800 970 33     0      error (invalid witness file) .52 .35 4.6 40 error (invalid witness file) 6.0 3.1 120 290 - -
minepump_spec3_product17_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2100 920 33     .098  error (invalid witness file) .55 .35 10   42 error (invalid witness file) 6.0 3.1 120 300 - -
minepump_spec3_product18_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2200 940 26     0      error (invalid witness file) .53 .35 8.2 42 error (invalid witness file) 6.1 3.2 120 300 - -
minepump_spec3_product19_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2200 940 33     0      error (invalid witness file) .48 .31 7.3 40 error (invalid witness file) 6.3 3.3 120 300 - -
minepump_spec3_product20_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 220   1900 970 18     .033  error (invalid witness file) .49 .32 6.9 40 error (invalid witness file) 5.9 3.1 120 300 - -
minepump_spec3_product21_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2000 940 36     0      error (invalid witness file) .53 .35 4.0 40 error (invalid witness file) 5.6 3.0 100 290 - -
minepump_spec3_product22_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2200 960 28     0      error (invalid witness file) .49 .30 6.5 39 error (invalid witness file) 6.1 3.2 100 300 - -
minepump_spec3_product23_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 260 250   2200 980 35     0      error (invalid witness file) .54 .35 14   44 error (invalid witness file) 6.1 3.2 110 300 - -
minepump_spec3_product24_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 270 260   2600 990 37     0      error (invalid witness file) .47 .32 5.9 39 error (invalid witness file) 6.0 3.2 100 290 - -
minepump_spec3_product25_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2200 920 33     0      error (invalid witness file) .51 .34 5.5 40 error (invalid witness file) 6.1 3.2 130 290 - -
minepump_spec3_product26_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 240 230   2300 930 35     0      error (invalid witness file) .49 .32 6.4 40 error (invalid witness file) 6.0 3.2 120 300 - -
minepump_spec3_product27_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2000 970 34     0      error (invalid witness file) .45 .31 6.0 40 error (invalid witness file) 6.3 3.3 110 300 - -
minepump_spec3_product28_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 210   2100 970 19     0      error (invalid witness file) .57 .36 6.2 39 error (invalid witness file) 5.9 3.1 110 290 - -
minepump_spec3_product29_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 250 240   2400 940 36     0      error (invalid witness file) .50 .33 12   41 error (invalid witness file) 6.3 3.3 130 300 - -
minepump_spec3_product30_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 220 210   1800 960 18     0      error (invalid witness file) .49 .32 3.6 39 error (invalid witness file) 6.2 3.3 120 300 - -
minepump_spec3_product31_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 260 250   2600 980 36     0      error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.8 3.5 110 310 - -
minepump_spec3_product32_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 270 260   2100 1000 36     0      error (invalid witness file) .48 .32 11   40 error (invalid witness file) 5.9 3.1 120 300 - -
minepump_spec3_product35_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 360 350   3000 860 26     0      error (invalid witness file) .55 .36 6.3 42 error (invalid witness file) 6.2 3.3 130 300 - -
minepump_spec3_product36_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 360 360   3100 870 26     .098  error (invalid witness file) .50 .32 9.6 39 error (invalid witness file) 6.2 3.3 110 300 - -
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 19 8.8 160 300 .14  .0041 false(unreach-call) 6.3  3.4  140   350 false(unreach-call) 9.5 5.1 200 330 - -
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 19 9.2 190 300 .25  .0041 false(unreach-call) 6.1  3.3  130   300 false(unreach-call) 9.8 5.2 200 350 - -
minepump_spec3_product43_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 360 350   3000 1100 10     0      error (invalid witness file) .54 .35 7.1 40 error (invalid witness file) 6.1 3.2 120 300 - -
minepump_spec3_product44_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 360 350   3500 1100 17     .098  error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.4 3.4 130 310 - -
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 19 9.3 160 300 .14  0      false(unreach-call) 6.2  3.3  130   310 false(unreach-call) 10   5.4 200 370 - -
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 20 9.6 170 300 .14  .0041 false(unreach-call) 5.9  3.2  120   290 false(unreach-call) 9.5 5.1 130 340 - -
minepump_spec3_product51_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 510 500   3700 740 25     0      error (invalid witness file) .45 .30 6.5 39 error (invalid witness file) 5.7 3.0 110 290 - -
minepump_spec3_product52_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 500 490   3900 740 25     0      error (invalid witness file) .53 .34 3.6 42 error (invalid witness file) 7.0 3.7 130 310 - -
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 21 11   180 330 .15  .0041 false(unreach-call) 6.3  3.4  130   320 false(unreach-call) 10   5.5 180 360 - -
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 58 48   570 660 1.2   .0041 false(unreach-call) 6.3  3.4  130   340 false(unreach-call) 10   5.4 210 340 - -
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 20 10   200 320 .14  .0041 false(unreach-call) 6.0  3.2  110   320 false(unreach-call) 10   5.4 200 340 - -
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 20 10   170 330 .14  .0041 false(unreach-call) 7.6  4.1  80   320 false(unreach-call) 9.7 5.1 200 330 - -
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 22 12   180 360 .16  0      false(unreach-call) 6.1  3.3  110   320 false(unreach-call) 11   5.8 200 360 - -
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 22 12   180 360 .16  0      false(unreach-call) 6.0  3.2  110   310 false(unreach-call) 11   5.6 180 360 - -
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 26 14   270 390 .22  .0041 false(unreach-call) 7.2  3.8  130   340 false(unreach-call) 11   5.9 200 370 - -
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 18 7.7 150 330 .15  0      false(unreach-call) 7.1  3.8  150   310 false(unreach-call) 16   8.7 270 420 - -
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 18 7.7 150 330 .15  .10   false(unreach-call) 6.5  3.5  110   290 false(unreach-call) 13   6.8 220 410 - -
minepump_spec4_product35_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 310 300   2500 750 7.4   0      error (invalid witness file) .51 .34 6.2 40 error (invalid witness file) 5.7 3.0 110 300 - -
minepump_spec4_product36_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 310 300   2900 750 8.7   0      error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.4 3.4 120 300 - -
minepump_spec4_product37_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 400 390   3300 1100 15     0      error (invalid witness file) .55 .34 11   42 error (invalid witness file) 5.6 3.0 110 280 - -
minepump_spec4_product38_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 400 390   3000 1200 16     0      error (invalid witness file) .55 .34 11   42 error (invalid witness file) 5.9 3.1 100 300 - -
minepump_spec4_product39_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 400 390   3200 1300 8.3   0      error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.4 3.4 110 290 - -
minepump_spec4_product40_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 400 390   3800 1300 7.3   0      error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.4 3.3 120 300 - -
minepump_spec4_product41_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 330 320   2500 820 17     0      error (invalid witness file) .48 .32 11   40 error (invalid witness file) 5.8 3.1 98 300 - -
minepump_spec4_product42_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 330 320   2800 830 17     0      error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.0 3.2 110 300 - -
minepump_spec4_product43_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 330 320   2600 940 8.7   0      error (invalid witness file) .50 .33 4.6 39 error (invalid witness file) 5.7 3.0 110 290 - -
minepump_spec4_product44_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 340 330   2800 950 16     0      error (invalid witness file) .48 .31 6.5 40 error (invalid witness file) 6.0 3.2 120 290 - -
minepump_spec4_product45_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 440   3600 770 11     0      error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.0 3.2 120 300 - -
minepump_spec4_product46_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   4900 780 11     0      error (invalid witness file) .51 .34 3.8 40 error (invalid witness file) 5.9 3.1 110 300 - -
minepump_spec4_product47_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3900 830 8.7   0      error (invalid witness file) .51 .33 10   43 error (invalid witness file) 6.6 3.5 92 320 - -
minepump_spec4_product48_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3800 830 9.7   0      error (invalid witness file) .49 .31 8.5 39 error (invalid witness file) 6.6 3.5 130 310 - -
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 740 730   5700 1000 4.5   0      error (invalid witness file) .49 .32 7.2 39 error (invalid witness file) 6.0 3.2 110 300 - -
minepump_spec1_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.0 130 560 .053 0      - - out of memory 340    320    4500   7000 true 12   6.6 250 370
minepump_spec1_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 18 5.0 140 580 .053 0      - - out of memory 310    300    4000   7000 true 11   6.3 110 370
minepump_spec1_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.1 150 580 .053 0      - - out of memory 310    290    3500   7000 true 10   5.7 150 370
minepump_spec1_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.7 160 780 .053 0      - - out of memory 320    300    3900   7000 true 10   5.5 190 350
minepump_spec1_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 23 5.9 180 710 .053 0      - - out of memory 280    270    3300   7000 true 11   5.8 240 360
minepump_spec1_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 32 7.8 250 1200 .053 0      - - out of memory 300    290    2900   7000 true 11   6.1 200 370
minepump_spec1_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 34 8.2 240 1300 .053 0      - - out of memory 260    240    3100   7000 true 11   5.8 200 350
minepump_spec1_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 35 8.5 250 1400 .053 0      - - out of memory 270    250    4000   7000 true 9.9 5.3 160 350
minepump_spec1_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 18 4.8 120 580 .053 0      - - out of memory 330    320    3400   7000 true 11   6.2 210 360
minepump_spec1_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 18 4.8 120 560 .053 .0082 - - out of memory 330    310    2900   7000 true 12   6.7 220 360
minepump_spec1_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.4 140 610 .053 0      - - out of memory 310    290    4000   7000 true 11   6.0 190 360
minepump_spec1_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.2 140 610 .053 0      - - out of memory 300    280    2900   7000 true 9.9 5.3 190 350
minepump_spec1_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 25 6.6 160 840 .053 0      - - out of memory 290    280    5400   7000 true 11   5.8 200 370
minepump_spec1_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 35 8.6 230 1400 .053 0      - - out of memory 260    240    3000   7000 true 11   5.8 240 360
minepump_spec1_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 33 8.1 250 1200 .053 .11   - - out of memory 290    270    5300   7000 true 12   6.2 230 360
minepump_spec1_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 34 8.4 230 1400 .053 0      - - out of memory 270    260    4400   7000 true 10   5.4 170 350
minepump_spec1_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 35 8.6 270 1400 .053 0      - - out of memory 450    440    7100   7000 true 12   6.4 190 370
minepump_spec1_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 43 12   310 2200 .053 .0082 - - out of memory 450    430    5200   7000 true 11   6.1 190 380
minepump_spec1_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 42 11   300 2200 .053 0      - - out of memory 360    350    4700   7000 true 13   6.7 240 380
minepump_spec1_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 12   340 2200 .053 0      - - out of memory 390    380    3700   7000 true 10   5.6 200 360
minepump_spec1_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 41 10   290 1500 .053 0      - - out of memory 360    340    4300   7000 true 11   5.9 230 370
minepump_spec1_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 52 15   370 2500 .053 .0082 - - out of memory 500    480    4000   7000 true 11   6.1 240 370
minepump_spec1_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 57 16   360 2500 .053 0      - - out of memory 350    330    5100   7000 true 11   6.1 210 360
minepump_spec1_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 53 16   400 2400 .053 0      - - out of memory 330    310    4300   7000 true 10   5.5 200 340
minepump_spec1_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 34 8.6 240 1400 .053 .0082 - - out of memory 420    400    5300   7000 true 11   6.1 240 370
minepump_spec1_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 42 11   280 1800 .053 .0082 - - out of memory 350    330    5900   7000 true 11   5.9 250 370
minepump_spec1_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 46 12   320 2200 .053 0      - - out of memory 400    380    4700   7000 true 11   6.1 240 360
minepump_spec1_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 42 11   270 2100 .053 0      - - out of memory 420    400    4700   7000 true 10   5.4 210 350
minepump_spec1_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 42 11   280 1700 .053 .11   - - out of memory 340    320    2800   7000 true 11   5.8 200 360
minepump_spec1_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 51 15   370 2400 .053 0      - - out of memory 430    420    9500   7000 true 12   6.3 210 360
minepump_spec1_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 51 15   420 2500 .053 0      - - out of memory 320    310    3100   7000 true 12   6.3 220 370
minepump_spec1_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 51 15   390 2500 .053 0      - - out of memory 320    300    5000   7000 true 11   5.8 200 360
minepump_spec1_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 300   5000 3900 .18  .082  - - out of memory 280    270    2900   7000 true 21   12   430 560
minepump_spec1_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   4800 3800 .18  .082  - - out of memory 290    280    3200   7000 true 31   17   650 640
minepump_spec1_product47_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3500 830 10     0      - - error (invalid witness file) .49 .31 4.9 39 error (invalid witness file) 7.3 3.8 150 330
minepump_spec1_product48_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3600 830 10     0      - - error (invalid witness file) .53 .34 6.5 41 error (invalid witness file) 6.9 3.6 110 320
minepump_spec1_product57_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   3400 820 13     .098  - - error (invalid witness file) .49 .33 6.8 39 error (invalid witness file) 6.0 3.2 100 300
minepump_spec1_product58_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   5000 820 12     0      - - error (invalid witness file) .55 .34 11   40 error (invalid witness file) 6.5 3.4 130 300
minepump_spec1_product59_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   3800 890 8.0   0      - - error (invalid witness file) .50 .33 6.4 40 error (invalid witness file) 5.7 3.1 120 290
minepump_spec1_product60_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   3500 890 9.8   0      - - error (invalid witness file) .50 .33 5.8 40 error (invalid witness file) 6.6 3.4 130 310
minepump_spec1_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   4900 4600 .11  .19   - - out of memory 270    260    4800   7000 true 29   16   560 630
minepump_spec1_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   6300 4700 .18  .0082 - - out of memory 280    260    3900   7000 true 24   13   450 600
minepump_spec1_product63_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4600 840 7.1   0      - - error (invalid witness file) .55 .36 12   43 error (invalid witness file) 6.1 3.2 120 300
minepump_spec1_product64_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4400 850 7.5   0      - - error (invalid witness file) .49 .31 9.8 39 error (invalid witness file) 6.2 3.2 120 290
minepump_spec2_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.1 140 600 .053 0      - - out of memory 800    780    12000   7000 true 14   7.7 290 490
minepump_spec2_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 18 4.9 130 560 .053 0      - - out of memory 690    670    11000   7000 true 14   7.9 310 490
minepump_spec2_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.4 130 620 .053 0      - - out of memory 760    740    6500   7000 true 11   5.6 220 360
minepump_spec2_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.1 150 630 .053 0      - - timeout 910    890    8000   5700 true 10   5.4 220 350
minepump_spec2_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 28 6.9 200 900 .053 0      - - out of memory 290    270    3300   7000 true 11   6.0 210 370
minepump_spec2_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 39 9.9 270 1800 .053 0      - - out of memory 300    280    3000   7000 true 11   6.1 210 360
minepump_spec2_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 37 9.1 250 1700 .053 .49   - - out of memory 270    260    4300   7000 true 11   5.7 210 350
minepump_spec2_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 36 9.5 270 1700 .053 0      - - out of memory 280    260    3000   7000 true 12   6.2 170 340
minepump_spec2_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.4 170 660 .053 0      - - out of memory 770    750    8200   7000 true 14   7.8 310 500
minepump_spec2_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.4 150 600 .053 0      - - out of memory 650    640    6200   7000 true 15   8.1 300 500
minepump_spec2_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.4 160 650 .053 0      - - out of memory 730    710    7200   7000 true 11   5.7 220 360
minepump_spec2_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.5 180 630 .053 0      - - out of memory 880    860    7000   7000 true 11   5.8 200 360
minepump_spec2_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 26 6.7 190 860 .053 0      - - out of memory 260    250    3700   7000 true 16   8.5 170 360
minepump_spec2_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 36 8.7 270 1300 .053 0      - - out of memory 270    250    2500   7000 true 11   6.0 220 370
minepump_spec2_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 36 8.7 290 1300 .053 0      - - out of memory 260    240    2600   7000 true 11   5.7 200 360
minepump_spec2_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 37 9.5 250 1700 .053 0      - - out of memory 300    280    4000   7000 true 10   5.6 210 360
minepump_spec2_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 37 9.6 250 1500 .053 .0082 - - out of memory 410    390    8400   7000 true 11   6.0 210 370
minepump_spec2_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 41 11   320 2200 .053 0      - - out of memory 420    410    5000   7000 true 12   6.2 230 360
minepump_spec2_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 46 12   310 2200 .053 0      - - out of memory 430    410    4700   7000 true 11   6.0 230 380
minepump_spec2_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 49 13   340 2100 .053 .11   - - out of memory 430    410    4400   7000 true 11   5.8 200 360
minepump_spec2_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 40 11   270 1700 .053 0      - - out of memory 360    340    4500   7000 true 11   6.0 230 360
minepump_spec2_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 53 16   400 2500 .053 .0082 - - out of memory 380    360    3600   7000 true 11   6.1 220 360
minepump_spec2_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 53 16   420 2500 .053 .11   - - out of memory 350    340    7000   7000 true 11   5.7 190 360
minepump_spec2_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 54 16   450 2500 .053 0      - - out of memory 310    290    7000   7000 true 11   5.7 230 360
minepump_spec2_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 35 8.9 230 1200 .053 0      - - out of memory 480    460    6600   7000 true 11   6.2 230 370
minepump_spec2_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 11   310 2200 .053 .0082 - - out of memory 450    440    7900   7000 true 11   6.1 240 370
minepump_spec2_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 47 13   340 2200 .053 .11   - - out of memory 400    390    6600   7000 true 11   6.0 200 360
minepump_spec2_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 49 13   330 2200 .053 0      - - out of memory 460    450    5400   7000 true 11   5.7 200 350
minepump_spec2_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 41 10   270 1500 .053 .49   - - out of memory 400    380    6100   7000 true 11   6.0 210 360
minepump_spec2_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 56 16   410 2500 .053 0      - - out of memory 350    340    6500   7000 true 11   5.9 230 360
minepump_spec2_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 54 16   400 2500 .053 0      - - out of memory 330    320    4800   7000 true 11   5.9 210 350
minepump_spec2_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 56 17   450 2500 .053 .0082 - - out of memory 330    310    4000   7000 true 11   6.0 230 350
minepump_spec2_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   6000 3800 .23  0      - - out of memory 330    310    4300   7000 true 21   11   290 600
minepump_spec2_product38_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   6000 3800 .15  0      - - out of memory 310    300    4900   7000 true 23   12   430 580
minepump_spec2_product39_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 410 410   2900 1300 11     0      - - error (invalid witness file) .49 .33 12   40 error (invalid witness file) 6.3 3.3 130 310
minepump_spec2_product40_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 410 410   3500 1300 12     0      - - error (invalid witness file) .51 .33 6.5 40 error (invalid witness file) 6.2 3.3 130 290
minepump_spec2_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   4600 3900 .18  0      - - out of memory 290    280    5400   7000 true 26   14   500 590
minepump_spec2_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 660 310   5600 3900 .18  0      - - out of memory 320    310    4400   7000 true 26   14   560 670
minepump_spec2_product47_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3700 840 13     0      - - error (invalid witness file) .52 .34 7.7 40 error (invalid witness file) 6.0 3.2 120 300
minepump_spec2_product48_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   4300 840 12     .098  - - error (invalid witness file) .55 .36 12   39 error (invalid witness file) 5.8 3.1 100 300
minepump_spec2_product49_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3200 610 12     0      - - error (invalid witness file) .48 .32 9.2 40 error (invalid witness file) 6.0 3.1 120 300
minepump_spec2_product50_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 430 420   3900 1200 19     0      - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.1 3.2 110 300
minepump_spec2_product51_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3300 690 7.6   0      - - error (invalid witness file) .45 .31 6.9 39 error (invalid witness file) 6.0 3.2 100 300
minepump_spec2_product52_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3700 1300 8.7   0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.0 3.2 100 300
minepump_spec2_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   6900 4500 .15  0      - - out of memory 300    280    2400   7000 true 25   14   490 650
minepump_spec2_product54_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 270   5800 4600 .098 0      - - error (invalid witness file) .55 .35 7.9 42 error (invalid witness file) 6.0 3.2 120 300
minepump_spec2_product55_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 540 540   5000 1200 7.4   0      - - error (invalid witness file) .53 .35 7.8 42 error (invalid witness file) 6.0 3.2 120 300
minepump_spec2_product56_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 550 550   4500 1300 7.8   0      - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 5.9 3.1 86 300
minepump_spec2_product57_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   4000 830 9.3   0      - - error (invalid witness file) .54 .35 12   42 error (invalid witness file) 5.5 3.0 110 290
minepump_spec2_product58_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   3500 830 13     0      - - error (invalid witness file) .52 .34 6.3 41 error (invalid witness file) 5.9 3.1 120 300
minepump_spec2_product59_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   4000 910 9.1   0      - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.1 3.2 100 300
minepump_spec2_product60_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   3800 910 11     0      - - error (invalid witness file) .52 .32 13   41 error (invalid witness file) 6.3 3.3 130 310
minepump_spec2_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   5200 4700 .18  .19   - - out of memory 360    340    3700   7000 true 25   14   470 630
minepump_spec2_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   5200 4700 .18  0      - - out of memory 330    310    2800   7000 true 26   14   500 590
minepump_spec2_product63_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4600 850 7.4   0      - - error (invalid witness file) .59 .37 11   44 error (invalid witness file) 6.1 3.3 110 310
minepump_spec2_product64_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4900 850 7.8   0      - - error (invalid witness file) .47 .30 9.4 40 error (invalid witness file) 5.8 3.1 120 300
minepump_spec3_product33_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 300   4400 3400 .18  .70   - - out of memory 320    300    3800   7000 true 13   7.3 300 450
minepump_spec3_product34_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 300   4400 3400 .18  .082  - - out of memory 320    300    3000   7000 true 15   8.2 320 480
minepump_spec3_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect 660 310   4100 3900 .18  0      - - out of memory 270    260    2800   7000 true 22   12   460 590
minepump_spec3_product38_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   4200 4200 .18  .082  - - out of memory 270    260    2500   7000 true 18   10   370 560
minepump_spec3_product41_true-unreach-call_false-termination.cil.c true 2 wit inspect 660 300   4500 3800 .18  0      - - out of memory 320    300    4800   7000 true 16   8.6 300 520
minepump_spec3_product42_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   4300 3900 .18  0      - - out of memory 280    270    4500   7000 true 16   8.7 360 540
minepump_spec3_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   5200 4300 .18  .0041 - - out of memory 270    260    4500   7000 true 23   13   460 560
minepump_spec3_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 670 310   5200 4200 .18  8.8    - - out of memory 280    270    2800   7000 true 33   18   510 560
minepump_spec3_product49_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3500 1300 12     0      - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.0 3.2 130 300
minepump_spec3_product50_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3500 670 12     0      - - error (invalid witness file) .51 .32 5.0 41 error (invalid witness file) 6.9 3.6 140 310
minepump_spec3_product53_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 550 540   4300 1200 13     0      - - error (invalid witness file) .51 .32 7.5 43 error (invalid witness file) 6.6 3.4 130 310
minepump_spec3_product54_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 550 540   4800 1200 14     0      - - error (invalid witness file) .52 .33 14   39 error (invalid witness file) 5.9 3.1 120 300
minepump_spec3_product57_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   3800 870 14     0      - - error (invalid witness file) .51 .32 9.9 40 error (invalid witness file) 6.0 3.2 130 290
minepump_spec3_product58_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   3700 870 14     0      - - error (invalid witness file) .49 .31 7.8 39 error (invalid witness file) 5.8 3.1 120 300
minepump_spec3_product61_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 580   4900 840 9.7   0      - - error (invalid witness file) .50 .32 8.8 43 error (invalid witness file) 6.4 3.3 120 300
minepump_spec3_product62_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 580   5000 840 10     0      - - error (invalid witness file) .50 .32 6.0 40 error (invalid witness file) 5.9 3.1 110 300
minepump_spec4_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 4.9 120 590 .053 0      - - out of memory 290    270    3200   7000 true 11   6.1 210 370
minepump_spec4_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.1 130 600 .053 0      - - out of memory 310    290    5700   7000 true 11   5.9 180 350
minepump_spec4_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.2 140 560 .053 .11   - - out of memory 300    280    3600   7000 true 12   6.4 250 370
minepump_spec4_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.2 140 580 .053 0      - - out of memory 300    280    4500   7000 true 10   5.4 210 360
minepump_spec4_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 29 7.4 220 940 .053 0      - - out of memory 290    270    4700   7000 true 12   6.4 240 370
minepump_spec4_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 38 10   280 1800 .053 0      - - out of memory 290    270    2900   7000 true 11   5.7 170 350
minepump_spec4_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 34 9.3 270 1700 .053 0      - - out of memory 290    270    3500   7000 true 14   7.8 280 490
minepump_spec4_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 40 9.8 280 1800 .053 0      - - out of memory 300    290    3500   7000 true 10   5.3 200 350
minepump_spec4_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 18 4.9 130 610 .053 0      - - out of memory 380    360    8200   7000 true 11   5.8 220 360
minepump_spec4_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.2 140 610 .053 .0082 - - out of memory 340    320    4200   7000 true 11   5.7 190 350
minepump_spec4_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.1 130 570 .053 0      - - out of memory 310    300    3700   7000 true 13   6.9 250 390
minepump_spec4_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.4 150 590 .053 .0082 - - out of memory 300    280    4700   7000 true 10   5.5 210 370
minepump_spec4_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 29 7.5 210 1000 .053 0      - - out of memory 310    290    6600   7000 true 13   7.0 240 430
minepump_spec4_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 35 8.8 230 1400 .053 0      - - out of memory 290    280    4800   7000 true 10   5.4 170 360
minepump_spec4_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 40 10   290 1900 .053 0      - - out of memory 270    260    3200   7000 true 13   7.3 290 490
minepump_spec4_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 38 9.5 260 1700 .053 0      - - out of memory 270    250    2700   7000 true 11   5.8 220 360
minepump_spec4_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 30 7.6 210 1100 .053 0      - - out of memory 410    390    4800   7000 true 12   6.9 240 430
minepump_spec4_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 12   330 2200 .053 0      - - out of memory 420    410    4800   7000 true 14   7.8 280 470
minepump_spec4_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 42 11   300 1900 .053 0      - - out of memory 400    390    3500   7000 true 13   7.4 250 500
minepump_spec4_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 44 12   320 1900 .053 0      - - out of memory 390    370    4800   7000 true 10   5.5 190 360
minepump_spec4_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 39 9.9 290 1400 .053 0      - - out of memory 350    330    4400   7000 true 13   6.9 210 450
minepump_spec4_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 52 15   390 2600 .053 0      - - out of memory 420    400    4500   7000 true 14   7.6 290 480
minepump_spec4_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 55 16   380 2600 .053 0      - - out of memory 340    330    6300   7000 true 13   7.4 280 530
minepump_spec4_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 62 17   400 2600 .053 0      - - out of memory 330    320    5000   7000 true 9.9 5.4 190 360
minepump_spec4_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 34 8.5 240 1400 .053 .0082 - - out of memory 480    460    5700   7000 true 13   6.9 200 420
minepump_spec4_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 11   320 2200 .053 .11   - - out of memory 470    460    5900   7000 true 12   6.7 240 400
minepump_spec4_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 46 12   330 2200 .053 0      - - out of memory 420    400    6000   7000 true 13   7.1 260 490
minepump_spec4_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 44 12   320 2100 .053 0      - - out of memory 370    350    4400   7000 true 10   5.4 190 350
minepump_spec4_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 39 10   310 1600 .053 0      - - out of memory 380    360    6800   7000 true 13   7.1 250 450
minepump_spec4_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 59 17   420 2600 .053 0      - - out of memory 460    440    5800   7000 true 14   7.5 240 470
minepump_spec4_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 57 17   380 2600 .053 0      - - out of memory 360    340    5200   7000 true 14   7.6 300 530
minepump_spec4_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 53 15   360 2600 .053 0      - - out of memory 320    310    4100   7000 true 10   5.4 230 350
minepump_spec4_product49_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   6800 3600 .23  0      - - out of memory 350    340    3100   7000 true 26   15   460 680
minepump_spec4_product50_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   6800 3600 .23  0      - - out of memory 420    400    6900   7000 true 27   15   440 650
minepump_spec4_product51_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 430 420   3600 1300 9.6   .098  - - error (invalid witness file) .46 .31 6.5 39 error (invalid witness file) 6.4 3.4 130 300
minepump_spec4_product52_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 430 420   3500 680 7.4   0      - - error (invalid witness file) .49 .32 7.5 40 error (invalid witness file) 5.7 3.0 100 300
minepump_spec4_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   5600 4600 .15  .090  - - out of memory 330    320    4900   7000 true 24   13   500 540
minepump_spec4_product54_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   5300 4700 .15  0      - - out of memory 390    380    5500   7000 true 26   14   470 680
minepump_spec4_product55_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 530 520   4400 1200 7.2   0      - - error (invalid witness file) .61 .40 7.2 40 error (invalid witness file) 5.8 3.1 120 290
minepump_spec4_product56_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 530 520   5400 1300 8.7   0      - - error (invalid witness file) .49 .31 12   40 error (invalid witness file) 6.0 3.2 130 300
minepump_spec4_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   6600 4600 .15  0      - - out of memory 330    310    5300   7000 true 32   18   610 730
minepump_spec4_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 710 310   5900 4700 .15  0      - - out of memory 370    350    4800   7000 true 38   21   800 710
minepump_spec4_product59_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 450   4800 890 7.4   .098  - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.0 3.2 130 300
minepump_spec4_product60_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 460   3900 890 9.2   .098  - - error (invalid witness file) .53 .33 9.7 41 error (invalid witness file) 5.9 3.1 100 300
minepump_spec4_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   5500 4800 .15  .090  - - out of memory 320    300    3200   7000 true 24   13   410 640
minepump_spec4_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   5500 4800 .15  .082  - - out of memory 320    300    3100   7000 true 25   14   570 670
minepump_spec4_product63_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4600 850 6.3   0      - - error (invalid witness file) .48 .32 11   41 error (invalid witness file) 5.9 3.2 120 290
minepump_spec4_product64_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   5700 850 7.0   0      - - error (invalid witness file) .53 .35 10   41 error (invalid witness file) 7.0 3.7 110 320
minepump_spec5_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 19 5.1 130 590 .053 0      - - true 11    5.6  200   390 true 12   6.4 250 360
minepump_spec5_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.1 140 560 .053 0      - - true 10    5.4  150   370 true 11   6.2 210 360
minepump_spec5_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.6 150 740 .053 0      - - true 9.9  5.2  140   350 true 10   5.5 210 360
minepump_spec5_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.4 150 650 .053 0      - - true 11    5.6  140   390 true 11   5.8 220 350
minepump_spec5_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 30 7.4 200 1000 .053 0      - - true 12    6.3  130   390 true 11   6.0 220 370
minepump_spec5_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 39 10   260 1700 .053 0      - - true 11    6.0  220   390 true 13   6.9 190 360
minepump_spec5_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 41 10   310 1800 .053 0      - - true 11    5.8  150   400 true 12   6.3 260 370
minepump_spec5_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 40 10   290 1600 .053 0      - - true 11    5.9  160   400 true 10   5.6 230 350
minepump_spec5_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.4 140 660 .053 .11   - - true 9.6  5.1  200   350 true 11   6.2 230 370
minepump_spec5_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 20 5.2 130 600 .053 0      - - true 11    5.6  170   380 true 12   6.2 220 360
minepump_spec5_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 21 5.5 150 640 .053 0      - - true 11    5.8  150   390 true 11   5.7 210 360
minepump_spec5_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 22 5.6 160 670 .053 0      - - true 10    5.4  220   350 true 11   5.9 230 360
minepump_spec5_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 29 7.1 210 980 .053 .012  - - true 12    6.1  250   430 true 11   6.1 230 370
minepump_spec5_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 39 10   260 1700 .053 0      - - true 12    6.2  190   400 true 11   6.1 220 360
minepump_spec5_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 43 11   330 2000 .053 0      - - true 11    5.9  140   420 true 11   6.2 230 370
minepump_spec5_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 43 11   320 2100 .053 0      - - true 12    6.1  160   400 true 10   5.5 170 350
minepump_spec5_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 33 8.3 240 1200 .053 .11   - - true 12    6.1  210   410 true 11   6.0 240 370
minepump_spec5_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 13   320 2200 .053 0      - - true 12    6.3  200   410 true 11   6.0 240 350
minepump_spec5_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 46 12   350 2200 .053 .0082 - - true 12    6.0  190   410 true 13   6.7 190 380
minepump_spec5_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 12   340 2300 .053 0      - - true 12    6.3  240   400 true 11   5.7 200 350
minepump_spec5_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 12   310 1900 .053 0      - - true 12    6.1  94   440 true 12   6.5 270 370
minepump_spec5_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 53 15   430 2700 .053 0      - - true 11    5.7  140   420 true 11   6.0 210 370
minepump_spec5_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 59 18   440 2700 .053 0      - - true 12    6.3  79   490 true 12   6.6 240 360
minepump_spec5_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 57 18   430 2700 .053 0      - - true 12    6.3  170   440 true 11   5.9 240 360
minepump_spec5_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 33 8.2 220 1100 .053 0      - - true 11    5.9  160   400 true 12   6.2 220 360
minepump_spec5_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 49 13   330 2300 .053 0      - - true 11    5.9  210   390 true 12   6.2 240 370
minepump_spec5_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 51 13   340 2200 .053 .0082 - - true 11    5.8  140   400 true 11   6.2 240 360
minepump_spec5_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 47 13   340 2300 .053 0      - - true 14    7.4  210   420 true 10   5.6 180 350
minepump_spec5_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 45 12   340 2200 .053 .0082 - - true 12    6.2  140   440 true 11   6.1 210 370
minepump_spec5_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 56 15   470 2700 .053 0      - - true 13    6.6  140   440 true 11   6.0 230 370
minepump_spec5_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 57 18   430 2700 .053 0      - - true 13    6.5  98   450 true 12   6.3 240 370
minepump_spec5_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 56 18   420 2800 .053 0      - - true 12    6.5  180   450 true 11   5.8 190 360
minepump_spec5_product33_true-unreach-call_false-termination.cil.c true 2 wit inspect 690 310   6800 2900 .23  0      - - timeout 900    890    9200   5800 true 22   12   470 550
minepump_spec5_product34_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   6600 3100 .23  0      - - out of memory 810    790    9700   7000 true 22   12   380 540
minepump_spec5_product35_true-unreach-call_false-termination.cil.c true 2 wit inspect 700 310   6800 3000 .23  .082  - - timeout 900    890    7300   5800 true 21   12   430 520
minepump_spec5_product36_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 320 310   2600 790 12     0      - - error (invalid witness file) .53 .36 7.2 40 error (invalid witness file) 5.8 3.1 110 300
minepump_spec5_product37_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 420 410   3400 1200 21     0      - - error (invalid witness file) .49 .32 7.3 40 error (invalid witness file) 5.8 3.1 120 300
minepump_spec5_product38_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 410 400   3700 1200 20     0      - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 6.0 3.2 120 300
minepump_spec5_product39_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 410 410   3400 1300 12     0      - - error (invalid witness file) .49 .32 7.6 40 error (invalid witness file) 6.1 3.2 120 300
minepump_spec5_product40_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 420 410   3800 1300 15     0      - - error (invalid witness file) .47 .31 8.5 39 error (invalid witness file) 6.5 3.4 130 300
minepump_spec5_product41_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 340 330   2700 850 21     0      - - error (invalid witness file) .54 .34 9.7 39 error (invalid witness file) 6.1 3.2 110 300
minepump_spec5_product42_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 340 340   2600 860 20     0      - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.9 3.2 110 300
minepump_spec5_product43_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 340 330   2900 990 11     0      - - error (invalid witness file) .49 .35 10   40 error (invalid witness file) 6.1 3.2 110 300
minepump_spec5_product44_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 350 340   3100 990 18     0      - - error (invalid witness file) .52 .35 9.7 41 error (invalid witness file) 5.8 3.1 120 290
minepump_spec5_product45_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3800 790 14     0      - - error (invalid witness file) .55 .36 9.5 39 error (invalid witness file) 6.3 3.3 130 300
minepump_spec5_product46_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3000 790 14     0      - - error (invalid witness file) .47 .31 9.7 39 error (invalid witness file) 6.3 3.3 120 300
minepump_spec5_product47_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   4800 840 11     0      - - error (invalid witness file) .50 .32 7.1 40 error (invalid witness file) 6.1 3.3 130 300
minepump_spec5_product48_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 450 440   3900 850 13     0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.9 3.1 110 300
minepump_spec5_product49_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 620   7300 3600 8.4   0      - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 5.9 3.2 110 300
minepump_spec5_product50_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 620   8000 3600 9.0   .0082 - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 5.7 3.1 110 300
minepump_spec5_product51_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 620   8700 3700 4.2   0      - - error (invalid witness file) .51 .34 4.1 40 error (invalid witness file) 6.5 3.5 130 320
minepump_spec5_product52_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 440 430   3600 700 9.0   0      - - error (invalid witness file) .62 .38 9.7 43 error (invalid witness file) 6.0 3.2 120 310
minepump_spec5_product53_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 670   6000 4600 9.2   0      - - error (invalid witness file) .54 .34 10   41 error (invalid witness file) 6.8 3.6 140 320
minepump_spec5_product54_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 670   9400 4700 9.3   0      - - error (invalid witness file) .49 .33 8.6 39 error (invalid witness file) 6.1 3.2 120 300
minepump_spec5_product55_true-unreach-call_false-termination.cil.c timeout (true) 0 wit inspect 900 680   7100 4700 4.1   0      - - error (invalid witness file) .51 .32 7.2 41 error (invalid witness file) 6.1 3.2 130 300
minepump_spec5_product56_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 540 540   4800 1300 11     0      - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.1 3.3 120 300
minepump_spec5_product57_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 450   4400 830 14     0      - - error (invalid witness file) .52 .36 4.3 41 error (invalid witness file) 5.4 2.9 100 290
minepump_spec5_product58_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   4600 840 10     0      - - error (invalid witness file) .51 .31 9.5 39 error (invalid witness file) 7.1 3.7 130 320
minepump_spec5_product59_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   4000 910 9.8   0      - - error (invalid witness file) .60 .37 7.6 43 error (invalid witness file) 5.7 3.0 91 290
minepump_spec5_product60_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 460   3200 910 10     0      - - error (invalid witness file) .48 .32 7.9 40 error (invalid witness file) 5.6 3.0 110 300
minepump_spec5_product61_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 580   5500 820 10     0      - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.6 3.0 99 290
minepump_spec5_product62_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4600 810 10     0      - - error (invalid witness file) .48 .33 6.9 39 error (invalid witness file) 6.5 3.4 120 310
minepump_spec5_product63_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 580   4600 850 7.6   0      - - error (invalid witness file) .52 .33 10   43 error (invalid witness file) 6.5 3.4 130 330
minepump_spec5_product64_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 580 570   4000 850 8.4   0      - - error (invalid witness file) .54 .34 12   43 error (invalid witness file) 5.4 2.9 110 280
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 740 740   6500 1000 6.7   0      - - error (invalid witness file) .50 .32 9.6 41 error (invalid witness file) 5.7 3.0 110 290
../../sv-benchmarks/c/product-lines/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 597 634 170000 140000 1500000 1600000 2400    36   597 2200 1200 34000 94000   597 4600 2500 70000 130000   597 52000 49000 660000 990000   597 15000 9700 230000 540000  
    correct results 414 666 88000 62000 750000 1400000 150    34   162 2000 1100 32000 86000   104 3800 2100 57000 92000   126 52000 49000 660000 990000   193 15000 9500 220000 510000  
        correct true 252 504 44000 26000 360000 650000 23    31   0 0 0 0 0   63 0 0 0 0   126 52000 49000 660000 990000   193 15000 9500 220000 510000  
        correct false 162 162 45000 36000 390000 710000 130    2.9 162 2000 1100 32000 86000   41 3800 2100 57000 92000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -32 450 390 3100 1700 .13 0   0 97 71 1100 4500   0 97 57 1100 2200   0 0 0 0 0   0 0 0 0 0  
        incorrect true 1 -32 450 390 3100 1700 .13 0   0 97 71 1100 4500   0 97 57 1100 2200   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (597 tasks, max score: 929) 634
Run set sv-comp17.ReachSafety-ProductLines