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