Tool CPAchecker 1.6.1-svn 22870
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS Linux 4.4.0-34-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135148 MB
Run set bmc-bitprecise.BMC.ProductLines k-induction-bitprecise.k-Induction.ProductLines predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines impact-bitprecise.Impact.ProductLines
Options -heap 10000M -noout -bmc -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT -heap 10000M -noout -sv-comp16--k-induction -setprop limits.time.cpu.thread=10000s -heap 10000M -noout -predicateAnalysis-PredAbsRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -heap 10000M -noout -predicateAnalysis-ImpactRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
test/programs/benchmarks/product-lines/ status cputime (s) walltime (s) memUsage host k BMC formula creation (s) SMT check (s) Bounds check (s) status cputime (s) walltime (s) memUsage host k BMC formula creation (s) SMT check (s) Invariant generation (s) Bounds check (s) Induction formula creation (s) Induction check (s) status cputime (s) walltime (s) memUsage host Refinement (s) Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) Abstraction (s) Solving (s) Model enumeration (s) SMT without itp (s) Boolean abstraction (s) status cputime (s) walltime (s) memUsage host Attempted forced coverings Refinement (s) Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) Abstraction (s) Solving (s) Model enumeration (s) SMT without itp (s) Forced covering (s) Successful forced coverings Boolean abstraction (s)
elevator_spec14_product20_false-unreach-call.cil.c 19.6  11.1  727957504 1 1.53  .004 72.5  36.7  1351553024 1 2.36  .017 9.29  78.0  52.6  1859104768 22.2   7.96  19.1   5.80  7.25  7.08  5.94  .00  5.94  66.1  43.5  1862713344 0 17.9   .899 13.8   7.32  .150 .001 .00  .00  .00  .070
elevator_spec14_product24_false-unreach-call.cil.c 21.0  12.2  762789888 1 1.58  .005 90.3  45.6  1605537792 1 2.91  .004 14.5   87.1  63.3  2394165248 22.9   8.93  26.0   8.63  7.86  7.61  6.45  .00  6.45  79.7  56.6  2199109632 0 24.3   .934 17.8   9.46  .186 .002 .00  .00  .00  .082
elevator_spec14_product28_false-unreach-call.cil.c 19.6  11.1  726867968 1 1.46  .005 80.4  40.7  1359736832 1 2.42  .006 12.1   80.7  54.7  1907412992 21.6   7.74  21.3   6.71  6.97  6.84  5.73  .00  5.73  67.9  45.7  1872072704 0 20.2   .819 13.5   6.98  .155 .004 .00  .00  .00  .099
elevator_spec14_product32_false-unreach-call.cil.c 21.3  12.4  763023360 1 1.86  .032 86.8  43.8  1613574144 1 2.84  .011 .005 95.5  66.8  2354495488 24.8   8.86  27.0   9.14  7.99  7.79  6.44  .00  6.44  80.5  57.3  2356092928 0 25.5   .901 17.5   10.1   .169 .001 .00  .00  .00  .116
elevator_spec14_productSimulator_false-unreach-call.cil.c 214    190    2360836096 1 11.8   2.57  523    262    5285154816 1 17.7   2.40  200     1000    967    4689915904 1000    968    4577275904
elevator_spec1_product18_false-unreach-call.cil.c 18.7  10.1  571920384 3 1.86  .004 .014 96.9  48.9  1659928576 3 3.66  .005 13.2   .023 19.0  3.83  903    869    1437609984 3.93  833     860     13.5   831     831     13.7   813     827     828     87.7  60.7  1618284544 6 17.4   6.72  32.8   8.58  5.89  5.66  3.42  1.39  4.89  10.8   1 4.82 
elevator_spec1_product20_false-unreach-call.cil.c 17.8  9.64 581402624 3 1.80  .002 .008 105    52.8  1838899200 3 4.44  .014 .005 .033 20.1  5.59  794    756    2264457216 15.3   692     729     18.4   689     689     31.0   652     683     683     94.4  68.5  1782702080 6 17.6   9.93  41.1   10.3   8.93  8.68  5.23  2.47  7.88  13.0   0 7.72 
elevator_spec1_product22_false-unreach-call.cil.c 19.7  10.7  622419968 3 2.03  .018 .009 113    57.1  2000007168 3 3.28  .004 19.2   .028 21.3  5.61  903    868    1955151872 9.11  817     854     17.9   814     813     32.7   775     807     808     104    76.5  2036858880 4 20.7   9.19  42.7   12.2   8.13  7.84  4.98  1.84  7.06  12.1   1 6.84 
elevator_spec1_product24_false-unreach-call.cil.c 18.9  10.4  568958976 3 1.75  .004 .020 130    65.8  2269085696 3 3.31  .006 21.6   .042 25.6  7.90  903    869    1802854400 5.05  824     859     17.8   822     822     18.8   798     817     818     121    92.7  2087391232 4 22.7   9.57  57.2   11.8   8.46  8.22  4.74  2.41  7.37  25.9   1 7.18 
elevator_spec1_product26_false-unreach-call.cil.c 18.6  10.0  571379712 3 1.72  .003 .012 108    54.4  1692684288 3 3.17  .004 15.3   .028 19.4  3.74  903    869    1624776704 5.95  826     858     14.6   824     823     23.2   795     818     818     92.7  64.9  1685303296 6 18.3   8.06  36.3   9.43  6.94  6.74  4.11  1.76  5.95  11.6   1 5.88 
elevator_spec1_product28_false-unreach-call.cil.c 18.7  10.2  586661888 3 1.91  .003 .035 106    53.7  1785593856 3 3.88  .005 15.5   .033 19.6  4.41  904    868    1719083008 8.18  819     855     16.4   817     816     33.8   776     810     811     96.2  70.2  1891782656 6 17.6   11.1   41.8   10.2   9.70  9.35  5.04  3.21  8.49  12.2   0 8.27 
elevator_spec1_product30_false-unreach-call.cil.c 19.8  10.9  722743296 3 2.14  .004 .006 115    58.1  2209026048 3 2.81  .004 19.9   .009 19.4  7.39  903    870    1689251840 4.93  828     860     15.7   826     825     20.5   801     821     822     145    116    2030002176 6 22.7   9.24  81.2   11.1   7.74  7.53  4.34  2.18  6.62  52.4   1 6.53 
elevator_spec1_product32_false-unreach-call.cil.c 18.9  10.3  587161600 3 1.79  .004 .023 129    65.0  2269237248 3 3.32  .006 23.1   .056 23.6  10.8   903    871    1559007232 5.04  829     861     15.9   827     826     18.7   804     822     823     116    86.3  2078511104 4 22.7   11.9   50.4   11.8   10.1   9.85  5.56  3.24  8.99  17.4   1 8.81 
elevator_spec1_productSimulator_false-unreach-call.cil.c 47.8  27.6  1122344960 3 12.1   .346 .771 212    107    4389982208 3 8.56  .554 58.6   1.27  36.1  9.90  904    867    2549751808 9.12  792     852     28.8   787     786     24.3   756     780     781     1000    967    4215369728
elevator_spec2_product18_false-unreach-call.cil.c 18.9  10.4  584937472 3 1.78  .023 .019 91.4  46.1  1749454848 3 3.20  .004 .004 .118 17.6  3.94  157    128    1778364416 11.7   84.4   106     10.5   82.9   82.5   12.8   67.0   79.8   80.0   103    76.8  1755901952 6 19.7   13.1   46.2   10.2   12.1   11.9   4.84  5.91  11.2   14.8   0 10.8  
elevator_spec2_product20_false-unreach-call.cil.c 18.9  10.2  662130688 3 1.71  .012 .011 104    52.2  1808683008 3 3.80  .006 14.1   .024 19.5  5.11  375    339    2130632704 12.9   287     315     13.4   285     284     18.1   262     280     281     101    74.8  1813147648 6 19.0   14.1   45.0   10.4   13.3   13.1   4.55  7.35  12.2   12.3   0 11.9  
elevator_spec2_product22_false-unreach-call.cil.c 19.4  10.5  564174848 3 1.63  .004 .007 111    56.0  1911672832 3 3.13  .004 .006 .013 20.8  5.27  454    419    2441936896 17.8   352     388     15.8   350     349     29.8   314     344     344     164    128    2236174336 6 23.3   20.5   92.0   16.7   19.1   18.8   6.25  11.3   18.0   44.5   0 17.6  
elevator_spec2_product24_false-unreach-call.cil.c 19.9  10.8  617963520 3 2.12  .004 .024 121    61.0  1989627904 3 4.12  .006 22.4   .151 18.3  6.37  270    237    2468900864 17.5   177     207     14.5   175     175     22.5   148     170     170     200    167    2276114432 6 26.3   23.0   127     15.6   21.9   21.6   5.32  15.1   20.8   76.7   0 20.5  
elevator_spec2_product26_false-unreach-call.cil.c 19.1  10.2  517488640 3 1.82  .003 .009 102    51.2  1775403008 3 3.41  .016 13.7   .007 21.0  3.46  321    287    2112299008 16.0   235     260     11.6   233     232     23.3   204     227     228     102    74.7  1817018368 6 20.1   13.1   44.1   11.4   12.1   11.9   4.87  5.91  11.1   11.5   0 10.8  
elevator_spec2_product28_false-unreach-call.cil.c 20.0  10.8  558333952 3 2.18  .015 .018 104    52.5  1802739712 3 4.03  .012 15.4   .037 19.8  4.34  166    135    2006573056 15.2   86.0   109     11.1   84.3   83.9   14.8   65.8   80.5   80.7   112    85.8  1864863744 6 22.1   16.9   52.5   10.4   15.5   15.2   5.20  8.84  14.4   16.7   0 14.1  
elevator_spec2_product30_false-unreach-call.cil.c 18.2  9.98 596725760 3 1.52  .003 .006 112    56.6  2029924352 3 3.45  .005 .005 .023 22.1  6.75  238    206    2397917184 15.9   152     177     13.4   150     150     17.0   130     147     147     151    114    2345308160 6 26.0   20.7   75.2   16.7   19.2   18.8   7.43  10.0   17.9   25.5   0 17.5  
elevator_spec2_product32_false-unreach-call.cil.c 18.7  10.4  582004736 3 1.55  .004 .007 135    68.1  2224668672 3 2.71  .005 .004 .028 20.3  6.25  891    858    2543235072 16.3   791     828     18.0   789     788     22.0   761     783     784     139    106    2216226816 6 25.2   19.3   67.4   16.3   17.8   17.4   6.35  9.93  16.7   19.7   0 16.3  
elevator_spec2_productSimulator_false-unreach-call.cil.c 42.7  24.5  1226792960 3 10.8   .346 .734 199    100    4146581504 3 8.76  .537 .005 1.83  33.2  12.4   905    872    2794962944 11.4   786     854     34.6   781     780     27.3   747     775     775     1000    964    4726034432
elevator_spec3_product03_false-unreach-call.cil.c 18.9  10.3  578674688 1 1.75  .006 65.3  33.1  1204330496 1 5.00  .029 6.49  79.1  55.3  1550118912 25.1   12.5   19.9   3.71  12.0   11.9   9.95  .00  9.95  60.8  41.5  1434570752 0 22.9   .553 8.70  4.43  .081 .00  .00  .00  .00  .046
elevator_spec3_product11_false-unreach-call.cil.c 19.5  10.7  617324544 1 1.84  .005 66.9  33.8  1138761728 1 5.23  .048 6.39  80.1  56.0  1576194048 25.0   12.5   20.1   4.03  12.0   11.8   9.81  .00  9.81  58.2  39.4  1483419648 0 19.7   .512 9.77  4.91  .101 .001 .00  .00  .00  .041
elevator_spec3_product19_false-unreach-call.cil.c 19.5  10.6  602222592 1 1.64  .004 65.4  33.1  1204404224 1 4.49  .047 6.68  76.0  53.5  1514172416 23.4   12.2   19.5   3.17  11.6   11.5   9.56  .00  9.56  60.9  40.9  1453318144 0 22.6   .437 8.20  3.99  .088 .002 .00  .00  .00  .051
elevator_spec3_product20_false-unreach-call.cil.c 20.3  11.5  742240256 1 1.81  .006 87.7  44.3  1367019520 1 3.43  .021 12.2   101    73.4  1922146304 33.5   15.9   27.9   6.50  15.2   15.0   12.5   .00  12.5   78.5  56.8  1885433856 0 30.8   .761 14.0   7.19  .157 .001 .00  .00  .00  .107
elevator_spec3_product23_false-unreach-call.cil.c 19.2  10.8  681218048 1 1.60  .006 70.3  35.5  1966206976 1 3.93  .048 8.86  94.9  68.5  1851691008 32.3   14.8   24.4   4.85  14.1   14.0   11.7   .00  11.7   80.3  55.4  1776787456 0 32.4   .645 10.9   5.46  .142 .002 .00  .00  .00  .054
elevator_spec3_product24_false-unreach-call.cil.c 22.6  13.1  786300928 1 1.97  .007 90.1  45.5  1595469824 1 3.02  .008 13.2   114    86.6  2356920320 35.9   18.0   36.0   9.87  17.1   16.8   13.8   .00  13.8   93.9  69.4  2289106944 0 37.3   .951 17.0   9.50  .175 .00  .00  .00  .00  .085
elevator_spec3_product27_false-unreach-call.cil.c 19.6  10.8  604442624 1 1.72  .005 74.3  37.6  1299415040 1 3.28  .019 10.2   80.6  57.6  1607340032 26.1   13.3   20.8   4.12  12.9   12.8   10.7   .00  10.7   64.9  44.8  1536434176 0 23.1   .820 11.3   5.76  .077 .001 .00  .00  .00  .070
elevator_spec3_product28_false-unreach-call.cil.c 21.2  12.2  776503296 1 1.59  .006 88.6  44.8  1385459712 1 3.48  .015 .005 107    78.0  1983385600 36.0   15.8   28.9   6.11  15.1   14.9   12.3   .00  12.3   89.2  62.7  1883152384 0 35.7   .791 13.8   7.04  .147 .001 .00  .00  .00  .058
elevator_spec3_product31_false-unreach-call.cil.c 19.1  10.8  695152640 1 1.57  .007 92.2  46.7  1491357696 1 3.15  .022 14.2   99.8  72.0  1866571776 34.5   15.3   26.0   5.52  14.6   14.4   12.1   .00  12.1   80.2  56.3  1805094912 0 34.0   .646 10.6   5.22  .169 .002 .00  .00  .00  .065
elevator_spec3_product32_false-unreach-call.cil.c 21.5  12.6  780713984 1 1.50  .007 98.9  49.9  1598164992 1 3.56  .032 16.4   124    94.1  2406051840 41.1   18.6   36.7   10.0   17.8   17.6   14.6   .00  14.6   102    75.3  2294702080 0 40.3   1.15  19.2   10.0   .212 .001 .00  .00  .00  .109
elevator_spec3_productSimulator_false-unreach-call.cil.c 1000    970    2446704640 1000    501    6017011712 1000    961    5281808384 1000    968    5093507072
elevator_spec9_product26_false-unreach-call.cil.c 19.4  10.4  599359488 3 1.89  .015 .017 100    50.5  1824288768 3 3.19  .005 14.3   .020 16.9  4.30  202    167    1970135040 12.7   117     143     11.9   115     115     15.7   95.7   111     112     106    78.1  1798053888 6 19.3   15.7   48.0   10.6   14.1   13.9   5.21  7.63  13.1   13.5   0 12.9  
elevator_spec9_product28_false-unreach-call.cil.c 19.4  10.6  541548544 3 1.97  .004 .007 108    54.5  1867890688 3 4.02  .004 17.6   .030 16.9  4.34  903    871    1715810304 5.74  834     861     12.3   832     831     20.9   806     827     828     109    81.5  1872302080 6 22.6   13.5   47.8   11.2   12.5   12.2   4.88  6.20  11.5   15.0   0 11.1  
elevator_spec9_product30_false-unreach-call.cil.c 19.0  10.5  646529024 3 1.62  .005 .023 115    57.7  1903616000 3 3.44  .005 20.2   .043 19.8  5.43  461    428    2377273344 16.6   365     398     15.6   363     362     22.4   336     358     359     203    170    2345484288 6 24.6   15.8   132     16.7   14.6   14.3   5.92  6.98  13.2   87.6   0 12.9  
elevator_spec9_product32_false-unreach-call.cil.c 20.3  11.1  626827264 3 2.12  .003 .028 120    60.6  2287783936 3 3.14  .006 .004 .034 18.0  6.53  904    871    1742155776 3.63  828     862     17.4   826     826     18.0   804     822     822     157    126    2402107392 6 25.9   20.6   87.1   15.1   19.2   18.9   7.58  10.2   18.2   39.6   0 17.8  
elevator_spec9_productSimulator_false-unreach-call.cil.c 43.9  25.4  1171914752 3 10.8   .465 .773 218    110    3793092608 3 9.37  .575 60.6   1.28  41.6  8.81  904    871    2564108288 11.3   801     854     25.6   796     795     20.3   771     791     791     1000    965    4426334208
elevator_spec13_product21_true-unreach-call.cil.c 903    881    2213449728 6524 82.5   .864 368     902    452    5637623808 1 4.58  .00  369     .048 903    876    2263826432 165     691     705     7.32  690     690     40.8   623     664     678     903    875    1996800000 219 821     2.44  39.0   18.5   .581 .036 .00  .00  1.55  3.48  150
elevator_spec13_product22_true-unreach-call.cil.c 903    882    3685228544 6616 86.1   .951 349     902    452    5539610624 1 3.30  .001 364     .022 903    869    3727761408 447     367     415     26.6   364     363     105     228     333     334     903    874    2553913344 115 794     3.71  58.3   30.3   .785 .041 .00  .00  .810 1.91  100
elevator_spec13_product23_true-unreach-call.cil.c 903    879    2052317184 8054 83.5   .973 355     902    452    5578674176 1 4.20  .009 368     .049 270    248    2065207296 168     61.9   75.2   6.32  60.9   60.7   46.5   4.33  50.9   47.9   904    876    2035798016 163 819     2.54  40.8   20.4   .604 .044 .00  .00  1.25  2.46  119
elevator_spec13_product24_true-unreach-call.cil.c 903    880    2467176448 7923 79.8   1.02  377     902    452    5798019072 1 2.64  .00  .004 .030 903    868    3073339392 244     573     618     22.4   570     570     101     446     547     544     903    874    2500902912 165 794     3.26  60.6   30.2   .769 .036 .00  .00  1.25  3.11  102
elevator_spec13_product29_true-unreach-call.cil.c 903    880    2390376448 6703 86.5   .959 337     902    452    5669298176 1 4.88  .001 368     .058 902    874    1938399232 163     694     705     5.70  693     693     39.6   644     683     682     903    876    2248630272 179 803     2.08  62.4   17.2   .453 .050 .00  .00  1.35  30.7   148
elevator_spec13_product30_true-unreach-call.cil.c 903    879    2586058752 6552 85.3   .850 351     903    452    5617618944 1 2.62  .00  368     .021 903    870    2915819520 261     562     602     20.2   560     559     82.6   456     539     536     902    877    1704562688 2285 107     1.02  764     10.8   .205 .027 .00  .00  58.7   719     101
elevator_spec13_product31_true-unreach-call.cil.c 903    880    1981317120 7993 81.5   .946 375     902    452    5775073280 1 4.20  .00  .008 .044 903    874    2335088640 181     669     687     9.18  668     668     53.4   603     656     655     903    873    1894981632 2134 444     1.51  420     13.1   .409 .050 .00  .00  35.3   379     141
elevator_spec13_product32_true-unreach-call.cil.c 903    880    2197090304 7970 80.5   .929 364     902    452    5680766976 1 3.14  .00  369     .026 903    873    2621403136 192     650     676     13.1   648     647     61.0   573     634     630     903    874    2681786368 103 795     3.91  60.0   31.2   .775 .028 .00  .00  .627 1.59  92
elevator_spec13_productSimulator_true-unreach-call.cil.c 1000    889    7717310464 903    452    6277881856 1 18.8   1.45  .005 2.77  904    863    4525625344 502     262     351     45.8   257     256     144     73.3   217     208     904    868    3129987072 1693 522     3.85  321     33.1   .845 .019 .00  .00  27.6   247     152
elevator_spec14_product03_true-unreach-call.cil.c 19.2  10.4  559599616 9 2.98  .001 .103 81.2  41.1  1492500480 1 5.08  .00  9.72  .051 7.20 7.81  83.8  64.9  1427890176 11.8   35.7   48.2   6.30  34.9   34.7   20.1   11.1   31.2   19.4   50.5  33.8  1345335296 3 16.1   .641 13.3   5.31  .132 .002 .00  .00  .022 3.21  1
elevator_spec14_product11_true-unreach-call.cil.c 20.5  11.0  547164160 9 3.19  .001 .102 77.2  39.0  1482330112 1 4.00  .00  9.67  .037 8.67 4.63  75.0  55.5  1391976448 12.8   26.7   37.6   5.21  26.1   25.9   16.5   6.42  22.9   12.7   53.8  37.7  1363283968 3 19.7   .565 13.2   4.68  .099 .001 .00  .00  .034 3.43  1
elevator_spec14_product19_true-unreach-call.cil.c 20.6  11.0  592723968 9 3.40  .003 .105 76.3  38.5  1474605056 1 4.68  .00  9.03  .026 9.87 5.32  63.3  47.2  1398169600 11.6   20.8   31.0   5.36  20.2   20.0   15.0   2.12  17.1   8.38  52.0  36.4  1367416832 3 17.9   .762 13.9   5.86  .087 .00  .00  .00  .020 3.58  1
elevator_spec14_product23_true-unreach-call.cil.c 21.9  12.0  684265472 12 3.78  .00  .143 107    53.8  1993842688 2 3.46  .00  18.1   .183 12.9  9.01  91.8  69.9  1510506496 17.6   33.2   47.4   7.03  32.3   32.0   20.4   8.36  28.8   16.8   102    81.9  1740804096 6 33.4   .953 43.7   7.15  .160 .002 .00  .00  .052 29.7   1
elevator_spec14_product27_true-unreach-call.cil.c 21.6  11.8  598888448 9 3.50  .002 .100 82.5  41.8  1533108224 1 3.88  .001 12.2   .037 7.14 4.93  73.0  54.1  1470992384 14.1   23.6   35.1   5.65  23.0   22.8   17.3   2.63  19.9   9.90  56.4  39.5  1413304320 3 18.8   .695 16.0   5.79  .117 .002 .00  .00  .021 4.14  1
elevator_spec14_product31_true-unreach-call.cil.c 23.4  12.8  715075584 12 3.88  .002 .192 129    64.8  2473746432 2 4.45  .001 24.5   .043 14.2  8.73  285    259    1830711296 20.0   214     233     10.6   213     212     29.8   178     207     190     83.7  63.6  1555394560 3 24.0   .711 34.8   6.62  .103 .001 .00  .00  .023 21.4   1
elevator_spec1_product01_true-unreach-call.cil.c 18.0  9.54 479035392 9 2.67  .001 .078 207    104    4641976320 9 4.94  .002 62.3   .101 22.1  61.6   541    512    1748566016 11.3   463     495     16.2   461     460     40.3   412     453     453     91.8  70.4  1259081728 14 19.3   8.08  46.6   5.08  7.66  7.50  4.28  2.34  6.92  28.8   2 6.64 
elevator_spec1_product03_true-unreach-call.cil.c 20.2  10.6  494444544 9 3.64  .001 .082 283    142    4728242176 9 5.23  .00  97.7   .117 20.7  101     903    874    1583476736 17.0   834     852     7.31  832     832     32.2   793     825     826     97.0  75.1  1313669120 13 22.4   9.34  48.1   6.25  8.93  8.83  5.35  2.37  8.05  27.1   1 7.74 
elevator_spec1_product09_true-unreach-call.cil.c 19.0  9.99 521965568 9 3.00  .002 .112 227    114    4608782336 9 4.89  .002 70.8   .092 21.2  70.8   902    873    1425219584 11.5   842     857     5.98  840     840     24.4   811     835     836     104    81.2  1321299968 14 24.7   9.47  51.8   5.74  8.76  8.62  4.83  2.71  7.96  31.5   1 7.56 
elevator_spec1_product11_true-unreach-call.cil.c 18.7  9.93 509526016 9 2.96  .00  .062 267    134    4704636928 9 5.29  .020 .005 .131 21.8  89.7   903    871    1994153984 15.5   817     851     16.0   815     814     48.6   757     805     806     97.4  75.7  1342328832 13 21.5   9.42  49.7   6.08  8.24  8.10  5.16  1.74  7.33  29.0   1 6.95 
elevator_spec1_product17_true-unreach-call.cil.c 19.3  10.2  506802176 9 3.10  .00  .096 220    111    4434677760 9 5.08  .00  64.6   .119 22.4  66.2   904    871    1803423744 17.2   820     849     12.4   818     817     51.2   757     808     809     74.2  52.8  1226637312 9 15.3   7.71  33.0   5.84  7.18  7.08  4.10  1.94  6.21  14.1   1 6.05 
elevator_spec1_product19_true-unreach-call.cil.c 19.4  10.3  495075328 9 3.24  .001 .085 308    155    4814708736 9 5.14  .00  111     .116 20.7  111     364    337    1393152000 8.90  303     322     9.55  301     301     22.0   275     297     297     152    129    1385844736 20 32.7   10.5   91.6   6.60  9.76  9.56  5.18  3.24  9.42  68.7   2 8.45 
elevator_spec1_product21_true-unreach-call.cil.c 18.6  9.92 524328960 9 2.83  .00  .065 540    271    5255311360 9 4.42  .012 222     .103 25.4  222     903    871    1555607552 6.73  834     859     11.9   831     831     26.8   799     826     827     903    877    1868283904 21 44.5   12.8   827     8.64  12.0   11.8   7.63  2.92  12.0   798     1 10.6  
elevator_spec1_product23_true-unreach-call.cil.c 22.5  11.8  604364800 9 4.13  .001 .116 655    328    5547192320 9 4.57  .001 269     .141 28.6  274     903    872    1337769984 7.19  837     860     11.0   836     835     23.8   807     831     831     903    878    2147254272 34 127     18.1   746     10.4   16.7   16.4   9.82  4.94  18.5   709     1 14.8  
elevator_spec1_product25_true-unreach-call.cil.c 19.2  10.1  545824768 9 2.94  .00  .085 269    135    4712402944 9 4.99  .002 89.2   .121 21.6  93.0   902    876    1184313344 9.23  851     862     4.76  850     850     14.7   832     846     847     77.3  55.3  1234993152 9 16.6   7.56  34.1   6.22  6.99  6.87  4.39  1.53  6.11  15.3   1 5.95 
elevator_spec1_product27_true-unreach-call.cil.c 20.7  10.8  506474496 9 3.30  .00  .090 350    176    4964069376 9 5.01  .001 127     .127 20.4  134     902    871    1682411520 15.4   830     851     9.65  828     828     36.1   785     821     822     130    107    1400811520 18 23.6   10.6   78.2   7.26  9.92  9.71  6.02  2.52  8.94  54.5   2 8.55 
elevator_spec1_product29_true-unreach-call.cil.c 18.6  9.96 520687616 9 2.96  .003 .066 624    313    5390364672 9 4.41  .001 261     .101 25.3  262     903    872    1487298560 6.13  836     861     12.0   834     833     30.9   797     828     828     903    878    2124349440 21 47.6   14.1   826     9.28  13.3   13.1   7.20  4.46  12.6   795     1 11.7  
elevator_spec1_product31_true-unreach-call.cil.c 20.2  10.7  595464192 9 3.54  .002 .097 748    375    5889708032 9 4.68  .001 308     .111 26.3  323     903    870    1778200576 10.1   827     855     13.0   824     824     43.1   774     817     818     903    877    2343096320 27 80.1   18.6   792     9.55  17.7   17.5   11.3   4.60  19.8   757     1 15.9  
elevator_spec2_product01_true-unreach-call.cil.c 17.2  9.10 520388608 5 2.65  .001 .033 96.2  48.5  1789358080 5 3.40  .00  16.9   .051 16.1  12.2   125    95.6  1390755840 16.3   60.1   74.6   6.40  58.9   58.6   20.8   33.9   54.6   54.9   166    146    1455140864 16 63.8   12.1   76.9   5.53  11.5   11.3   6.09  4.05  14.3   54.0   1 10.2  
elevator_spec2_product03_true-unreach-call.cil.c 17.8  9.45 505335808 5 2.55  .00  .019 112    56.8  2060115968 5 4.86  .002 19.8   .071 17.7  19.9   129    103    1483513856 13.6   68.8   85.2   6.84  67.2   66.9   21.3   41.3   62.5   62.8   129    107    1348419584 11 45.3   13.6   56.8   5.64  13.0   12.9   5.42  6.24  13.8   31.9   1 11.7  
elevator_spec2_product09_true-unreach-call.cil.c 16.7  8.92 475648000 5 2.11  .00  .025 105    52.8  1961807872 5 4.12  .001 .004 .038 15.3  19.0   161    134    1559736320 25.3   87.6   103     6.27  86.0   85.6   33.9   45.5   79.4   79.7   117    96.0  1341280256 11 41.1   11.8   50.3   6.22  11.2   11.0   5.32  4.48  11.2   27.1   1 9.82 
elevator_spec2_product11_true-unreach-call.cil.c 17.3  9.11 547913728 5 2.24  .00  .021 114    57.3  2312527872 5 4.56  .00  21.2   .059 18.7  19.8   902    872    1731936256 22.3   828     845     7.00  827     826     34.3   783     817     821     132    110    1367408640 11 44.5   15.5   60.8   6.86  14.8   14.6   5.69  7.70  15.6   33.0   1 13.4  
elevator_spec2_product17_true-unreach-call.cil.c 16.9  8.96 521674752 5 2.13  .00  .013 102    51.3  1984905216 5 4.42  .002 17.9   .056 15.5  14.4   161    134    1613725696 24.8   89.9   105     5.88  88.7   87.9   28.5   53.8   82.3   82.6   123    101    1356148736 11 41.4   12.1   55.5   6.66  11.5   11.4   5.17  5.12  11.9   30.7   1 10.3  
elevator_spec2_product19_true-unreach-call.cil.c 18.1  9.54 491995136 5 2.49  .006 .037 112    56.7  2776367104 5 4.64  .00  .015 .051 13.1  17.9   115    89.4  1427304448 17.9   52.8   66.7   5.58  51.8   51.5   22.7   24.3   46.9   47.1   188    167    1599361024 16 71.1   14.2   90.8   6.74  13.6   13.5   6.54  5.62  15.9   63.9   1 12.2  
elevator_spec2_product21_true-unreach-call.cil.c 19.0  10.1  459448320 5 2.53  .001 .027 137    68.9  2540482560 5 3.51  .001 .004 .039 17.4  28.6   903    871    1857015808 23.3   814     843     11.3   812     812     40.6   762     803     805     903    878    2276995072 8 20.7   13.0   853     8.42  12.2   12.0   6.06  4.94  11.5   824     0 11.0  
elevator_spec2_product23_true-unreach-call.cil.c 18.5  9.91 526700544 5 2.63  .001 .026 146    73.5  2770616320 5 4.25  .002 34.9   .071 19.7  29.5   774    740    1894404096 20.9   684     714     13.5   682     681     44.9   628     673     674     288    264    1620615168 11 64.8   19.0   195     9.38  18.2   18.0   8.62  8.05  20.1   160     1 16.7  
elevator_spec2_product25_true-unreach-call.cil.c 16.6  8.87 489111552 5 2.03  .00  .036 111    56.1  1908940800 5 4.60  .00  .004 .053 18.9  18.3   151    124    1509502976 16.4   87.7   103     6.12  86.3   86.0   22.3   59.1   81.4   81.7   129    107    1372016640 11 43.3   14.4   59.0   7.27  13.9   13.7   5.63  6.89  14.6   31.8   1 12.6  
elevator_spec2_product27_true-unreach-call.cil.c 18.2  9.55 544681984 5 2.37  .00  .044 118    59.4  2206023680 5 4.79  .001 23.4   .060 18.2  19.6   135    105    1593712640 19.7   64.4   80.2   7.01  63.1   62.8   25.1   32.9   58.1   58.3   145    122    1441841152 11 51.2   14.7   65.6   6.95  14.1   13.9   6.31  6.08  14.2   38.2   1 12.4  
elevator_spec2_product29_true-unreach-call.cil.c 17.0  9.11 511938560 5 2.09  .00  .021 172    86.5  3350327296 5 4.32  .002 48.5   .048 17.6  43.0   903    874    1638486016 8.29  833     860     13.3   831     830     37.2   786     824     825     903    878    1860743168 17 68.1   21.5   805     10.0   20.6   20.3   8.36  10.6   22.9   765     0 19.0  
elevator_spec2_product31_true-unreach-call.cil.c 18.0  9.48 526667776 5 2.46  .001 .055 185    93.2  3612209152 5 4.34  .001 .007 .052 19.2  49.1   903    875    1503956992 5.26  841     864     10.7   840     839     24.8   810     835     835     437    412    1797488640 16 105     25.8   302     9.71  24.8   24.5   10.3   12.6   31.0   258     1 23.0  
elevator_spec3_product01_true-unreach-call.cil.c 21.3  11.5  605335552 12 3.64  .00  .162 87.6  44.5  1481785344 1 4.91  .001 10.6   .046 8.09 7.79  145    128    1438277632 16.7   94.4   107     6.70  93.6   93.4   28.1   60.4   88.5   68.4   832    808    2413051904 40 449     .755 354     7.96  .192 .003 .00  .00  26.5   336     1
elevator_spec3_product09_true-unreach-call.cil.c 22.0  11.8  605933568 12 3.88  .001 .199 89.6  45.3  1519538176 1 5.35  .008 10.9   .051 9.01 7.32  82.1  62.7  1383698432 19.2   29.3   38.7   4.89  28.6   28.5   19.0   6.00  25.0   11.0   903    881    2678587392 41 492     .979 384     6.97  .185 .001 .00  .00  25.4   368     0
elevator_spec3_product17_true-unreach-call.cil.c 20.5  11.1  589606912 12 3.43  .001 .126 87.3  44.3  1469468672 1 4.75  .00  11.4   .017 7.26 6.66  147    127    1424769024 18.7   88.7   104     7.84  87.8   87.6   33.7   47.8   81.6   57.4   904    881    2540867584 45 458     .884 418     8.20  .199 .002 .00  .00  23.8   400     0
elevator_spec3_product18_true-unreach-call.cil.c 22.6  12.6  719413248 12 3.84  .001 .165 97.9  49.4  1732304896 1 3.27  .00  14.9   .042 12.4  3.55  132    107    1695625216 28.6   55.5   72.9   8.81  54.3   54.1   25.1   24.0   49.1   31.1   903    877    3056513024 32 567     1.49  305     12.3   .265 .003 .00  .00  16.3   280     0
elevator_spec3_product21_true-unreach-call.cil.c 23.8  13.3  744194048 12 4.19  .00  .127 94.2  47.5  1561001984 1 4.12  .00  .005 .024 11.3  2.96  125    99.9  1608118272 28.1   51.8   66.9   8.26  50.6   50.4   28.1   17.8   45.9   26.4   904    880    2379870208 15 320     1.12  555     9.02  .166 .012 .00  .00  3.92  538     0
elevator_spec3_product22_true-unreach-call.cil.c 23.9  13.7  753270784 12 3.81  .001 .174 130    65.8  2323156992 1 3.04  .00  26.7   .030 14.5  2.72  229    204    2128195584 33.6   136     164     15.5   135     134     40.9   86.9   128     102     904    877    2885001216 17 542     1.69  330     15.5   .301 .003 .00  .00  6.79  300     0
elevator_spec3_product25_true-unreach-call.cil.c 21.9  11.9  595304448 12 3.61  .004 .196 82.0  41.4  1488314368 1 4.55  .001 9.78  .037 8.42 6.40  133    112    1443622912 20.1   72.9   86.5   6.89  72.2   71.9   25.8   41.2   67.0   48.6   903    881    2976907264 39 523     1.07  352     8.70  .196 .003 .00  .00  29.0   333     0
elevator_spec3_product26_true-unreach-call.cil.c 22.3  12.6  754266112 12 3.41  .00  .125 96.7  48.8  1833664512 1 3.42  .001 15.0   .008 11.8  3.24  212    184    1867034624 27.3   129     152     11.6   128     127     36.0   84.9   121     96.3   904    878    3054411776 28 628     1.62  245     12.6   .285 .005 .00  .00  9.57  220     0
elevator_spec3_product29_true-unreach-call.cil.c 23.1  12.6  723816448 12 3.79  .00  .166 102    51.6  1738919936 1 3.65  .00  16.8   .036 10.4  2.28  182    159    1733185536 30.4   107     123     7.97  106     106     31.5   69.5   101     78.5   904    879    2448330752 15 356     .894 518     8.20  .159 .003 .00  .00  4.01  502     0
elevator_spec3_product30_true-unreach-call.cil.c 25.6  14.5  782188544 12 3.94  .00  .206 111    56.2  3356172288 1 3.69  .001 19.1   .030 14.2  2.66  287    262    2101661696 34.2   194     222     15.8   193     192     41.5   144     186     158     903    876    2707369984 12 448     1.57  422     14.3   .353 .004 .00  .00  4.76  395     0
elevator_spec9_product09_true-unreach-call.cil.c 17.3  9.18 483938304 5 2.27  .00  .038 104    52.7  1908318208 5 4.05  .00  17.2   .256 18.0  15.6   903    874    1195073536 6.61  848     862     7.09  847     847     14.7   828     843     844     125    103    1346899968 11 40.9   12.7   57.4   6.87  12.1   11.9   5.46  5.28  12.4   32.2   1 10.8  
elevator_spec9_product11_true-unreach-call.cil.c 17.9  9.56 497926144 5 2.45  .002 .021 118    59.3  2037243904 5 4.66  .00  19.9   .071 18.5  19.2   172    144    1599254528 24.3   95.9   115     6.98  94.2   93.6   29.5   58.3   87.8   88.3   191    169    1553440768 16 75.7   17.2   88.7   6.94  16.5   16.4   6.34  8.69  19.0   58.9   1 15.1  
elevator_spec9_product25_true-unreach-call.cil.c 17.8  9.43 491139072 5 2.30  .00  .031 107    54.1  2044547072 5 4.45  .001 .004 .072 18.9  15.2   131    105    1510785024 15.6   70.7   84.4   7.12  69.6   69.3   22.6   42.4   65.0   65.2   122    102    1331822592 11 41.9   13.6   54.7   6.31  13.0   12.9   5.24  6.52  13.9   28.9   1 11.8  
elevator_spec9_product27_true-unreach-call.cil.c 17.4  9.30 426369024 5 2.23  .00  .026 117    59.1  2160078848 5 4.45  .00  .004 .026 17.6  21.3   903    876    1176281088 6.82  850     864     6.72  849     849     11.5   834     845     846     133    111    1442009088 11 46.5   13.8   60.1   6.80  13.2   13.0   5.71  6.13  13.6   33.6   1 11.9  
elevator_spec9_product29_true-unreach-call.cil.c 18.3  9.81 540532736 5 2.41  .001 .019 165    82.8  3231870976 5 4.39  .00  .005 .066 17.8  40.1   250    222    1909317632 17.4   175     200     11.6   173     172     33.9   133     166     167     692    668    1832038400 11 58.4   18.9   605     8.84  18.0   17.8   7.86  8.76  20.6   570     1 16.6  
elevator_spec9_product31_true-unreach-call.cil.c 19.0  10.1  517754880 5 2.69  .00  .032 159    80.1  3115343872 5 4.55  .001 .004 .050 20.9  34.6   903    872    1509376000 11.7   833     856     10.3   831     830     32.7   790     823     825     768    743    2022514688 16 108     24.6   630     9.55  23.6   23.4   9.88  12.1   29.0   587     1 22.0  
email_spec0_product16_false-unreach-call.cil.c 1000    983    3192164352 1000    501    7066873856 1000    984    2813186048 1000    982    2605023232
email_spec0_product21_false-unreach-call.cil.c 1000    981    3488739328 1000    501    6824329216 902    881    1118916608 2.06  866     874     3.66  865     865     18.0   832     850     848     1000    981    2731970560
email_spec0_product22_false-unreach-call.cil.c 1000    982    3163889664 1000    501    6374416384 1000    981    2326888448 1000    984    2507853824
email_spec0_product26_false-unreach-call.cil.c 1000    981    3516071936 1000    501    7497871360 902    880    1129320448 2.63  864     872     3.79  863     863     23.1   827     850     840     1000    981    2894073856
email_spec0_product31_false-unreach-call.cil.c 1000    982    3559690240 1000    501    6159773696 1000    982    3001856000 1000    981    2629427200
email_spec0_product33_false-unreach-call.cil.c 1000    982    3526479872 1000    501    7273533440 1000    981    2438598656 1000    982    2653659136
email_spec0_product34_false-unreach-call.cil.c 1000    983    3924529152 1000    501    7245660160 902    880    1269035008 1.92  865     873     3.75  865     865     17.7   832     850     847     1000    980    2898198528
email_spec0_product35_false-unreach-call.cil.c 1000    980    3671023616 1000    501    7610630144 1000    979    2728927232 1000    980    2963910656
email_spec0_productSimulator_false-unreach-call.cil.c 1000    971    4982878208 1000    501    7968370688 902    873    3512569856 2.78  810     865     25.7   807     806     193     542     735     554     1000    964    5297926144
email_spec11_product15_false-unreach-call.cil.c 1000    985    3118604288 1000    501    6339543040 1000    981    2535182336 1000    982    2565541888
email_spec11_product20_false-unreach-call.cil.c 1000    982    3604512768 1000    501    5978796032 902    883    1219780608 2.03  869     876     3.09  869     869     16.9   826     842     854     1000    981    2678542336
email_spec11_product22_false-unreach-call.cil.c 1000    986    3269042176 1000    501    5854683136 1000    980    2788524032 1000    983    2518106112
email_spec11_product26_false-unreach-call.cil.c 1000    981    4022915072 1000    501    7477604352 1000    979    2599546880 1000    982    2974978048
email_spec11_product30_false-unreach-call.cil.c 1000    981    3143659520 1000    501    6282342400 1000    982    2690072576 1000    983    2514948096
email_spec11_product32_false-unreach-call.cil.c 1000    980    3644846080 1000    501    7353704448 902    881    1027735552 1.33  868     875     3.25  868     867     9.11  849     858     860     1000    979    2947510272
email_spec11_product33_false-unreach-call.cil.c 1000    984    3217960960 1000    501    7316959232 1000    980    2631331840 1000    983    2627325952
email_spec11_product35_false-unreach-call.cil.c 1000    980    3600535552 1000    501    7772401664 1000    978    2658217984 1000    980    2799734784
email_spec11_productSimulator_false-unreach-call.cil.c 1000    971    4929380352 1000    501    8175828992 904    873    2919591936 2.60  817     864     20.0   814     812     515     181     697     185     905    867    4661166080 6 721     4.35  68.3   32.6   .947 .035 .00  .00  32.0   3.43  0
email_spec1_product14_false-unreach-call.cil.c 159    148    2750676992 3 4.28  .564 .413 1000    734    6509584384 902    886    794234880 .393 876     881     2.50  876     876     2.02  868     870     875     185    168    2943733760 6 9.95  .367 7.33  3.04  .083 .002 .00  .00  .769 1.52  1
email_spec1_product15_false-unreach-call.cil.c 145    134    2617896960 3 3.77  .692 .215 1000    718    6148550656 1000    984    2749620224 169    154    2724945920 6 5.46  .324 5.47  2.18  .059 .001 .00  .00  .103 1.16  1
email_spec1_product16_false-unreach-call.cil.c 127    117    2618933248 3 3.90  .735 .229 1000    712    6212640768 1000    984    2729197568 160    146    2698522624 6 5.82  .248 5.40  1.82  .037 .00  .00  .00  .084 1.00  1
email_spec1_product20_false-unreach-call.cil.c 713    690    3074162688 3 5.49  2.21  .283 1000    501    6362173440 902    886    819040256 .682 876     881     2.36  876     875     2.73  867     870     874     1000    978    3146711040
email_spec1_product21_false-unreach-call.cil.c 762    738    3128766464 3 6.64  3.01  .357 1000    501    6611165184 902    881    967720960 1.17  869     875     3.21  868     868     8.19  850     858     861     1000    976    3187695616
email_spec1_product22_false-unreach-call.cil.c 169    156    2630201344 3 4.25  .729 .385 1000    694    6593449984 1000    979    3025178624 183    168    2772299776 6 6.32  .755 5.78  2.04  .096 .002 .00  .00  .230 1.29  1
email_spec1_product26_false-unreach-call.cil.c 800    776    3228188672 3 6.34  3.96  .297 1000    501    7145947136 1000    977    3306078208 1000    976    3248214016
email_spec1_product29_false-unreach-call.cil.c 169    157    2766667776 3 3.80  .524 .252 1000    729    6379610112 1000    977    3155820544 187    170    3070951424 6 10.1   .983 9.32  3.41  .059 .001 .00  .00  .506 2.32  1
email_spec1_product30_false-unreach-call.cil.c 155    144    2623008768 3 4.11  .784 .295 1000    699    6299815936 1000    981    2832674816 184    168    2739290112 6 5.36  .251 6.87  2.22  .073 .004 .00  .00  .105 1.95  1
email_spec1_product31_false-unreach-call.cil.c 145    131    2753433600 3 4.21  .673 .211 1000    685    6791446528 1000    976    3024019456 202    186    2782269440 6 5.69  .386 7.07  2.32  .087 .001 .00  .00  .283 1.89  1
email_spec1_product32_false-unreach-call.cil.c 655    632    3219218432 3 6.81  3.48  .261 1000    501    7201665024 1000    977    3280826368 1000    977    3281887232
email_spec1_product33_false-unreach-call.cil.c 174    158    2770472960 3 4.39  .967 .307 1000    676    6773972992 1000    979    2988167168 203    187    2799403008 6 5.33  .297 7.61  2.52  .036 .002 .00  .00  .282 2.00  1
email_spec1_product34_false-unreach-call.cil.c 902    879    3292954624 3 8.56  2.54  .258 1000    501    7455313920 1000    977    3287384064 1000    976    3291426816
email_spec1_product35_false-unreach-call.cil.c 965    943    3300306944 3 6.33  5.17  .352 1000    501    7346753536 1000    977    3378270208 1000    976    3264794624
email_spec1_productSimulator_false-unreach-call.cil.c 1000    971    4463611904 1000    501    8022781952 902    880    1895251968 2.08  846     873     15.6   844     844     21.7   812     833     819     1000    962    5628964864
email_spec27_product17_false-unreach-call.cil.c 357    346    2765504512 3 3.49  .508 .356 1000    501    6274134016 902    885    883068928 .692 875     880     2.05  875     875     3.93  862     866     872     224    208    3021271040 6 11.3   .406 7.16  3.12  .063 .002 .00  .00  .425 1.45  1
email_spec27_product18_false-unreach-call.cil.c 233    222    2624438272 3 3.75  .658 .237 1000    556    6429462528 1000    981    2770452480 167    153    2749464576 6 6.17  .689 5.24  1.88  .059 .001 .00  .00  .161 .985 1
email_spec27_product19_false-unreach-call.cil.c 291    279    2618368000 3 3.85  .969 .301 1000    584    6167572480 1000    979    2929430528 187    172    2760302592 6 6.70  .325 5.42  1.96  .054 .001 .00  .00  .168 1.11  1
email_spec27_product23_false-unreach-call.cil.c 953    932    3186667520 3 5.74  4.29  .271 1000    501    6888345600 902    882    902488064 .991 871     876     2.69  871     871     3.89  858     862     868     1000    980    3120484352
email_spec27_product24_false-unreach-call.cil.c 236    224    2677403648 3 4.22  .809 .425 1000    576    6220177408 1000    980    3014373376 195    179    2764591104 6 6.50  .286 6.33  2.58  .052 .001 .00  .00  .220 1.42  1
email_spec27_product25_false-unreach-call.cil.c 1000    977    3215736832 1000    501    7053430784 902    884    980959232 1.30  872     878     2.65  872     872     7.83  854     862     865     1000    979    3209224192
email_spec27_product27_false-unreach-call.cil.c 1000    979    3263320064 1000    501    7343968256 902    882    1019326464 1.57  869     876     3.40  868     868     8.92  848     857     860     1000    974    3276288000
email_spec27_product29_false-unreach-call.cil.c 376    360    2929532928 3 3.82  .862 .234 1000    501    7343742976 1000    977    3211317248 226    209    3049218048 6 12.4   .371 7.51  2.86  .075 .008 .00  .00  .259 1.55  1
email_spec27_product30_false-unreach-call.cil.c 325    313    2728300544 3 4.73  1.07  .251 1000    513    7200337920 1000    982    2860871680 250    235    2754068480 6 5.16  .269 6.41  2.56  .037 .003 .00  .00  .151 1.40  1
email_spec27_product31_false-unreach-call.cil.c 286    271    2822045696 3 4.40  .941 .267 1000    538    7102279680 1000    982    2904842240 194    177    2871238656 6 6.28  .362 7.27  2.91  .095 .001 .00  .00  .252 1.75  1
email_spec27_product32_false-unreach-call.cil.c 1000    977    3304640512 1000    501    7526285312 1000    976    3354079232 1000    978    3265650688
email_spec27_product33_false-unreach-call.cil.c 334    317    2844008448 3 5.19  1.23  .241 1000    501    7687585792 1000    978    3042279424 201    185    2872516608 6 6.12  .713 7.88  2.47  .040 .001 .00  .00  .170 2.39  1
email_spec27_product34_false-unreach-call.cil.c 1000    977    3288948736 1000    501    7541592064 1000    976    3435171840 1000    975    3324821504
email_spec27_product35_false-unreach-call.cil.c 1000    976    3338141696 1000    501    8035278848 902    884    934522880 1.01  873     878     2.92  872     872     5.12  861     866     867     1000    975    3355484160
email_spec27_productSimulator_false-unreach-call.cil.c 1000    968    4874584064 1000    501    8725360640 903    873    3759460352 1.89  830     866     17.7   827     827     647     16.3   663     18.5   905    870    4176318464 1 753     2.88  48.3   25.2   .681 .028 .00  .00  9.57  .627 0
email_spec3_product13_false-unreach-call.cil.c 14.6  7.92 449478656 1 1.51  .003 903    806    4685447168 1 5.65  .049 733     1000    980    2931736576 287    271    2758402048 6 5.29  .232 4.99  1.68  .043 .002 .00  .00  .111 1.03  1
email_spec3_product17_false-unreach-call.cil.c 16.7  9.00 452325376 1 1.82  .003 902    807    4713312256 1 5.42  .029 .004 905    883    1068785664 3.82  864     870     2.42  863     863     13.0   835     848     851     1000    975    3194916864
email_spec3_product18_false-unreach-call.cil.c 15.6  8.44 432087040 1 1.76  .004 902    803    5662883840 1 3.09  .209 .021 1000    974    3070562304 1000    978    2871578624
email_spec3_product19_false-unreach-call.cil.c 15.6  8.41 459255808 1 1.87  .015 902    814    5291511808 1 5.53  .036 .005 1000    974    3089301504 1000    979    2902622208
email_spec3_product23_false-unreach-call.cil.c 16.2  8.68 477306880 1 1.79  .003 908    794    5947121664 1 6.32  .015 706     902    884    864292864 1.24  873     878     2.32  873     873     4.53  862     867     869     1000    974    3273195520
email_spec3_product24_false-unreach-call.cil.c 16.5  8.84 453406720 1 1.83  .002 903    794    5755281408 1 4.55  .343 711     1000    974    3078287360 1000    976    2929307648
email_spec3_product25_false-unreach-call.cil.c 16.7  9.02 484884480 1 1.82  .003 903    784    6153580544 1 6.03  .019 685     1000    974    3420037120 1000    976    3268833280
email_spec3_product27_false-unreach-call.cil.c 16.7  9.01 467431424 1 1.70  .002 902    771    6366494720 1 5.33  .032 661     902    884    936841216 1.37  873     878     2.27  872     872     5.70  859     865     868     1000    973    3287515136
email_spec3_product28_false-unreach-call.cil.c 16.6  8.94 471191552 1 2.29  .004 902    803    5069561856 1 5.36  .022 .005 1000    980    2987175936 289    270    2803924992 6 7.83  .299 5.02  2.17  .074 .001 .00  .00  .191 .934 1
email_spec3_product29_false-unreach-call.cil.c 17.0  9.14 450338816 1 1.81  .003 902    801    5921546240 1 5.39  .075 .004 1000    973    3317268480 1000    973    3217981440
email_spec3_product30_false-unreach-call.cil.c 15.5  8.31 468623360 1 1.88  .002 902    789    6163546112 1 5.37  .021 .004 1000    973    3116777472 1000    978    2960285696
email_spec3_product31_false-unreach-call.cil.c 17.3  9.15 465907712 1 1.82  .004 903    792    5939171328 1 5.39  .011 707     1000    977    3005747200 1000    976    3046612992
email_spec3_product32_false-unreach-call.cil.c 16.5  8.84 449519616 1 1.77  .003 902    769    6518104064 1 5.40  .045 .013 903    883    940625920 2.07  870     876     2.57  870     870     6.39  858     864     865     1000    974    3315032064
email_spec3_product33_false-unreach-call.cil.c 16.2  8.76 481583104 1 1.96  .003 902    765    6475051008 1 5.74  .155 .017 1000    974    3170349056 1000    977    3055747072
email_spec3_product34_false-unreach-call.cil.c 16.9  9.18 464302080 1 1.76  .005 902    752    7142518784 1 5.28  .021 .004 902    883    919097344 1.94  871     876     2.04  870     870     6.77  858     865     865     1000    974    3374116864
email_spec3_product35_false-unreach-call.cil.c 17.9  9.58 463048704 1 1.87  .002 902    728    7245975552 1 5.21  .030 575     902    883    963444736 2.08  871     876     2.65  870     870     7.11  858     865     864     1000    974    3363684352
email_spec3_productSimulator_false-unreach-call.cil.c 38.8  24.9  1391112192 1 4.05  .090 907    695    7687184384 1 5.65  .157 .005 904    879    1690759168 4.33  848     867     10.2   847     847     29.1   804     833     812     1000    967    5635235840
email_spec4_product18_false-unreach-call.cil.c 201    190    2613141504 3 3.67  .632 .209 1000    573    6701621248 167    154    2695208960 1.75  4.16  8.58  2.15  3.88  3.79  2.84  .343 3.18  1.50  174    161    2684792832 6 4.71  .686 5.11  1.77  .040 .00  .00  .00  .054 .897 1
email_spec4_product19_false-unreach-call.cil.c 257    246    2636759040 3 4.39  .535 .325 1000    595    6597558272 206    193    2731372544 2.03  4.58  9.10  2.13  4.29  4.25  2.63  .835 3.47  2.17  155    140    2772652032 6 6.61  .806 4.95  1.66  .083 .001 .00  .00  .059 1.00  1
email_spec4_product23_false-unreach-call.cil.c 825    803    3088175104 3 5.21  3.40  .260 1000    501    7456501760 1000    980    3197706240 1000    978    3060568064
email_spec4_product24_false-unreach-call.cil.c 233    222    2679025664 3 4.47  .529 .284 1000    595    6980403200 1000    979    2924163072 175    159    2752454656 6 6.16  .239 5.71  2.38  .056 .003 .00  .00  .123 1.13  1
email_spec4_product25_false-unreach-call.cil.c 918    897    3088076800 3 5.79  3.84  .292 1000    501    6863511552 1000    979    3249217536 1000    978    3091603456
email_spec4_product27_false-unreach-call.cil.c 856    832    3192770560 3 7.38  3.79  .328 1000    501    7620706304 1000    978    3216269312 1000    978    3096064000
email_spec4_product30_false-unreach-call.cil.c 267    254    2655657984 3 4.55  .728 .452 1000    582    6884323328 192    179    2741202944 1.98  4.28  8.77  2.27  4.03  3.95  2.56  .718 3.28  1.89  188    171    2782785536 6 6.64  .267 6.16  2.04  .073 .003 .00  .00  .059 1.57  1
email_spec4_product31_false-unreach-call.cil.c 257    241    2759778304 3 4.32  .731 .214 1000    621    6793084928 1000    980    2848518144 207    191    2792366080 6 5.07  .339 7.38  2.89  .083 .003 .00  .00  .109 1.98  1
email_spec4_product32_false-unreach-call.cil.c 872    849    3239407616 3 6.83  3.11  .262 1000    501    7285383168 1000    979    3259334656 1000    977    3194667008
email_spec4_product33_false-unreach-call.cil.c 294    277    2783424512 3 4.91  1.01  .266 1000    577    7205855232 1000    982    2798256128 211    195    2777997312 6 4.89  .291 7.72  3.10  .062 .001 .00  .00  .102 1.93  1
email_spec4_product34_false-unreach-call.cil.c 832    810    3290464256 3 6.45  2.00  .292 1000    501    7222337536 1000    975    3409739776 1000    976    3273359360
email_spec4_product35_false-unreach-call.cil.c 1000    976    3352588288 1000    501    7894855680 1000    977    3247706112 1000    976    3263418368
email_spec4_productSimulator_false-unreach-call.cil.c 1000    972    4290281472 1000    501    7976943616 1000    965    6080794624 1000    968    5665951744
email_spec6_product12_false-unreach-call.cil.c 119    110    2607882240 3 3.38  .520 .228 1000    742    6246031360 1000    979    2893045760 159    145    2630320128 6 3.83  .268 4.82  2.13  .046 .009 .00  .00  .082 .947 1
email_spec6_product14_false-unreach-call.cil.c 387    376    2752933888 3 3.58  .529 .252 1000    501    6993567744 1000    976    3291860992 1000    979    2932248576
email_spec6_product15_false-unreach-call.cil.c 259    249    2608467968 3 3.73  .513 .274 1000    577    6875176960 1000    978    2980728832 1000    981    2688831488
email_spec6_product16_false-unreach-call.cil.c 226    214    2645385216 3 4.29  .751 .297 1000    578    6776737792 902    885    951164928 .732 875     880     2.34  874     874     3.20  860     863     873     1000    980    2730573824
email_spec6_product20_false-unreach-call.cil.c 894    871    3190968320 3 5.49  3.61  .259 1000    501    7034945536 902    880    1126653952 1.13  868     874     3.08  868     867     11.4   840     852     859     1000    978    3049279488
email_spec6_product21_false-unreach-call.cil.c 1000    979    3187920896 1000    501    7206481920 902    881    1132965888 2.27  865     874     3.68  864     863     22.3   809     831     844     1000    978    3065597952
email_spec6_product22_false-unreach-call.cil.c 224    213    2637164544 3 4.15  .751 .342 1000    551    6888525824 1000    975    3070545920 1000    980    2750275584
email_spec6_product26_false-unreach-call.cil.c 897    873    3282997248 3 7.62  3.10  .457 1000    501    7355011072 1000    978    3423543296 1000    979    3072495616
email_spec6_product28_false-unreach-call.cil.c 110    99.4  2572963840 3 3.79  .538 .193 1000    735    6256582656 1000    983    2828218368 160    144    2762391552 6 5.71  .293 6.24  2.07  .044 .003 .00  .00  .102 1.51  1
email_spec6_product29_false-unreach-call.cil.c 390    377    2864742400 3 3.87  .676 .239 1000    501    7253876736 902    885    1079185408 .557 873     879     3.26  873     872     5.56  848     853     868     1000    979    3008942080
email_spec6_product30_false-unreach-call.cil.c 236    223    2657771520 3 4.53  .832 .283 1000    602    6314737664 1000    979    2994581504 1000    980    2719318016
email_spec6_product31_false-unreach-call.cil.c 284    268    2758430720 3 4.69  .854 .270 1000    531    7263936512 1000    980    2989068288 1000    981    2769297408
email_spec6_product32_false-unreach-call.cil.c 1000    978    3248803840 1000    501    7198351360 902    881    1276604416 1.12  869     876     3.50  868     868     11.5   836     847     857     1000    978    3108298752
email_spec6_product33_false-unreach-call.cil.c 297    280    2805940224 3 5.36  1.18  .273 1000    517    7621562368 1000    976    3106123776 1000    980    2752442368
email_spec6_product34_false-unreach-call.cil.c 1000    979    3244003328 1000    501    7549222912 902    878    1355292672 1.78  864     872     3.69  863     863     19.1   820     839     845     1000    977    3159654400
email_spec6_product35_false-unreach-call.cil.c 1000    977    3320242176 1000    501    7584608256 1000    978    3513122816 1000    976    3171577856
email_spec6_productSimulator_false-unreach-call.cil.c 1000    971    4336873472 1000    501    8089399296 902    880    1603444736 2.42  853     873     10.4   852     851     11.3   832     843     840     1000    965    5269639168
email_spec7_product28_false-unreach-call.cil.c 121    111    2605035520 3 3.16  .657 .197 1000    728    6147776512 1000    980    2841423872 165    151    2683805696 6 3.67  .294 5.11  2.13  .058 .001 .00  .00  .094 1.02  1
email_spec7_product29_false-unreach-call.cil.c 366    353    2827702272 3 3.89  .788 .235 1000    501    6651260928 902    882    1076568064 1.17  869     877     2.99  869     869     9.97  835     845     860     1000    976    3043328000
email_spec7_product30_false-unreach-call.cil.c 268    257    2647449600 3 4.15  1.01  .298 1000    579    6499368960 1000    979    3007266816 1000    981    2674917376
email_spec7_product31_false-unreach-call.cil.c 305    294    2667540480 3 4.44  .865 .216 1000    535    6692958208 1000    976    3209498624 1000    981    2741866496
email_spec7_product32_false-unreach-call.cil.c 1000    976    3245674496 1000    501    7640289280 1000    975    3303981056 1000    979    3029225472
email_spec7_product33_false-unreach-call.cil.c 316    298    2778750976 3 5.04  1.46  .256 1000    576    7010643968 1000    975    3153543168 1000    981    2765598720
email_spec7_product34_false-unreach-call.cil.c 1000    978    3282481152 1000    501    7513182208 902    879    1253302272 1.48  866     873     3.68  865     865     11.7   833     845     854     1000    979    3095990272
email_spec7_product35_false-unreach-call.cil.c 1000    977    3303407616 1000    501    7881551872 1000    980    3417710592 1000    978    3180539904
email_spec7_productSimulator_false-unreach-call.cil.c 1000    969    4556800000 1000    501    7991164928 1000    965    5111959552 1000    964    5560844288
email_spec8_product15_false-unreach-call.cil.c 148    137    2621882368 3 3.77  .611 .230 1000    734    6178148352 175    162    2717667328 1.82  3.86  8.43  2.22  3.59  3.48  2.13  .727 2.86  1.90  190    176    2706497536 6 4.62  .298 5.19  1.99  .061 .003 .00  .00  .067 .938 1
email_spec8_product16_false-unreach-call.cil.c 168    157    2637537280 3 4.08  .587 .332 1000    710    6181666816 1000    983    2825650176 195    179    2737000448 6 5.82  .308 5.74  2.34  .037 .001 .00  .00  .120 1.31  1
email_spec8_product20_false-unreach-call.cil.c 756    734    3108327424 3 5.13  3.96  .286 1000    501    7179239424 1000    974    3267072000 1000    978    3074490368
email_spec8_product21_false-unreach-call.cil.c 683    661    3162468352 3 5.22  5.28  .277 1000    501    7239483392 1000    979    3185229824 1000    978    3105669120
email_spec8_product22_false-unreach-call.cil.c 136    125    2621403136 3 3.76  .686 .302 1000    707    6674841600 1000    981    2862792704 198    183    2739937280 6 5.08  .678 5.60  1.62  .041 .002 .00  .00  .079 1.55  1
email_spec8_product26_false-unreach-call.cil.c 733    709    3207045120 3 8.14  2.90  .285 1000    501    8047702016 902    885    965488640 1.27  874     879     2.64  873     873     7.76  858     866     867     1000    976    3185905664
email_spec8_product30_false-unreach-call.cil.c 183    171    2641944576 3 4.28  .760 .281 1000    720    6637387776 1000    980    2828988416 210    194    2778902528 6 6.16  .695 6.59  2.21  .033 .001 .00  .00  .074 1.77  1
email_spec8_product31_false-unreach-call.cil.c 158    143    2746744832 3 4.38  .769 .299 1000    700    6958198784 1000    981    2832850944 197    182    2762186752 6 5.34  .879 6.61  2.38  .056 .002 .00  .00  .097 1.27  1
email_spec8_product32_false-unreach-call.cil.c 929    904    3230289920 3 8.89  2.34  .287 1000    501    7470354432 1000    977    3233710080 1000    977    3154354176
email_spec8_product33_false-unreach-call.cil.c 173    158    2768449536 3 4.54  .914 .269 1000    682    6665269248 1000    980    2914361344 214    199    2801197056 6 5.39  .421 7.34  3.11  .091 .003 .00  .00  .090 1.50  1
email_spec8_product34_false-unreach-call.cil.c 810    785    3298258944 3 8.54  2.62  .242 1000    501    7551426560 902    886    941973504 1.33  876     881     2.68  875     875     5.18  863     868     871     1000    978    3188875264
email_spec8_product35_false-unreach-call.cil.c 869    845    3310235648 3 6.60  4.14  .256 1000    501    7452835840 902    883    961957888 1.58  870     876     3.25  869     869     9.37  851     860     861     1000    977    3267440640
email_spec8_productSimulator_false-unreach-call.cil.c 1000    973    4308709376 1000    501    8217571328 902    879    2394853376 3.63  826     870     20.8   823     822     40.8   766     806     773     1000    967    5538050048
email_spec9_product15_false-unreach-call.cil.c 153    143    2588463104 3 3.80  .587 .232 1000    737    6094442496 176    164    2720165888 1.93  4.00  8.15  2.19  3.68  3.61  2.28  .683 2.96  2.01  193    178    2699468800 6 5.62  .229 5.29  2.35  .053 .011 .00  .00  .074 .972 1
email_spec9_product16_false-unreach-call.cil.c 124    113    2608177152 3 4.03  .594 .342 1000    735    6160736256 1000    982    2838347776 167    153    2726809600 6 5.36  .290 5.75  2.52  .061 .003 .00  .00  .167 1.28  1
email_spec9_product20_false-unreach-call.cil.c 694    673    3058413568 3 5.57  3.41  .290 1000    501    7254003712 1000    976    3249008640 1000    978    3087937536
email_spec9_product21_false-unreach-call.cil.c 761    739    3150684160 3 5.89  4.40  .283 1000    501    7569272832 1000    976    3225817088 1000    977    3132530688
email_spec9_product22_false-unreach-call.cil.c 144    133    2631749632 3 3.70  .798 .283 1000    704    6605955072 1000    983    2860994560 175    161    2709864448 6 4.38  .619 5.38  1.89  .093 .001 .00  .00  .075 1.15  1
email_spec9_product26_false-unreach-call.cil.c 864    841    3211108352 3 8.89  2.08  .292 1000    501    7311872000 902    884    928473088 1.40  872     878     2.67  871     871     9.38  854     864     863     1000    977    3176923136
email_spec9_product30_false-unreach-call.cil.c 139    128    2635005952 3 4.29  .797 .488 1000    721    6617268224 1000    981    2801238016 182    166    2726473728 6 6.56  .279 6.31  2.72  .050 .002 .00  .00  .056 1.22  1
email_spec9_product31_false-unreach-call.cil.c 158    143    2743599104 3 4.59  .797 .275 1000    686    6887661568 1000    980    2846490624 213    196    2808090624 6 5.32  .436 7.84  2.64  .140 .002 .00  .00  .147 2.15  1
email_spec9_product32_false-unreach-call.cil.c 627    606    3245625344 3 7.88  2.71  .256 1000    501    7575748608 1000    977    3209318400 1000    977    3187220480
email_spec9_product33_false-unreach-call.cil.c 148    134    2742902784 3 4.33  .807 .218 1000    663    6988742656 1000    981    2898640896 162    146    2824011776 6 6.13  .493 6.83  3.03  .082 .003 .00  .00  .125 1.27  1
email_spec9_product34_false-unreach-call.cil.c 735    713    3250339840 3 6.32  1.95  .238 1000    501    7528787968 902    884    946257920 1.36  873     878     2.56  872     872     5.46  859     865     868     1000    976    3252678656
email_spec9_product35_false-unreach-call.cil.c 923    901    3299880960 3 6.65  5.45  .262 1000    501    7504097280 902    884    976859136 1.58  871     878     3.33  871     871     9.45  853     862     862     1000    976    3232186368
email_spec9_productSimulator_false-unreach-call.cil.c 1000    969    4328349696 1000    501    8028262400 902    877    2388942848 3.94  827     869     21.3   823     822     44.0   763     807     770     1000    967    5577220096
email_spec0_product05_true-unreach-call.cil.c 15.7  8.37 410005504 5 2.71  .00  .450 21.1  11.1  509972480 1 3.85  .00  .011 .349 10.1  5.55 387375104 .258 .147 1.30  .386 .043 .037 .001 .00  .001 10.5  5.75 351981568 0 .277 .093 1.32  .487 .012 .002 .00  .00  .00  .007
email_spec0_product09_true-unreach-call.cil.c 24.9  13.0  534843392 5 5.82  .00  .691 33.4  17.1  846413824 1 4.18  .00  .013 .619 12.9  7.07 423657472 1.00  .258 1.90  .548 .124 .105 .011 .00  .011 12.7  7.06 377876480 0 .764 .611 2.01  .712 .013 .002 .00  .00  .00  .010
email_spec0_product10_true-unreach-call.cil.c 16.0  8.57 439472128 5 2.71  .004 .468 28.5  14.7  668405760 1 3.54  .00  .005 .620 10.4  5.71 393048064 .333 .137 1.40  .407 .059 .046 .003 .00  .003 10.6  5.85 369328128 0 .384 .110 1.54  .505 .011 .001 .00  .00  .00  .012
email_spec0_product11_true-unreach-call.cil.c 19.9  10.6  486666240 5 4.04  .00  .781 37.5  19.1  871116800 1 4.11  .001 2.81  .710 5.95 .023 11.9  6.51 416333824 .310 .229 1.92  .944 .066 .033 .001 .00  .001 11.9  6.49 393224192 0 .272 .613 2.08  .728 .465 .447 .00  .00  .00  .006
email_spec0_product19_true-unreach-call.cil.c 22.8  12.1  508227584 5 5.26  .001 .838 47.6  24.3  1143980032 1 5.21  .00  .004 1.29  8.23 .048 13.0  7.16 445521920 .471 .240 2.35  1.21  .074 .050 .003 .00  .003 13.7  7.38 426012672 0 .503 .232 2.56  .943 .064 .001 .00  .00  .00  .022
email_spec0_product24_true-unreach-call.cil.c 24.1  12.9  522575872 5 5.49  .00  .860 49.8  25.5  924278784 1 4.94  .00  3.98  1.54  9.22 .047 13.7  7.43 459874304 .730 .280 2.27  1.08  .122 .073 .004 .00  .004 14.3  7.72 434667520 0 .727 .155 2.67  1.44  .037 .001 .00  .00  .00  .014
email_spec0_product25_true-unreach-call.cil.c 31.9  16.9  864862208 5 8.62  .001 1.76  66.7  33.8  1013796864 1 5.90  .00  .007 1.68  14.8  .071 18.0  9.88 526249984 2.27  .430 3.18  1.48  .239 .174 .035 .00  .035 17.8  9.91 489930752 0 1.96  .218 3.48  1.46  .039 .001 .00  .00  .00  .011
email_spec0_product27_true-unreach-call.cil.c 34.6  18.5  893657088 5 8.89  .001 2.71  69.0  35.0  1061957632 1 5.45  .001 5.52  .996 15.8  .075 18.3  10.2  520536064 2.17  .485 3.58  1.71  .223 .145 .020 .00  .020 24.2  13.0  565325824 0 4.04  .309 3.98  1.74  .060 .002 .00  .00  .00  .011
email_spec0_product36_true-unreach-call.cil.c 25.5  13.5  585596928 5 6.47  .00  .904 48.2  24.6  900579328 1 4.04  .001 .005 .544 9.79 .050 13.3  7.55 457158656 1.19  .298 2.15  .649 .124 .090 .011 .00  .011 13.2  7.48 430190592 0 1.17  .491 2.12  .800 .030 .002 .00  .00  .00  .002
email_spec0_product37_true-unreach-call.cil.c 20.2  10.7  483749888 5 4.14  .00  .990 43.1  22.1  887463936 1 5.16  .025 3.79  .905 6.56 .024 12.3  6.69 436699136 .336 .202 2.14  1.14  .051 .033 .002 .00  .002 12.8  7.00 403693568 0 .352 .159 2.41  .841 .038 .002 .00  .00  .00  .010
email_spec0_product38_true-unreach-call.cil.c 29.2  15.4  636481536 5 6.27  .00  2.12  57.1  29.0  961671168 1 5.81  .00  .009 1.21  10.6  .053 15.2  8.20 462008320 1.13  .276 2.71  1.34  .132 .101 .014 .00  .014 14.9  8.12 395390976 0 1.17  .223 2.73  1.50  .036 .002 .00  .00  .00  .035
email_spec0_product40_true-unreach-call.cil.c 31.0  16.4  712159232 5 7.83  .001 2.27  61.9  31.5  1010028544 1 5.73  .024 5.02  1.82  12.2  .069 16.6  9.07 490409984 1.64  .373 2.97  1.51  .161 .134 .025 .00  .025 15.5  8.58 459952128 0 1.40  .226 3.07  1.26  .039 .001 .00  .00  .00  .030
email_spec11_product03_true-unreach-call.cil.c 15.1  8.20 404500480 5 2.35  .00  .462 25.8  13.3  593256448 1 4.38  .00  .010 .389 10.6  5.83 395853824 .247 .133 1.19  .308 .070 .037 .002 .00  .002 10.6  5.77 364437504 0 .257 .124 1.38  .833 .034 .00  .00  .00  .00  .005
email_spec11_product07_true-unreach-call.cil.c 21.4  11.2  462827520 5 4.74  .00  .656 35.0  18.0  815210496 1 3.14  .002 .011 1.20  12.6  6.98 446484480 .863 .282 1.80  .606 .147 .124 .009 .00  .009 12.4  6.97 412930048 0 .807 .174 1.82  1.01  .023 .002 .00  .00  .00  .007
email_spec11_product08_true-unreach-call.cil.c 17.7  9.54 468058112 5 3.29  .00  .842 39.0  19.9  883269632 1 5.04  .00  2.96  .749 6.14 .023 11.9  6.48 419418112 .335 .201 1.87  .948 .057 .038 .001 .00  .001 12.2  6.69 393740288 0 .302 .156 2.06  1.12  .025 .001 .00  .00  .00  .008
email_spec11_product10_true-unreach-call.cil.c 16.2  8.70 441192448 5 3.04  .00  .488 27.8  14.3  625729536 1 3.05  .00  .006 1.30  11.4  6.19 396988416 .355 .126 1.45  .377 .048 .040 .002 .00  .002 10.7  5.87 378388480 0 .326 .123 1.48  .444 .022 .002 .00  .00  .00  .001
email_spec11_product18_true-unreach-call.cil.c 21.7  11.5  500875264 5 4.70  .00  .996 46.7  23.8  863404032 1 5.34  .00  3.78  1.35  7.37 .045 12.4  6.82 443662336 .432 .190 2.22  1.22  .062 .045 .003 .00  .003 13.1  7.13 420851712 0 .463 .147 2.60  1.40  .037 .001 .00  .00  .00  .019
email_spec11_product23_true-unreach-call.cil.c 31.3  16.3  777584640 5 7.27  .00  2.31  67.4  34.2  980078592 1 5.30  .00  5.47  1.49  14.0  .046 17.3  9.48 507961344 2.02  .390 3.13  1.62  .173 .145 .016 .00  .016 16.0  8.93 463966208 0 1.53  .280 3.28  1.87  .072 .001 .00  .00  .00  .009
email_spec11_product24_true-unreach-call.cil.c 25.2  13.3  561577984 5 5.42  .001 1.37  48.2  24.6  884334592 1 5.61  .00  .003 1.04  8.64 .029 14.0  7.60 448061440 .543 .277 2.40  1.16  .125 .061 .004 .00  .004 14.1  7.67 429957120 0 .479 .560 2.76  1.12  .066 .002 .00  .00  .00  .016
email_spec11_product27_true-unreach-call.cil.c 33.9  18.1  911052800 5 9.15  .00  2.23  70.0  35.4  1001500672 1 5.17  .00  5.76  1.91  14.5  .045 18.5  10.3  517656576 2.09  .415 3.60  1.72  .158 .116 .021 .00  .021 20.4  11.2  530391040 0 2.36  .720 3.92  1.69  .048 .001 .00  .00  .00  .022
email_spec11_product36_true-unreach-call.cil.c 23.6  12.5  539082752 5 6.07  .00  .555 47.7  24.3  919089152 1 4.05  .001 .006 .534 9.89 .033 13.7  7.72 441012224 1.21  .273 2.18  .727 .134 .093 .009 .00  .009 13.5  7.57 427286528 0 1.16  .211 2.24  1.28  .026 .002 .00  .00  .00  .008
email_spec11_product37_true-unreach-call.cil.c 20.3  10.9  493547520 5 4.09  .00  .870 42.2  21.6  898686976 1 4.47  .001 3.28  .788 7.11 .043 12.8  6.95 408522752 .339 .226 2.07  1.09  .070 .028 .002 .00  .002 12.6  6.90 374374400 0 .334 .166 2.40  .847 .014 .001 .00  .00  .00  .009
email_spec11_product39_true-unreach-call.cil.c 24.8  13.2  560594944 5 5.46  .001 1.11  50.3  25.6  876392448 1 4.94  .028 4.14  1.25  9.37 .044 14.5  7.86 468148224 1.23  .394 2.41  1.14  .186 .153 .018 .00  .018 15.3  8.33 439799808 0 1.14  .206 2.92  1.15  .043 .001 .00  .00  .00  .017
email_spec11_product40_true-unreach-call.cil.c 30.1  15.8  739708928 5 6.84  .001 2.59  60.6  30.7  980054016 1 5.04  .001 .010 1.04  11.4  .090 16.0  8.71 482668544 1.48  .285 2.88  1.48  .140 .083 .011 .00  .011 15.6  8.64 460222464 0 1.31  .182 2.85  1.53  .047 .002 .00  .00  .00  .024
email_spec1_product12_true-unreach-call.cil.c 17.8  9.65 443248640 5 3.17  .001 .908 71.6  36.3  1475076096 3 7.75  .00  .004 4.77  10.3  4.56  16.1  8.58 447336448 .390 1.45  3.66  1.12  1.27  1.22  .904 .020 .924 .394 13.3  7.13 383180800 1 .465 .174 2.50  .940 .027 .009 .00  .00  .013 .130 1
email_spec1_product28_true-unreach-call.cil.c 20.7  11.0  503771136 5 4.07  .00  1.05  93.7  47.4  1565741056 4 10.2   .00  .006 5.01  12.9  9.96  17.8  9.58 510386176 .439 1.83  4.61  1.34  1.50  1.47  1.17  .010 1.18  .293 14.5  7.82 436449280 1 .624 .180 2.90  1.66  .023 .001 .00  .00  .007 .084 1
email_spec27_product13_true-unreach-call.cil.c 21.1  11.6  517562368 5 3.65  1.41  .752 87.6  44.2  1307975680 3 8.26  1.92  8.83  3.14  12.5  9.29  25.1  14.3  508219392 .585 5.71  9.39  1.86  5.41  5.34  2.48  2.25  4.72  3.43  17.3  9.51 467365888 3 1.03  .249 3.93  1.83  .058 .002 .00  .00  .048 .503 1
email_spec27_product28_true-unreach-call.cil.c 22.2  12.2  530432000 5 4.10  1.17  .858 99.5  50.3  1672744960 4 7.87  1.93  .004 2.52  15.0  13.5   26.1  15.4  529551360 .702 5.96  10.2   2.27  5.70  5.65  3.14  1.85  5.00  2.76  19.5  10.4  513548288 3 1.70  .241 4.22  1.90  .032 .001 .00  .00  .042 .757 1
email_spec4_product13_true-unreach-call.cil.c 20.5  11.0  506798080 5 3.56  .920 .795 82.7  41.9  1323245568 3 8.11  1.48  8.80  3.50  11.6  8.15  15.8  8.57 461451264 .341 1.40  3.67  1.19  1.19  1.14  .877 .010 .887 .413 12.8  6.96 414838784 1 .496 .594 2.32  .821 .421 .386 .00  .00  .007 .091 1
email_spec4_product17_true-unreach-call.cil.c 22.4  12.6  533278720 5 4.41  .954 .810 94.6  47.8  1537626112 3 9.27  .945 11.8   3.48  16.1  8.05  33.2  20.2  749535232 .598 9.75  15.3   2.79  9.40  9.23  6.26  1.59  7.85  3.26  36.3  20.3  676245504 5 8.47  .334 7.17  2.56  .060 .004 .00  .00  .189 1.60  1
email_spec4_product28_true-unreach-call.cil.c 20.7  11.4  497324032 5 4.03  .773 .746 98.4  49.8  1660366848 5 9.99  1.71  13.5   2.26  13.9  10.2   24.2  13.6  529457152 .648 4.14  8.44  2.23  3.80  3.73  2.42  .648 3.07  1.86  16.7  9.19 470913024 3 1.07  .293 3.83  1.81  .077 .001 .00  .00  .022 .375 1
email_spec4_product29_true-unreach-call.cil.c 32.5  17.5  727855104 5 5.69  2.53  2.10  123    62.1  2491113472 5 10.3   2.33  23.1   2.79  20.5  13.2   33.2  21.1  792907776 .869 10.1   15.6   2.66  9.64  9.55  7.20  .846 8.04  2.51  37.0  21.9  765267968 5 9.31  .441 8.07  3.42  .089 .001 .00  .00  .182 1.66  1
email_spec7_product13_true-unreach-call.cil.c 18.2  9.90 489893888 5 3.29  .00  .873 45.5  23.3  894140416 1 5.57  .001 3.75  1.52  7.00 .023 12.4  6.78 410558464 .307 .244 2.04  1.00  .052 .030 .003 .00  .003 13.3  7.21 389042176 0 .434 .159 2.48  1.46  .021 .001 .00  .00  .00  .004
email_spec7_product17_true-unreach-call.cil.c 21.3  11.5  502026240 5 4.41  .001 .928 63.0  32.1  993153024 1 5.72  .00  5.53  1.81  11.1  .032 16.5  9.11 477712384 1.49  .336 3.08  1.55  .148 .107 .013 .00  .013 15.6  8.66 419434496 0 1.30  .672 3.05  1.18  .056 .002 .00  .00  .00  .011
email_spec7_product18_true-unreach-call.cil.c 20.6  11.0  486436864 5 4.21  .00  .957 43.3  22.1  879906816 1 4.39  .020 3.45  .837 7.49 .018 12.1  6.65 428847104 .306 .175 2.13  1.14  .055 .034 .003 .00  .003 13.2  7.11 417812480 0 .504 .195 2.29  .982 .031 .002 .00  .00  .00  .026
email_spec7_product19_true-unreach-call.cil.c 22.4  11.9  487469056 5 4.89  .00  .918 47.1  24.1  907300864 1 5.03  .00  3.97  .766 8.79 .042 12.6  6.93 439181312 .421 .183 2.19  1.18  .072 .051 .003 .00  .003 13.6  7.33 403959808 0 .445 .234 2.56  1.44  .037 .001 .00  .00  .00  .011
email_spec7_product23_true-unreach-call.cil.c 33.3  17.3  791625728 5 8.27  .002 2.28  60.1  30.4  984834048 1 5.51  .001 4.69  .957 13.1  .052 16.7  9.23 494624768 1.64  .311 3.09  1.51  .124 .106 .017 .00  .017 15.8  8.78 419860480 0 1.23  .292 3.19  1.67  .063 .001 .00  .00  .00  .015
email_spec7_product24_true-unreach-call.cil.c 25.3  13.5  569810944 5 5.43  .003 .953 53.5  27.3  891097088 1 6.17  .001 4.31  1.27  8.97 .042 12.8  6.88 435085312 .397 .197 2.24  1.15  .057 .034 .003 .00  .003 13.8  7.46 425046016 0 .503 .734 2.65  .953 .060 .012 .00  .00  .00  .013
email_spec7_product25_true-unreach-call.cil.c 34.3  18.3  872493056 5 9.41  .00  1.90  70.4  35.7  965881856 1 5.77  .00  5.85  1.53  14.3  .032 17.6  9.72 512036864 1.68  .363 3.42  1.68  .182 .146 .013 .00  .013 16.9  9.37 487514112 0 1.66  .224 3.25  1.36  .055 .00  .00  .00  .00  .024
email_spec7_product27_true-unreach-call.cil.c 34.2  18.4  900726784 5 9.11  .001 2.48  67.8  34.3  988807168 1 5.46  .00  5.61  1.34  14.0  .057 19.0  10.3  530718720 2.15  .393 3.67  1.80  .167 .124 .014 .00  .014 17.1  9.61 481206272 0 1.67  .197 3.49  1.71  .043 .002 .00  .00  .00  .035
email_spec8_product12_true-unreach-call.cil.c 18.6  9.90 485339136 5 3.32  .00  .940 74.6  37.7  1059332096 3 7.80  .00  .013 3.46  12.2  5.04  15.0  8.17 453287936 .367 1.01  3.47  .775 .831 .799 .607 .008 .615 .344 13.1  7.18 420077568 1 .427 .517 2.41  .956 .036 .007 .00  .00  .005 .065 1
email_spec8_product14_true-unreach-call.cil.c 22.3  12.6  536801280 5 4.56  1.11  .857 96.1  48.5  1544749056 3 7.94  1.46  .005 3.44  17.4  7.53  550    532    954863616 2.38  517     525     3.56  516     516     20.3   488     509     497     49.1  32.2  881381376 14 15.6   .428 11.9   3.51  .115 .002 .00  .00  1.05  5.21  1
email_spec8_product28_true-unreach-call.cil.c 20.1  10.8  490889216 5 4.03  .001 .884 93.3  47.4  1560080384 4 9.79  .002 .005 2.65  12.7  12.2   17.0  9.17 513286144 .413 1.89  4.33  1.24  1.69  1.66  1.35  .009 1.36  .477 14.0  7.63 429846528 1 .477 .580 2.77  1.03  .382 .001 .00  .00  .007 .131 1
email_spec8_product29_true-unreach-call.cil.c 31.2  16.9  712159232 5 5.80  2.98  1.28  123    62.2  2545819648 5 9.24  2.54  24.1   2.77  21.1  13.8   902    883    1035370496 1.97  869     877     3.71  868     868     12.1   841     853     858     58.9  43.9  939020288 19 22.7   .552 16.3   3.73  .111 .003 .00  .00  1.85  8.43  1
email_spec9_product12_true-unreach-call.cil.c 18.7  9.98 496164864 5 3.32  .00  .940 72.2  36.6  1039618048 3 7.81  .002 .014 4.99  10.7  3.77  15.6  8.36 463265792 .384 1.30  3.48  1.07  1.11  1.06  .838 .022 .860 .264 13.3  7.23 417021952 1 .439 .568 2.39  .825 .047 .012 .00  .00  .006 .097 1
email_spec9_product14_true-unreach-call.cil.c 24.2  13.5  571711488 5 4.18  1.64  .842 95.2  48.1  1584726016 3 8.92  1.59  12.3   2.59  16.3  7.41  544    527    972898304 2.29  512     520     3.34  511     511     19.9   484     504     492     49.5  32.5  887267328 14 15.5   .871 12.3   3.17  .111 .005 .00  .00  1.10  5.60  1
email_spec9_product28_true-unreach-call.cil.c 20.7  11.1  491352064 5 4.21  .001 .888 92.9  47.0  1499754496 5 9.54  .001 .005 4.12  12.6  10.8   16.0  8.74 480866304 .427 1.26  4.04  1.46  1.11  1.08  .861 .009 .870 .271 13.6  7.39 394780672 1 .517 .186 2.52  .912 .014 .001 .00  .00  .005 .072 1
email_spec9_product29_true-unreach-call.cil.c 31.2  17.1  708288512 5 5.67  2.71  1.44  122    61.7  2711949312 5 9.35  2.80  23.7   3.00  19.3  12.7   902    884    1086132224 1.72  872     878     2.71  871     871     11.0   843     854     862     62.8  45.5  1004945408 19 23.6   .579 17.1   4.50  .155 .001 .00  .00  1.95  8.67  1
minepump_spec1_product33_false-unreach-call.cil.c 8.39 4.72 343687168 1 .761 .013 19.9  10.3  499462144 1 .919 .065 1.55  9.52 5.40 376913920 .681 .278 .669 .175 .143 .129 .059 .001 .060 .048 8.74 4.92 341680128 1 .256 .529 .961 .190 .014 .001 .00  .00  .004 .022 1
minepump_spec1_product34_false-unreach-call.cil.c 8.27 4.63 343511040 1 .721 .013 19.1  10.0  505856000 1 .755 .047 1.57  8.67 4.91 367644672 .689 .207 .615 .175 .148 .138 .061 .00  .061 .039 8.44 4.75 344018944 1 .271 .084 .919 .614 .006 .001 .00  .00  .003 .017 1
minepump_spec1_product35_false-unreach-call.cil.c 8.75 4.92 359112704 1 .777 .015 17.7  9.30 440578048 1 .781 .044 1.48  8.95 5.05 376557568 .696 .221 .670 .195 .149 .133 .056 .00  .056 .035 8.41 4.77 332996608 1 .253 .070 .956 .208 .009 .00  .00  .00  .004 .018 1
minepump_spec1_product36_false-unreach-call.cil.c 8.16 4.59 346685440 1 .717 .019 16.6  8.70 467955712 1 .578 .039 1.09  8.67 4.92 371068928 .561 .236 .653 .198 .153 .143 .059 .002 .061 .043 8.48 4.77 342495232 1 .266 .538 .958 .225 .008 .001 .00  .00  .004 .017 1
minepump_spec1_product37_false-unreach-call.cil.c 8.36 4.70 347717632 1 .821 .010 18.4  9.67 483549184 1 .883 .087 .005 9.18 5.22 380293120 .738 .292 .812 .198 .183 .159 .089 .00  .089 .042 8.53 4.82 343502848 1 .627 .089 .649 .270 .012 .006 .00  .00  .004 .028 1
minepump_spec1_product38_false-unreach-call.cil.c 8.25 4.71 351748096 1 .605 .013 22.5  11.7  527110144 1 1.18  .104 1.63  8.72 4.93 384282624 .659 .254 .791 .248 .166 .156 .075 .002 .077 .049 8.48 4.82 346636288 1 .692 .068 .648 .266 .005 .00  .00  .00  .004 .022 1
minepump_spec1_product39_false-unreach-call.cil.c 8.89 5.00 356122624 1 .802 .018 22.4  11.7  528871424 1 1.06  .072 1.71  9.51 5.35 373682176 .911 .265 .826 .230 .185 .171 .083 .002 .085 .043 8.91 4.98 346025984 1 .320 .087 1.18  .777 .012 .008 .00  .00  .007 .037 1
minepump_spec1_product40_false-unreach-call.cil.c 8.87 4.93 354488320 1 .773 .019 21.3  11.1  511946752 1 1.27  .099 1.68  9.39 5.27 382128128 .737 .245 .810 .230 .164 .153 .089 .001 .090 .048 9.09 5.11 348635136 1 .287 .078 1.18  .304 .012 .002 .00  .00  .003 .023 1
minepump_spec1_product41_false-unreach-call.cil.c 9.03 5.08 366772224 2 .870 .083 .016 32.2  16.5  708833280 2 1.27  .338 2.50  .096 5.11 .953 11.0  6.17 396021760 1.09  .603 1.27  .276 .488 .467 .287 .018 .305 .178 9.16 5.16 359084032 2 .860 .073 .694 .294 .004 .001 .00  .00  .369 .066 1
minepump_spec1_product42_false-unreach-call.cil.c 9.67 5.39 372146176 2 .999 .129 .015 32.9  16.9  685060096 2 1.34  .363 2.53  .032 4.61 .882 10.7  6.05 398110720 .852 .655 1.35  .292 .564 .548 .360 .018 .378 .215 9.26 5.25 359710720 2 .472 .094 1.26  .817 .012 .001 .00  .00  .013 .059 1
minepump_spec1_product43_false-unreach-call.cil.c 9.31 5.23 363614208 2 .865 .118 .018 36.8  18.8  725319680 2 1.42  .404 2.67  .063 4.14 2.41  10.7  6.06 391446528 1.01  .654 1.35  .269 .530 .509 .307 .029 .336 .207 9.32 5.26 349650944 2 .862 .098 .728 .272 .013 .002 .00  .00  .011 .064 1
minepump_spec1_product44_false-unreach-call.cil.c 9.52 5.38 362573824 2 .910 .066 .018 36.9  19.0  754003968 2 1.45  .562 2.87  .231 4.75 .859 10.3  5.87 391409664 .891 .588 1.26  .237 .493 .479 .298 .026 .324 .194 9.63 5.43 363659264 2 .921 .075 .740 .261 .013 .001 .00  .00  .012 .064 1
minepump_spec1_product49_false-unreach-call.cil.c 9.05 5.02 351961088 1 .779 .011 18.8  9.78 467795968 1 1.32  .126 1.32  10.1  5.72 383864832 .760 .292 .902 .260 .211 .190 .101 .003 .104 .051 8.64 4.90 350703616 1 .285 .098 1.11  .243 .011 .001 .00  .00  .003 .029 1
minepump_spec1_product50_false-unreach-call.cil.c 8.95 5.00 354291712 1 .784 .014 22.2  11.6  495833088 1 1.15  .068 1.74  9.61 5.37 383787008 .781 .279 .766 .230 .189 .173 .092 .002 .094 .049 8.85 4.97 343040000 1 .751 .065 .709 .308 .006 .001 .00  .00  .004 .021 1
minepump_spec1_product51_false-unreach-call.cil.c 8.44 4.73 349540352 1 .741 .013 24.6  12.7  570961920 1 1.27  1.07  .009 9.26 5.24 374628352 .756 .280 .842 .267 .192 .175 .108 .002 .110 .046 9.02 5.05 349990912 1 .295 .102 1.19  .293 .006 .002 .00  .00  .003 .025 1
minepump_spec1_product52_false-unreach-call.cil.c 8.96 5.05 355794944 1 .832 .014 22.4  11.7  496160768 1 1.24  .093 1.64  9.49 5.34 378265600 .808 .281 .820 .241 .199 .183 .098 .003 .101 .060 9.02 5.09 348553216 1 .301 .502 1.10  .260 .016 .00  .00  .00  .003 .025 1
minepump_spec1_product53_false-unreach-call.cil.c 9.04 5.04 345522176 1 .699 .010 24.4  12.6  569204736 1 1.66  .092 1.61  11.3  6.33 391241728 .418 .359 1.68  .373 .253 .222 .122 .002 .124 .070 9.50 5.35 347230208 1 .328 .142 1.46  .364 .013 .001 .00  .00  .003 .029 1
minepump_spec1_product54_false-unreach-call.cil.c 9.18 5.08 356392960 1 .757 .010 25.8  13.4  581390336 1 1.56  .622 2.00  9.82 5.59 397475840 .335 .371 1.53  .362 .255 .220 .145 .002 .147 .064 9.43 5.35 355278848 1 .343 .087 1.43  .394 .017 .001 .00  .00  .003 .026 1
minepump_spec1_product55_false-unreach-call.cil.c 9.04 5.04 360624128 1 .784 .013 27.2  14.0  628162560 1 1.94  .554 2.10  10.1  5.67 383307776 .396 .408 1.63  .288 .278 .253 .159 .002 .161 .068 9.80 5.43 364650496 1 .398 .102 1.36  .834 .014 .001 .00  .00  .004 .034 1
minepump_spec1_product56_false-unreach-call.cil.c 9.27 5.19 360980480 1 .763 .014 24.2  12.5  537567232 1 1.52  .204 1.78  10.4  5.84 390586368 .774 .459 1.26  .330 .356 .335 .213 .003 .216 .091 9.89 5.50 363978752 1 .404 .107 1.47  .463 .005 .001 .00  .00  .004 .039 1
minepump_spec1_productSimulator_false-unreach-call.cil.c 13.8  7.45 442527744 1 1.81  .088 37.3  19.1  782004224 1 3.33  .350 3.06  16.8  9.11 458502144 1.12  1.32  3.93  1.00  .627 .588 .392 .005 .397 .198 12.4  6.84 397516800 1 .634 .194 2.44  .857 .025 .001 .00  .00  .004 .044 1
minepump_spec2_product33_false-unreach-call.cil.c 9.27 5.15 357756928 2 .898 .041 .023 32.5  16.7  725958656 2 1.16  .236 2.61  .095 4.06 1.49  9.60 5.43 386723840 .755 .588 1.14  .255 .493 .479 .263 .022 .285 .309 10.6  6.02 368734208 6 .606 .448 1.71  .313 .363 .350 .213 .017 .258 .155 1 .237
minepump_spec2_product34_false-unreach-call.cil.c 9.26 5.14 355528704 2 .864 .057 .034 33.3  17.1  728018944 2 1.09  .222 2.69  .133 3.16 2.82  10.3  5.85 379342848 .844 .529 1.18  .269 .438 .425 .238 .029 .267 .304 9.91 5.59 352387072 3 .491 .729 1.36  .272 .648 .637 .537 .016 .572 .077 1 .559
minepump_spec2_product35_false-unreach-call.cil.c 9.47 5.30 368418816 2 .916 .082 .020 35.4  18.2  740921344 2 1.29  .277 2.77  .105 4.81 1.50  10.9  6.12 392122368 .863 .563 1.26  .271 .486 .473 .270 .031 .301 .322 9.57 5.39 353820672 3 .464 .355 1.47  .296 .269 .266 .162 .014 .191 .073 1 .181
minepump_spec2_product36_false-unreach-call.cil.c 9.13 5.12 363319296 2 .931 .036 .020 34.8  17.9  734400512 2 1.22  .241 3.09  .334 4.17 1.38  10.6  5.97 391897088 .868 .591 1.20  .257 .486 .477 .267 .034 .301 .321 9.67 5.49 357404672 3 .492 .760 1.39  .228 .637 .629 .136 .015 .168 .077 1 .159
minepump_spec2_product41_false-unreach-call.cil.c 10.1  5.66 368726016 3 1.07  .118 .063 53.0  27.1  929972224 3 1.73  .570 4.55  1.22  7.80 5.82  11.8  6.61 409071616 .905 .977 1.97  .381 .875 .847 .561 .043 .604 .639 12.1  6.97 383098880 8 1.00  .681 2.29  .882 .576 .562 .368 .036 .445 .324 1 .409
minepump_spec2_product42_false-unreach-call.cil.c 10.4  5.81 375857152 3 1.21  .105 .065 48.7  25.0  909230080 3 1.84  .747 4.57  1.29  7.33 4.49  11.6  6.55 409567232 .880 .893 1.95  .390 .775 .728 .433 .046 .479 .507 11.6  6.59 369524736 5 .747 .554 2.02  .901 .460 .449 .296 .027 .353 .194 1 .334
minepump_spec2_product43_false-unreach-call.cil.c 10.2  5.74 384045056 3 1.16  .117 .075 50.0  25.6  944562176 3 1.94  .758 4.44  1.33  8.21 4.37  11.6  6.52 402952192 .878 1.01  1.92  .341 .860 .842 .474 .085 .559 .616 10.8  6.21 372719616 5 .740 .963 1.90  .390 .468 .451 .304 .018 .348 .184 1 .329
minepump_spec2_product44_false-unreach-call.cil.c 10.1  5.64 375189504 3 1.14  .116 .076 54.9  28.0  949317632 3 1.79  .870 5.04  1.34  8.19 5.91  12.4  6.97 413966336 .971 1.23  2.21  .376 1.08  1.06  .600 .123 .723 .774 11.3  6.49 369356800 5 .787 .579 1.98  .354 .485 .471 .318 .025 .372 .186 1 .350
minepump_spec2_productSimulator_false-unreach-call.cil.c 16.0  8.71 495931392 2 2.73  .072 .222 63.1  32.0  1431203840 2 4.30  .183 7.24  .408 14.2  .657 21.5  11.7  518885376 1.25  1.83  5.79  1.33  1.43  1.36  .823 .125 .948 .970 19.9  10.8  471883776 3 2.02  1.21  4.39  1.38  1.04  1.01  .636 .042 .697 .159 1 .698
minepump_spec3_product01_false-unreach-call.cil.c 8.03 4.53 342532096 1 .648 .013 12.0  6.41 378494976 1 .598 .010 .014 8.73 4.90 366080000 .617 .170 .548 .180 .120 .108 .032 .001 .033 .031 8.12 4.62 331886592 1 .226 .050 .823 .188 .008 .002 .00  .00  .007 .023 1
minepump_spec3_product02_false-unreach-call.cil.c 8.59 4.82 342536192 1 .879 .009 14.6  7.71 442228736 1 .619 .012 .009 8.89 5.00 365936640 .691 .162 .507 .136 .106 .100 .036 .001 .037 .040 8.37 4.71 327770112 1 .228 .052 .976 .163 .006 .00  .00  .00  .018 .598 1
minepump_spec3_product03_false-unreach-call.cil.c 8.44 4.71 339189760 1 .796 .008 15.9  8.38 441159680 1 .660 .022 1.15  8.25 4.68 373682176 .660 .159 .493 .146 .105 .101 .034 .003 .037 .041 8.17 4.60 340193280 1 .217 .034 .798 .188 .006 .001 .00  .00  .007 .417 1
minepump_spec3_product04_false-unreach-call.cil.c 8.35 4.69 345960448 1 .734 .008 19.1  10.0  471752704 1 .726 .038 .010 8.50 4.79 362082304 .715 .167 .535 .180 .110 .100 .039 .001 .040 .033 8.38 4.67 332447744 1 .709 .038 .445 .206 .007 .001 .00  .00  .006 .043 1
minepump_spec3_product05_false-unreach-call.cil.c 8.28 4.63 336416768 1 .678 .008 16.7  8.79 448544768 1 .550 .022 .008 8.70 4.91 368144384 .666 .229 .650 .177 .152 .129 .062 .00  .062 .040 8.44 4.77 336523264 1 .266 .097 .889 .593 .011 .001 .00  .00  .009 .028 1
minepump_spec3_product06_false-unreach-call.cil.c 8.37 4.69 342282240 1 .630 .009 16.9  8.93 475652096 1 .539 .016 1.14  8.91 5.02 369745920 .613 .226 .617 .166 .127 .119 .049 .001 .050 .031 8.29 4.62 340041728 1 .737 .050 .459 .180 .006 .001 .00  .00  .007 .025 1
minepump_spec3_product07_false-unreach-call.cil.c 8.32 4.66 345796608 1 .683 .010 14.2  7.47 379543552 1 .446 .034 .004 8.58 4.82 376242176 .646 .211 .641 .186 .136 .130 .060 .001 .061 .047 8.97 4.99 338944000 1 .279 .084 .980 .191 .016 .002 .00  .00  .007 .026 1
minepump_spec3_product08_false-unreach-call.cil.c 8.60 4.79 346136576 1 .708 .010 21.1  11.1  520409088 1 .862 .345 1.83  9.04 5.10 375398400 .741 .230 .632 .170 .138 .129 .051 .001 .052 .036 8.55 4.82 336850944 1 .710 .059 .433 .184 .010 .001 .00  .00  .007 .021 1
minepump_spec3_product09_false-unreach-call.cil.c 8.34 4.69 332660736 1 .728 .015 16.6  8.81 506097664 1 .801 .010 1.25  8.50 4.78 373280768 .611 .173 .526 .164 .109 .096 .035 .00  .035 .037 8.06 4.55 343404544 1 .216 .056 .764 .530 .010 .00  .00  .00  .009 .024 1
minepump_spec3_product10_false-unreach-call.cil.c 8.40 4.75 344764416 1 .697 .009 17.5  9.22 488947712 1 .676 .013 .011 9.30 5.17 368496640 .708 .148 .548 .169 .098 .093 .037 .001 .038 .034 8.35 4.71 335159296 1 .596 .049 .409 .147 .009 .001 .00  .00  .007 .045 1
minepump_spec3_product11_false-unreach-call.cil.c 8.47 4.78 339021824 1 .695 .006 15.5  8.20 449306624 1 .699 .024 1.18  8.64 4.84 365821952 .644 .153 .514 .192 .100 .091 .035 .00  .035 .031 7.47 4.27 333778944 1 .484 .046 .388 .159 .014 .002 .00  .00  .008 .027 1
minepump_spec3_product12_false-unreach-call.cil.c 8.55 4.77 349843456 1 .738 .008 15.4  8.11 421949440 1 .584 .020 .006 8.43 4.74 364736512 .663 .166 .548 .184 .110 .103 .030 .002 .032 .039 8.38 4.70 340058112 1 .263 .043 .802 .171 .005 .001 .00  .00  .011 .034 1
minepump_spec3_product13_false-unreach-call.cil.c 8.70 4.86 343842816 1 .834 .008 17.7  9.40 494448640 1 .908 .040 1.35  8.61 4.80 373133312 .642 .236 .593 .144 .175 .157 .087 .00  .087 .056 8.55 4.84 331755520 1 .305 .070 .995 .206 .006 .001 .00  .00  .009 .027 1
minepump_spec3_product14_false-unreach-call.cil.c 8.13 4.60 337100800 1 .689 .009 18.1  9.55 494260224 1 .758 .040 1.54  8.84 4.99 373764096 .687 .239 .630 .180 .172 .149 .054 .002 .056 .056 7.71 4.35 333783040 1 .265 .047 .755 .219 .006 .001 .00  .00  .006 .027 1
minepump_spec3_product15_false-unreach-call.cil.c 8.38 4.70 347385856 1 .660 .010 17.4  9.15 469880832 1 .707 .104 .012 8.99 5.09 363335680 .640 .199 .609 .146 .126 .120 .060 .002 .062 .037 8.42 4.74 339877888 1 .262 .077 .921 .191 .009 .002 .00  .00  .006 .029 1
minepump_spec3_product16_false-unreach-call.cil.c 8.14 4.62 342675456 1 .698 .013 19.3  10.2  511406080 1 .980 .114 .004 8.93 5.07 370274304 .615 .210 .666 .200 .148 .137 .051 .00  .051 .042 8.43 4.75 337145856 1 .258 .050 1.00  .201 .008 .001 .00  .00  .010 .022 1
minepump_spec3_product17_false-unreach-call.cil.c 8.86 4.96 345550848 1 .794 .008 16.9  8.96 429142016 1 .639 .010 1.32  8.79 4.93 377737216 .843 .208 .610 .180 .134 .127 .066 .00  .066 .040 8.60 4.81 342663168 1 .299 .065 .957 .705 .009 .001 .00  .00  .011 .022 1
minepump_spec3_product18_false-unreach-call.cil.c 8.44 4.76 341327872 1 .737 .009 15.7  8.35 436195328 1 .737 .011 1.13  8.40 4.71 371609600 .586 .197 .582 .149 .137 .130 .058 .00  .058 .045 8.10 4.59 343691264 1 .267 .106 .910 .190 .010 .001 .00  .00  .012 .031 1
minepump_spec3_product19_false-unreach-call.cil.c 8.65 4.86 343998464 1 .705 .012 19.3  10.1  518688768 1 .859 .021 1.64  8.46 4.81 377040896 .603 .216 .638 .204 .149 .138 .062 .00  .062 .041 8.75 4.89 341086208 1 .309 .087 .980 .219 .013 .001 .00  .00  .013 .023 1
minepump_spec3_product20_false-unreach-call.cil.c 8.55 4.82 345579520 1 .721 .012 19.5  10.3  501559296 1 .965 .079 .004 8.25 4.68 374272000 .540 .194 .645 .225 .141 .131 .062 .001 .063 .041 8.36 4.76 335437824 1 .715 .081 .538 .215 .009 .001 .00  .00  .006 .022 1
minepump_spec3_product21_false-unreach-call.cil.c 8.08 4.51 346382336 1 .589 .010 19.0  9.97 468406272 1 .847 .079 1.46  9.70 5.44 385732608 .771 .298 .881 .245 .199 .188 .099 .001 .100 .049 8.82 4.96 344109056 1 .279 .093 1.17  .748 .017 .002 .00  .00  .006 .033 1
minepump_spec3_product22_false-unreach-call.cil.c 8.77 4.91 345690112 1 .709 .017 19.4  10.1  489570304 1 .800 .026 1.52  9.07 5.11 380411904 .739 .230 .746 .220 .163 .155 .079 .00  .079 .045 8.85 5.03 343552000 1 .276 .527 1.10  .265 .019 .001 .00  .00  .006 .032 1
minepump_spec3_product23_false-unreach-call.cil.c 8.84 4.89 346255360 1 .784 .009 21.8  11.4  526172160 1 1.09  .041 1.91  8.78 5.00 380293120 .568 .255 .812 .232 .190 .158 .085 .00  .085 .049 8.47 4.76 345993216 1 .616 .078 .637 .268 .014 .001 .00  .00  .005 .031 1
minepump_spec3_product24_false-unreach-call.cil.c 9.12 5.10 349876224 1 .837 .016 15.0  7.82 399253504 1 .977 .048 1.02  8.81 4.99 373694464 .672 .254 .762 .222 .174 .162 .082 .002 .084 .047 9.17 5.17 345014272 1 .815 .108 .650 .281 .006 .001 .00  .00  .006 .025 1
minepump_spec3_product25_false-unreach-call.cil.c 8.79 4.87 346308608 1 .820 .007 17.5  9.24 469716992 1 .733 .105 1.27  8.96 5.04 377188352 .800 .222 .621 .175 .154 .148 .053 .001 .054 .036 8.44 4.76 340000768 1 .264 .071 .952 .181 .006 .001 .00  .00  .007 .036 1
minepump_spec3_product26_false-unreach-call.cil.c 8.30 4.68 341864448 1 .672 .006 16.9  9.01 447242240 1 .649 .010 .003 8.94 5.03 373682176 .617 .214 .630 .194 .153 .148 .069 .002 .071 .044 8.34 4.74 343310336 1 .269 .060 .938 .218 .012 .001 .00  .00  .012 .022 1
minepump_spec3_product27_false-unreach-call.cil.c 8.16 4.58 346140672 1 .727 .007 17.0  8.95 446636032 1 .653 .012 .013 8.64 4.94 365625344 .608 .230 .637 .162 .140 .119 .057 .001 .058 .036 8.46 4.80 342106112 1 .292 .075 .906 .592 .008 .001 .00  .00  .012 .026 1
minepump_spec3_product28_false-unreach-call.cil.c 8.33 4.64 353726464 1 .635 .016 16.5  8.61 395603968 1 .715 .028 1.19  8.63 4.89 369618944 .673 .246 .659 .195 .182 .172 .080 .002 .082 .062 8.64 4.88 340717568 1 .726 .071 .517 .213 .009 .001 .00  .00  .462 .034 1
minepump_spec3_product29_false-unreach-call.cil.c 8.37 4.70 351051776 1 .545 .008 20.0  10.4  506298368 1 .980 .267 1.54  9.50 5.31 379166720 .704 .250 .820 .252 .174 .162 .073 .001 .074 .044 8.86 4.98 342876160 1 .296 .505 1.14  .286 .007 .001 .00  .00  .006 .029 1
minepump_spec3_product30_false-unreach-call.cil.c 8.54 4.79 346173440 1 .787 .008 19.2  10.1  518393856 1 1.06  .041 1.46  8.92 5.07 374788096 .646 .266 .752 .223 .176 .160 .089 .00  .089 .049 9.05 5.08 341221376 1 .735 .070 .666 .288 .012 .002 .00  .00  .007 .026 1
minepump_spec3_product31_false-unreach-call.cil.c 8.57 4.83 346456064 1 .717 .010 19.7  10.3  484200448 1 1.16  .024 1.52  9.43 5.33 379379712 .705 .268 .875 .265 .197 .191 .108 .001 .109 .044 8.80 4.94 346411008 1 .707 .083 .647 .249 .020 .003 .00  .00  .005 .035 1
minepump_spec3_product32_false-unreach-call.cil.c 8.78 4.92 347693056 1 .796 .009 17.9  9.42 490405888 1 .741 .052 .005 9.91 5.57 384032768 .766 .272 .848 .258 .182 .173 .091 .002 .093 .063 8.91 4.96 344215552 1 .733 .116 .730 .263 .011 .00  .00  .00  .007 .029 1
minepump_spec3_product35_false-unreach-call.cil.c 8.87 4.98 349995008 1 .818 .020 16.0  8.46 409272320 1 .602 .072 1.08  9.16 5.24 376324096 .692 .305 .763 .203 .226 .213 .096 .009 .105 .087 8.43 4.72 336261120 1 .278 .049 .901 .629 .008 .001 .00  .00  .008 .029 1
minepump_spec3_product36_false-unreach-call.cil.c 8.63 4.88 349569024 1 .635 .013 19.3  10.2  479141888 1 .854 .094 .016 9.00 5.09 376283136 .593 .286 .754 .214 .219 .208 .111 .011 .122 .073 9.01 5.05 343322624 1 .763 .081 .562 .219 .009 .001 .00  .00  .477 .036 1
minepump_spec3_product39_false-unreach-call.cil.c 8.89 4.95 355106816 1 .807 .012 18.7  9.77 430440448 1 .978 .150 1.30  9.91 5.53 384831488 .842 .404 1.00  .259 .286 .275 .163 .012 .175 .078 8.87 4.99 348766208 1 .303 .464 1.11  .311 .009 .002 .00  .00  .016 .045 1
minepump_spec3_product40_false-unreach-call.cil.c 8.45 4.74 354152448 1 .692 .018 25.1  13.0  537047040 1 1.72  .953 1.95  9.95 5.54 380502016 .684 .403 1.09  .275 .291 .278 .149 .020 .169 .099 9.15 5.15 345526272 1 .322 .092 1.17  .769 .017 .001 .00  .00  .013 .035 1
minepump_spec3_product43_false-unreach-call.cil.c 8.83 4.93 345788416 1 .774 .020 20.7  10.8  520548352 1 .935 .086 1.59  8.95 5.10 377204736 .657 .326 .856 .242 .239 .229 .128 .013 .141 .079 8.87 5.02 343502848 1 .691 .080 .544 .201 .012 .002 .00  .00  .374 .029 1
minepump_spec3_product44_false-unreach-call.cil.c 9.11 5.06 351698944 1 .890 .014 23.3  12.1  562802688 1 1.25  .627 2.03  9.16 5.10 386478080 .699 .352 .833 .196 .281 .271 .149 .018 .167 .091 8.84 4.99 346116096 1 .293 .496 1.06  .238 .437 .00  .00  .00  .007 .030 1
minepump_spec3_product47_false-unreach-call.cil.c 8.70 4.87 355926016 1 .873 .023 24.3  12.7  560128000 1 1.10  .378 2.02  10.8  6.06 397955072 .826 .539 1.36  .356 .429 .414 .269 .022 .291 .150 9.22 5.21 349655040 1 .345 .092 1.26  .342 .014 .003 .00  .00  .010 .034 1
minepump_spec3_product48_false-unreach-call.cil.c 8.92 5.00 344625152 1 .805 .023 23.0  12.0  537276416 1 1.36  .142 .005 9.67 5.53 386269184 .719 .460 1.17  .320 .306 .295 .157 .018 .175 .090 9.22 5.21 349319168 1 .332 .101 1.29  .384 .017 .003 .00  .00  .013 .037 1
minepump_spec3_product51_false-unreach-call.cil.c 8.47 4.76 351326208 1 .771 .013 24.4  12.7  543920128 1 1.34  .615 .011 10.4  5.82 380755968 .838 .302 1.00  .316 .200 .191 .104 .002 .106 .049 9.22 5.22 362717184 1 .372 .116 1.15  .728 .017 .002