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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_product01_true-unreach-call.cil.c 906    892    5112897536 206 4.87  .022 878     10.5  5.64 364756992 1 .669 .00  .005 .089 8.01 4.46 332681216 .432 .147 .496 .138 .111 .104 .032 .001 .033 .038 7.67 4.26 303235072 2 .093 .062 .815 .177 .004 .002 .00  .00  .002 .450 2
minepump_spec1_product02_true-unreach-call.cil.c 905    887    3503267840 173 4.68  .015 874     10.6  5.67 355479552 1 .555 .00  .005 .071 8.00 4.44 330285056 .509 .145 .480 .173 .092 .085 .035 .002 .037 .036 7.57 4.22 300810240 2 .093 .053 .390 .178 .007 .001 .00  .00  .003 .025 2
minepump_spec1_product03_true-unreach-call.cil.c 905    889    3665260544 184 4.74  .010 876     11.4  6.14 362536960 1 .695 .00  .008 .082 7.99 4.45 332062720 .473 .168 .549 .172 .101 .093 .035 .003 .038 .034 8.06 4.48 306511872 2 .101 .069 .410 .164 .012 .003 .00  .00  .003 .038 2
minepump_spec1_product04_true-unreach-call.cil.c 905    892    3320442880 169 4.75  .012 878     10.8  5.79 389267456 1 .663 .001 .005 .374 7.57 4.25 338796544 .413 .167 .523 .157 .110 .101 .042 .002 .044 .038 8.11 4.51 309809152 2 .095 .058 .380 .141 .009 .001 .00  .00  .002 .030 2
minepump_spec1_product05_true-unreach-call.cil.c 906    892    5105774592 201 4.87  .010 877     10.9  5.85 333643776 1 .475 .00  .004 .106 8.81 4.93 357322752 .492 .478 1.04  .229 .378 .368 .210 .010 .220 .160 8.60 4.77 312549376 4 .280 .072 1.15  .748 .011 .002 .00  .00  .015 .103 2
minepump_spec1_product06_true-unreach-call.cil.c 905    891    3511189504 179 4.66  .014 878     10.9  5.84 351379456 1 .559 .00  .005 .024 8.76 4.94 350150656 .470 .425 .962 .260 .340 .322 .174 .013 .187 .123 8.81 4.92 312340480 5 .740 .071 .712 .258 .012 .002 .00  .00  .020 .130 3
minepump_spec1_product07_true-unreach-call.cil.c 912    898    5123010560 184 4.95  .018 884     11.7  6.28 391536640 1 .785 .00  .006 .036 9.20 5.06 354828288 .548 .488 1.06  .226 .407 .381 .238 .012 .250 .142 8.66 4.87 318222336 4 .248 .093 1.13  .619 .013 .002 .00  .00  .019 .119 2
minepump_spec1_product08_true-unreach-call.cil.c 906    891    5129388032 185 5.01  .015 877     13.6  7.24 427380736 1 .558 .017 .009 .028 9.50 5.31 353869824 .563 .587 1.14  .199 .474 .456 .253 .023 .276 .201 8.27 4.65 316833792 4 .637 .076 .665 .255 .025 .001 .00  .00  .019 .106 2
minepump_spec1_product09_true-unreach-call.cil.c 906    888    5167390720 203 4.88  .012 874     10.1  5.43 342548480 1 .467 .00  .007 .037 7.82 4.36 334012416 .449 .161 .512 .146 .107 .095 .031 .002 .033 .039 7.23 4.09 297619456 2 .107 .395 .730 .177 .011 .001 .00  .00  .004 .027 2
minepump_spec1_product10_true-unreach-call.cil.c 905    891    3484340224 176 4.62  .012 878     10.2  5.49 353697792 1 .569 .005 8.00 4.51 338628608 .457 .165 .539 .166 .113 .102 .037 .001 .038 .041 7.76 4.32 301113344 2 .098 .046 .399 .168 .006 .003 .00  .00  .004 .024 2
minepump_spec1_product11_true-unreach-call.cil.c 905    891    3713310720 188 4.70  .009 877     12.0  6.37 376782848 1 .420 .001 .004 .030 1.17 .176 7.79 4.36 337117184 .437 .176 .497 .139 .108 .102 .051 .00  .051 .049 7.97 4.43 302362624 2 .105 .067 .418 .177 .009 .002 .00  .00  .003 .027 2
minepump_spec1_product12_true-unreach-call.cil.c 904    887    3343417344 165 4.52  .010 874     11.3  6.07 399921152 1 .744 .00  .020 .066 7.74 4.38 328744960 .557 .160 .509 .123 .107 .082 .036 .002 .038 .033 8.16 4.52 307003392 2 .093 .051 .954 .689 .007 .001 .00  .00  .003 .035 2
minepump_spec1_product13_true-unreach-call.cil.c 906    892    5091307520 205 5.02  .014 877     10.7  5.80 349556736 1 .765 .00  .005 .060 9.22 5.10 346091520 .594 .443 1.03  .228 .337 .327 .171 .010 .181 .133 8.44 4.74 317841408 4 .238 .096 1.17  .279 .017 .001 .00  .00  .017 .542 2
minepump_spec1_product14_true-unreach-call.cil.c 905    891    3534557184 179 4.74  .010 878     11.4  6.11 356323328 1 .643 .00  .005 .054 8.85 4.94 352591872 .522 .479 .978 .202 .363 .333 .206 .009 .215 .123 8.39 4.69 311517184 5 .281 .076 1.08  .624 .016 .001 .00  .00  .021 .121 3
minepump_spec1_product15_true-unreach-call.cil.c 905    891    3722657792 183 5.21  .014 878     12.2  6.54 377044992 1 .576 .001 .004 .048 9.17 5.10 344399872 .541 .521 1.13  .251 .406 .395 .222 .009 .231 .139 8.77 4.87 316309504 4 .231 .082 1.13  .253 .013 .003 .00  .00  .018 .125 2
minepump_spec1_product16_true-unreach-call.cil.c 905    891    3644280832 179 4.99  .012 876     11.3  6.09 390365184 1 .564 .00  .014 .027 9.41 5.22 352260096 .620 .545 1.09  .206 .467 .453 .263 .025 .288 .179 8.75 4.89 319905792 4 .273 .093 1.22  .243 .014 .001 .00  .00  .017 .105 2
minepump_spec1_product17_true-unreach-call.cil.c 906    892    5103149056 205 4.55  .007 879     10.3  5.52 362147840 1 .672 .001 .005 .054 9.80 5.55 363286528 .560 .537 1.20  .243 .435 .396 .217 .010 .227 .138 8.55 4.80 306495488 5 .262 .111 1.19  .658 .017 .002 .00  .00  .021 .131 3
minepump_spec1_product18_true-unreach-call.cil.c 905    892    3413180416 174 4.50  .013 877     11.0  5.90 354951168 1 .543 .00  .004 .024 8.92 5.04 358985728 .604 .461 1.09  .256 .372 .329 .185 .010 .195 .124 8.55 4.83 324677632 4 .257 .078 1.23  .724 .014 .009 .00  .00  .023 .100 2
minepump_spec1_product19_true-unreach-call.cil.c 906    891    3679371264 181 5.00  .012 877     11.0  5.93 355487744 1 .873 .00  .006 .087 9.38 5.29 355475456 .584 .563 1.22  .282 .480 .459 .226 .020 .246 .165 8.57 4.83 323743744 4 .272 .128 1.17  .649 .018 .001 .00  .00  .015 .097 2
minepump_spec1_product20_true-unreach-call.cil.c 905    890    3725897728 182 5.08  .015 877     11.4  6.13 373559296 1 .951 .004 .006 .090 9.80 5.51 348467200 .722 .510 1.21  .274 .426 .407 .252 .008 .260 .155 8.46 4.74 312504320 4 .256 .079 1.23  .762 .008 .001 .00  .00  .014 .110 2
minepump_spec1_product21_true-unreach-call.cil.c 906    891    5093601280 201 5.41  .015 875     11.9  6.36 364937216 1 .598 .00  .013 .064 10.4  5.73 370241536 .628 .706 1.57  .341 .608 .580 .315 .031 .346 .243 9.08 5.08 323710976 4 .332 .103 1.35  .775 .014 .002 .00  .00  .024 .146 2
minepump_spec1_product22_true-unreach-call.cil.c 906    891    3461492736 176 5.10  .010 876     11.7  6.21 375422976 1 .947 .00  .007 .072 10.4  5.79 380112896 .615 .629 1.50  .329 .490 .452 .248 .020 .268 .178 9.06 5.15 324161536 4 .294 .108 1.47  .825 .012 .00  .00  .00  .023 .124 2
minepump_spec1_product23_true-unreach-call.cil.c 913    896    5174284288 12.0  6.42 375341056 1 1.16  .00  .003 .136 10.2  5.66 370233344 .677 .717 1.55  .331 .588 .539 .291 .043 .334 .221 9.26 5.23 323907584 4 .369 .123 1.37  .344 .022 .002 .00  .00  .018 .153 2
minepump_spec1_product24_true-unreach-call.cil.c 905    888    3798216704 179 5.25  .012 873     14.2  7.46 402096128 1 1.06  .010 .007 .085 10.3  5.73 378712064 .613 .756 1.61  .319 .617 .593 .351 .058 .409 .271 8.86 5.00 323817472 4 .349 .106 1.30  .306 .015 .002 .00  .00  .019 .134 2
minepump_spec1_product25_true-unreach-call.cil.c 906    892    5104164864 203 5.00  .015 877     10.8  5.80 359333888 1 .608 .00  .006 .026 8.75 4.91 359346176 .539 .473 1.10  .207 .385 .370 .212 .011 .223 .129 8.48 4.79 312225792 5 .271 .083 1.17  .644 .005 .001 .00  .00  .024 .132 3
minepump_spec1_product26_true-unreach-call.cil.c 905    888    3489587200 175 4.51  .009 875     11.6  6.16 358416384 1 .677 .00  .019 .033 8.98 5.03 351297536 .556 .460 1.09  .236 .365 .350 .182 .011 .193 .132 8.84 4.94 318922752 4 .283 .105 1.21  .692 .037 .002 .00  .00  .026 .114 2
minepump_spec1_product27_true-unreach-call.cil.c 906    891    3700584448 183 5.08  .015 877     11.7  6.24 368046080 1 .749 .00  .005 .032 9.78 5.51 355368960 .593 .549 1.27  .260 .465 .449 .210 .027 .237 .157 8.56 4.81 317816832 4 .265 .097 1.24  .276 .009 .002 .00  .00  .014 .117 2
minepump_spec1_product28_true-unreach-call.cil.c 905    888    3694981120 179 5.10  .014 874     12.2  6.53 392376320 1 .799 .00  .019 .106 9.49 5.32 353349632 .652 .562 1.22  .303 .476 .459 .270 .010 .280 .164 8.48 4.73 325001216 4 .719 .076 .728 .239 .014 .002 .00  .00  .015 .102 2
minepump_spec1_product29_true-unreach-call.cil.c 906    890    5107724288 200 5.28  .009 875     10.7  5.76 372510720 1 .794 .010 10.3  5.73 371933184 .759 .632 1.47  .322 .471 .451 .269 .017 .286 .183 9.10 5.12 334454784 4 .312 .122 1.34  .317 .019 .001 .00  .00  .026 .131 2
minepump_spec1_product30_true-unreach-call.cil.c 905    891    3573141504 181 4.99  .014 878     11.4  6.12 386207744 1 .677 .00  .005 .019 10.3  5.68 371347456 .688 .629 1.50  .276 .518 .482 .282 .015 .297 .185 9.17 5.17 330182656 4 .350 .096 1.30  .746 .015 .001 .00  .00  .022 .120 2
minepump_spec1_product31_true-unreach-call.cil.c 905    887    3792195584 178 5.14  .016 873     13.3  7.04 397918208 1 .865 .00  .006 .027 10.5  5.80 374108160 .761 .727 1.62  .338 .632 .605 .373 .048 .421 .295 8.99 5.03 325353472 4 .335 .095 1.33  .748 .018 .001 .00  .00  .017 .117 2
minepump_spec1_product32_true-unreach-call.cil.c 906    891    5111054336 183 5.21  .011 877     13.7  7.34 415793152 1 1.55  .001 .015 .266 10.0  5.55 365989888 .545 .716 1.60  .326 .611 .589 .364 .033 .397 .250 8.88 4.96 328716288 4 .749 .125 .982 .349 .015 .001 .00  .00  .015 .128 2
minepump_spec1_product45_true-unreach-call.cil.c 905    892    3455229952 76 5.35  48.7   815     30.9  15.9  674541568 1 1.61  .089 2.60  .412 6.67 1.09  11.7  6.46 375975936 .634 .996 2.26  .505 .855 .825 .557 .030 .587 .368 9.43 5.29 330203136 4 .365 .125 1.72  .431 .010 .001 .00  .00  .023 .159 2
minepump_spec1_product46_true-unreach-call.cil.c 905    890    3440361472 74 5.29  60.4   802     28.5  14.7  678203392 1 1.06  .135 .006 .524 6.99 .565 11.4  6.25 378785792 .634 .952 2.20  .508 .813 .782 .509 .032 .541 .327 9.85 5.51 330391552 4 .419 .098 1.57  .843 .012 .001 .00  .00  .024 .164 2
minepump_spec1_product47_true-unreach-call.cil.c 905    891    3810021376 77 5.51  418     441     33.8  17.4  775774208 2 1.71  .357 .021 .501 7.55 1.55  11.2  6.29 375525376 .752 .998 2.12  .408 .852 .819 .527 .062 .589 .330 9.77 5.43 330960896 4 .453 .124 1.60  .424 .017 .001 .00  .00  .019 .177 2
minepump_spec1_product48_true-unreach-call.cil.c 907    892    3456421888 71 5.05  250     613     35.7  18.3  796925952 2 1.94  .645 .014 .607 7.67 1.74  12.6  6.95 386940928 .821 1.46  2.70  .436 1.30  1.28  .825 .079 .904 .483 9.65 5.41 343326720 4 .424 .119 1.47  .434 .026 .003 .00  .00  .014 .150 2
minepump_spec1_product57_true-unreach-call.cil.c 905    891    2951618560 62 4.58  491     378     169    85.0  2827866112 12 2.40  7.84  .016 6.38  25.1  36.2   12.5  6.87 377032704 .773 1.36  2.66  .471 1.18  1.13  .721 .093 .814 .479 10.7  6.09 340971520 7 .736 .106 1.88  .840 .011 .002 .00  .00  .079 .392 2
minepump_spec1_product58_true-unreach-call.cil.c 904    891    2931511296 60 4.77  477     392     188    94.5  3387600896 13 2.74  8.99  .012 7.99  26.3  41.2   13.2  7.19 402939904 .433 1.62  3.31  .790 1.44  1.40  .960 .116 1.08  .598 9.46 5.31 335990784 4 .477 .476 1.49  .366 .010 .001 .00  .00  .039 .175 2
minepump_spec1_product59_true-unreach-call.cil.c 906    892    2977214464 61 5.00  598     270     177    89.0  2989899776 12 2.93  10.3   .004 7.86  26.5  34.1   13.3  7.39 402780160 .367 1.58  3.46  .952 1.42  1.37  .869 .148 1.02  .554 9.68 5.42 333959168 4 .435 .543 1.68  .446 .023 .001 .00  .00  .018 .165 2
minepump_spec1_product60_true-unreach-call.cil.c 905    892    2988572672 59 4.81  540     330     235    118    3683729408 14 3.14  15.4   .011 10.1   30.6  51.5   13.7  7.54 399925248 .926 1.55  2.96  .534 1.37  1.35  .825 .153 .978 .591 10.0  5.60 335417344 4 .388 .138 1.68  .420 .020 .002 .00  .00  .022 .185 2
minepump_spec1_product61_true-unreach-call.cil.c 905    890    3431387136 66 6.54  47.9   812     34.5  17.7  815099904 1 1.20  .576 .006 .474 8.72 .244 14.2  7.67 419688448 .311 1.42  3.76  1.09  1.18  1.12  .745 .047 .792 .448 10.5  5.97 342216704 4 .460 .140 2.12  .602 .015 .002 .00  .00  .021 .203 2
minepump_spec1_product62_true-unreach-call.cil.c 905    891    3441168384 66 6.18  58.4   804     38.2  19.6  839475200 1 2.37  .127 3.36  .202 8.03 1.10  16.0  8.65 428744704 .379 1.98  4.37  1.03  1.39  1.31  .847 .089 .936 .514 10.7  5.95 348434432 4 .559 .121 2.04  1.07  .020 .005 .00  .00  .020 .234 2
minepump_spec1_product63_true-unreach-call.cil.c 907    892    3650912256 67 6.24  380     480     37.6  19.2  842309632 2 1.92  .688 .008 .381 8.40 1.33  17.7  9.48 434585600 .524 2.28  5.35  .900 2.00  1.92  1.27  .141 1.41  .775 10.5  5.91 350941184 4 .929 .158 1.73  .683 .021 .001 .00  .00  .016 .196 2
minepump_spec1_product64_true-unreach-call.cil.c 905    890    3270782976 60 5.97  202     660     39.1  20.0  886022144 2 2.01  .756 .008 .756 8.38 1.59  16.5  8.85 451596288 .540 1.84  4.41  1.12  1.59  1.54  1.00  .134 1.14  .710 10.8  6.03 345120768 4 .491 .200 2.17  .579 .043 .002 .00  .00  .016 .212 2
minepump_spec2_product01_true-unreach-call.cil.c 906    891    5106475008 196 4.95  .010 878     10.1  5.43 369348608 1 .631 .001 .004 .046 7.79 4.34 340844544 .466 .170 .511 .141 .118 .113 .046 .003 .049 .059 8.01 4.40 305930240 2 .080 .644 .980 .148 .621 .611 .563 .007 .575 .036 2 .575
minepump_spec2_product02_true-unreach-call.cil.c 904    889    3491184640 173 4.31  .012 877     10.2  5.52 368132096 1 .763 .00  .018 .070 7.98 4.47 336191488 .624 .198 .518 .138 .137 .130 .043 .004 .047 .058 7.88 4.34 305664000 2 .085 .504 .872 .175 .463 .461 .413 .005 .422 .040 2 .422
minepump_spec2_product03_true-unreach-call.cil.c 905    891    3712765952 186 4.84  .013 877     11.2  6.00 375840768 1 .505 .00  .005 .062 8.29 4.59 333688832 .487 .181 .561 .184 .131 .124 .049 .004 .053 .069 7.80 4.34 302714880 2 .082 .150 .928 .599 .103 .096 .035 .007 .046 .028 2 .049
minepump_spec2_product04_true-unreach-call.cil.c 904    890    3354267648 168 4.62  .007 877     14.0  7.42 433872896 1 .576 .00  .006 .042 7.64 4.29 342581248 .468 .154 .515 .163 .117 .112 .043 .001 .044 .058 7.66 4.27 309080064 2 .080 .493 .868 .183 .440 .433 .050 .005 .058 .037 2 .063
minepump_spec2_product05_true-unreach-call.cil.c 906    889    5158408192 201 5.08  .010 874     10.7  5.69 332554240 1 .761 .00  .005 .042 10.3  5.76 361181184 .652 .659 1.46  .287 .564 .538 .307 .030 .337 .361 9.89 5.53 321171456 7 .285 .933 1.69  .269 .327 .317 .182 .017 .242 .200 3 .204
minepump_spec2_product06_true-unreach-call.cil.c 905    888    3562553344 175 4.81  .012 874     10.8  5.81 347435008 1 .797 .001 .013 .075 10.2  5.63 360325120 .576 .778 1.53  .281 .662 .632 .346 .035 .381 .408 9.84 5.59 326041600 7 .368 .865 1.79  .298 .788 .358 .222 .018 .282 .249 2 .248
minepump_spec2_product07_true-unreach-call.cil.c 906    890    3766177792 181 5.01  .006 876     11.9  6.38 379076608 1 .968 .00  .009 .070 9.58 5.32 361746432 .540 .647 1.39  .291 .563 .530 .244 .048 .292 .324 9.39 5.32 327012352 8 .372 .876 1.72  .328 .307 .290 .185 .012 .240 .206 2 .200
minepump_spec2_product08_true-unreach-call.cil.c 905    887    3720978432 177 5.19  .010 873     14.5  7.80 461119488 1 .711 .00  .016 .143 9.94 5.55 363147264 .556 .735 1.47  .290 .633 .611 .329 .060 .389 .416 9.80 5.55 326893568 10 .404 .849 1.75  .325 .768 .754 .619 .023 .699 .284 3 .651
minepump_spec2_product09_true-unreach-call.cil.c 905    889    5143724032 202 4.98  .014 872     10.7  5.78 363954176 1 .688 .00  .005 .029 7.76 4.29 335724544 .415 .179 .481 .142 .144 .132 .041 .004 .045 .064 8.00 4.43 308170752 2 .071 .168 .966 .196 .112 .107 .041 .004 .049 .033 2 .053
minepump_spec2_product10_true-unreach-call.cil.c 905    891    3460313088 174 4.37  .017 878     10.8  5.73 351141888 1 .614 .00  .005 .090 7.86 4.40 337932288 .434 .181 .524 .134 .138 .129 .056 .003 .059 .076 7.86 4.38 311660544 2 .075 .529 .899 .191 .470 .465 .409 .004 .417 .032 2 .420
minepump_spec2_product11_true-unreach-call.cil.c 906    891    3637329920 183 5.04  .010 878     11.5  6.08 368017408 1 .600 .00  .005 .061 7.20 3.98 337010688 .445 .169 .481 .149 .137 .127 .061 .003 .064 .080 8.06 4.47 306184192 2 .082 .504 .885 .160 .465 .447 .035 .005 .044 .046 2 .043
minepump_spec2_product12_true-unreach-call.cil.c 904    886    3304529920 162 4.58  .007 873     11.1  5.99 394604544 1 .900 .00  .013 .082 8.14 4.53 338833408 .486 .201 .528 .149 .150 .147 .043 .002 .045 .063 7.80 4.38 305033216 2 .074 .139 .939 .166 .106 .099 .048 .004 .055 .027 2 .056
minepump_spec2_product13_true-unreach-call.cil.c 906    888    5177974784 208 5.30  .009 873     10.3  5.53 363864064 1 .862 .006 10.4  5.74 362749952 .692 .747 1.46  .266 .634 .612 .328 .029 .357 .393 9.25 5.25 306872320 7 .303 .368 1.59  .265 .291 .276 .174 .016 .222 .176 3 .195
minepump_spec2_product14_true-unreach-call.cil.c 905    891    3424022528 172 4.61  .013 878     10.9  5.84 380821504 1 .633 .00  .006 .038 10.2  5.65 359960576 .565 .872 1.57  .266 .734 .718 .362 .046 .408 .463 9.64 5.48 331673600 7 .338 .419 1.78  .787 .352 .343 .214 .018 .270 .244 2 .241
minepump_spec2_product15_true-unreach-call.cil.c 905    891    5106991104 183 5.93  .015 876     12.7  6.70 393392128 1 .596 .00  .005 .026 9.92 5.49 356708352 .539 .681 1.47  .300 .595 .574 .275 .059 .334 .362 9.25 5.27 323792896 8 .692 .402 1.27  .312 .334 .322 .188 .020 .254 .222 2 .217
minepump_spec2_product16_true-unreach-call.cil.c 905    889    5170900992 182 5.11  .009 876     11.8  6.25 410943488 1 .595 .00  .013 .027 10.9  6.04 368898048 .677 .779 1.58  .326 .680 .655 .359 .061 .420 .450 9.53 5.45 330334208 10 .391 .445 1.75  .718 .368 .361 .209 .021 .291 .279 3 .243
minepump_spec2_product17_true-unreach-call.cil.c 906    890    5156581376 198 5.06  .015 875     10.5  5.61 361078784 1 .724 .00  .005 .104 10.4  5.77 372682752 .596 .734 1.53  .301 .600 .575 .301 .032 .333 .385 8.78 5.05 327360512 7 .276 .485 1.50  .552 .403 .390 .251 .024 .304 .190 3 .281
minepump_spec2_product18_true-unreach-call.cil.c 905    890    3405955072 171 4.51  .015 877     11.2  6.00 349298688 1 .774 .00  .003 .069 10.3  5.75 357732352 .742 .677 1.49  .307 .590 .571 .323 .031 .354 .384 10.1  5.78 339927040 7 .434 .534 1.87  .755 .455 .434 .264 .021 .325 .260 2 .291
minepump_spec2_product19_true-unreach-call.cil.c 905    891    5117419520 183 5.15  .007 877     12.2  6.58 416309248 1 .530 .00  .010 .040 10.3  5.79 358051840 .622 .778 1.56  .310 .683 .651 .315 .061 .376 .404 10.7  6.06 341970944 9 .475 .692 2.35  .340 .591 .578 .378 .030 .454 .343 3 .416
minepump_spec2_product20_true-unreach-call.cil.c 905    891    3651141632 178 5.15  .011 877     12.9  6.87 401764352 1 .917 .00  .010 .092 9.00 5.01 359948288 .487 .532 1.11  .235 .449 .440 .244 .038 .282 .320 10.1  5.80 338604032 8 .574 .587 1.97  .314 .489 .480 .322 .025 .402 .297 2 .357
minepump_spec2_product21_true-unreach-call.cil.c 906    889    5159862272 200 5.41  .013 875     11.5  6.19 388702208 1 1.19  .005 12.0  6.57 393691136 .673 .952 2.30  .488 .810 .783 .453 .049 .502 .528 10.3  5.82 342548480 7 .416 .597 2.09  .772 .490 .479 .298 .036 .369 .238 3 .341
minepump_spec2_product22_true-unreach-call.cil.c 904    890    3471396864 174 4.99  .009 876     11.9  6.39 390168576 1 .702 .001 .018 .020 12.4  6.77 378912768 .629 1.17  2.53  .539 1.01  .946 .572 .069 .641 .681 10.6  6.10 342441984 7 .510 .638 2.29  .839 .532 .508 .317 .023 .374 .327 2 .346
minepump_spec2_product23_true-unreach-call.cil.c 905    888    5178843136 180 5.04  .012 874     13.1  6.96 386994176 1 .982 .00  .023 .138 11.4  6.25 376283136 .835 .998 2.20  .446 .896 .869 .448 .095 .543 .581 10.8  6.18 350236672 7 .479 1.09  2.33  .436 .998 .963 .328 .031 .397 .364 2 .363
minepump_spec2_product24_true-unreach-call.cil.c 905    892    5100822528 178 5.33  .012 877     13.7  7.25 433700864 1 .839 .001 .010 .049 12.1  6.61 378339328 .654 1.22  2.42  .414 1.03  .984 .583 .083 .666 .694 11.9  6.74 351408128 8 .591 1.16  2.61  .471 .617 .597 .396 .042 .488 .461 2 .450
minepump_spec2_product25_true-unreach-call.cil.c 906    892    5111287808 201 5.07  .014 877     11.1  5.93 374566912 1 .543 .001 .005 .034 9.69 5.36 366075904 .519 .815 1.53  .258 .681 .639 .343 .038 .381 .411 9.33 5.34 330788864 7 .281 .976 1.76  .318 .887 .872 .727 .027 .782 .207 3 .765
minepump_spec2_product26_true-unreach-call.cil.c 904    890    3476918272 174 4.65  .009 876     12.1  6.38 360960000 1 .662 .001 .005 .133 10.5  5.81 374550528 .622 .705 1.52  .288 .592 .573 .292 .034 .326 .358 10.0  5.66 329994240 7 .388 1.01  1.91  .323 .944 .935 .270 .027 .331 .279 2 .304
minepump_spec2_product27_true-unreach-call.cil.c 905    891    5102567424 185 5.20  .011 877     11.2  6.01 386252800 1 .910 .00  .005 .120 10.5  5.82 366497792 .685 .890 1.66  .285 .761 .740 .361 .061 .422 .484 10.8  6.14 344924160 9 .520 .628 2.06  .725 .541 .525 .355 .029 .432 .304 3 .397
minepump_spec2_product28_true-unreach-call.cil.c 906    892    5102956544 182 4.81  .010 878     13.2  7.04 427876352 1 .595 .00  .005 .050 9.39 5.24 351055872 .674 .511 1.20  .312 .420 .406 .223 .024 .247 .266 10.3  5.84 337154048 8 .514 .573 1.97  .303 .491 .479 .317 .027 .401 .304 2 .354
minepump_spec2_product29_true-unreach-call.cil.c 905    888    5171830784 196 5.17  .013 874     10.9  5.84 369860608 1 .669 .005 12.6  6.84 391368704 .625 1.06  2.41  .505 .918 .900 .536 .075 .611 .659 10.4  5.88 340717568 7 .420 .620 2.10  .339 .541 .523 .334 .038 .403 .253 3 .379
minepump_spec2_product30_true-unreach-call.cil.c 905    890    3416641536 172 4.92  .008 876     10.9  5.83 340209664 1 .719 .005 12.3  6.81 382623744 .711 1.22  2.48  .503 1.03  1.01  .563 .059 .622 .700 10.5  6.02 344412160 7 .500 .993 2.23  .455 .881 .866 .727 .026 .788 .294 2 .759
minepump_spec2_product31_true-unreach-call.cil.c 906    891    3685392384 177 5.18  .006 874     13.1  6.98 422047744 1 .814 .00  .006 .050 11.7  6.42 373841920 .550 1.01  2.31  .537 .890 .870 .486 .078 .564 .590 11.4  6.49 341286912 7 .544 1.12  2.39  .446 .519 .507 .344 .032 .413 .360 2 .380
minepump_spec2_product32_true-unreach-call.cil.c 905    891    3714400256 177 5.23  .028 877     14.2  7.59 449175552 1 .863 .007 .005 .189 11.1  6.21 384741376 .564 1.01  2.28  .549 .819 .794 .439 .076 .515 .557 11.7  6.67 346365952 8 .558 .689 2.66  1.02  .595 .579 .394 .039 .479 .470 2 .443
minepump_spec2_product37_true-unreach-call.cil.c 904    891    3333160960 81 5.00  52.8   811     30.5  15.7  673435648 1 1.31  .00  2.62  .170 6.21 2.09  12.5  6.80 375992320 .707 1.24  2.53  .524 1.11  1.08  .637 .152 .789 .813 10.5  5.94 341729280 7 .396 .610 2.14  .830 .513 .491 .299 .039 .366 .251 3 .349
minepump_spec2_product38_true-unreach-call.cil.c 904    888    3378577408 79 4.93  56.7   805     28.8  14.8  644308992 1 1.40  .00  2.38  .305 6.15 1.01  12.7  6.93 370417664 .748 1.32  2.58  .477 1.14  1.11  .576 .112 .688 .745 10.7  6.02 339132416 6 .457 .650 2.06  .379 .536 .512 .340 .033 .408 .194 2 .380
minepump_spec2_product39_true-unreach-call.cil.c 908    890    3669274624 84 5.18  423     437     43.6  22.4  905129984 3 2.11  .282 .005 .842 8.90 4.58  12.2  6.71 381329408 .811 1.20  2.36  .410 1.03  1.00  .550 .127 .677 .697 10.3  5.90 348037120 8 .544 .659 2.18  .395 .563 .550 .361 .036 .438 .284 2 .405
minepump_spec2_product40_true-unreach-call.cil.c 905    891    3218694144 75 5.18  231     633     47.5  24.2  929607680 3 1.99  .749 .005 1.44  11.3  3.45  11.9  6.49 381091840 .777 1.18  2.22  .380 1.02  .991 .596 .119 .715 .741 11.7  6.71 348930048 9 .646 .790 2.59  .504 .673 .640 .434 .038 .534 .399 3 .483
minepump_spec2_product45_true-unreach-call.cil.c 905    890    3306201088 72 5.22  52.2   812     36.5  18.8  811896832 1 1.72  .00  3.21  1.15  7.17 2.09  13.7  7.54 402903040 .806 1.45  3.11  .628 1.29  1.23  .724 .116 .840 .927 11.1  6.30 344760320 7 .475 .693 2.47  .466 .617 .604 .415 .055 .498 .338 3 .474
minepump_spec2_product46_true-unreach-call.cil.c 904    890    3252150272 70 5.03  48.6   815     32.3  16.6  730230784 1 1.66  .00  2.84  .458 7.39 1.25  12.8  7.14 398368768 .647 1.45  2.89  .469 1.26  1.21  .761 .140 .901 .940 11.2  6.33 350736384 6 .556 1.09  2.33  .429 .998 .971 .372 .037 .441 .306 2 .825
minepump_spec2_product47_true-unreach-call.cil.c 907    893    3630395392 75 4.69  418     445     51.3  26.3  927309824 2 1.96  .358 .006 .811 9.13 8.19  12.7  6.95 396726272 .705 1.49  2.83  .430 1.28  1.24  .755 .128 .883 .909 12.2  7.16 361148416 9 .827 .874 2.88  .887 .765 .743 .527 .050 .653 .447 3 .585
minepump_spec2_product48_true-unreach-call.cil.c 905    892    3433390080 70 5.36  283     580     51.8  26.4  937910272 3 2.24  1.25  .005 1.76  10.9  4.32  13.3  7.23 390991872 .767 1.48  2.92  .465 1.28  1.24  .659 .141 .800 .869 11.4  6.49 351203328 8 .647 1.18  2.56  .476 1.02  1.00  .397 .038 .493 .366 2 .442
minepump_spec2_product49_true-unreach-call.cil.c 905    892    2987986944 70 4.60  482     385     294    148    4420190208 18 3.04  13.2   .005 15.3   37.9  70.3   12.5  6.87 374673408 .694 1.38  2.64  .450 1.23  1.17  .724 .088 .812 .858 13.0  7.52 363151360 11 .983 .951 3.14  1.14  .834 .809 .559 .046 .680 .491 2 .614
minepump_spec2_product50_true-unreach-call.cil.c 906    891    2938494976 68 4.83  486     382     166    83.9  3087749120 13 3.04  6.19  .013 6.89  27.1  33.5   12.2  6.61 387309568 .679 1.32  2.56  .461 1.18  1.16  .683 .115 .798 .863 15.0  9.09 372252672 16 1.46  1.14  4.03  .946 .980 .954 .677 .064 .881 1.26  2 .758
minepump_spec2_product51_true-unreach-call.cil.c 904    891    2938683392 65 4.69  612     255     228    115    3559358464 15 3.00  12.1   .019 9.71  29.8  52.9   12.7  6.89 380669952 .702 1.42  2.70  .522 1.24  1.22  .719 .156 .875 .927 11.8  6.77 350023680 9 .714 .791 2.71  .454 .703 .686 .470 .034 .571 .405 3 .514
minepump_spec2_product52_true-unreach-call.cil.c 904    892    2956214272 60 4.52  503     367     233    117    3705622528 15 2.87  12.8   .008 11.3   32.1  50.5   12.8  7.04 380223488 .645 1.44  2.65  .532 1.29  1.26  .670 .176 .846 .922 11.8  6.83 351842304 8 .668 1.19  2.75  .587 1.08  1.06  .494 .040 .590 .358 2 .889
minepump_spec2_product53_true-unreach-call.cil.c 905    891    3439304704 72 5.83  51.5   810     34.8  17.9  833396736 1 1.59  .00  .016 .110 7.94 1.59  16.4  8.87 448663552 .443 1.97  4.69  .735 1.71  1.66  .978 .208 1.19  1.25  11.8  6.65 347627520 6 .559 1.17  2.69  .619 1.06  1.02  .831 .035 .892 .269 2 .874
minepump_spec2_product54_true-unreach-call.cil.c 904    891    3442237440 71 5.92  49.4   812     34.6  17.8  793952256 1 1.84  .00  2.80  .171 7.88 1.45  15.0  8.10 424935424 .437 1.64  4.08  .688 1.47  1.43  .777 .125 .902 .943 13.4  7.56 355598336 7 .744 1.33  3.29  .701 1.22  1.20  .945 .049 1.05  .496 2 1.01 
minepump_spec2_product55_true-unreach-call.cil.c 904    890    3304284160 67 5.67  324     538     46.0  23.6  888889344 2 2.12  .353 .010 1.24  10.7  2.49  15.7  8.52 462737408 .421 2.09  4.47  .685 1.87  1.80  .983 .254 1.24  1.38  12.4  6.90 359993344 6 .557 .824 2.78  .615 .614 .581 .385 .047 .463 .298 2 .437
minepump_spec2_product56_true-unreach-call.cil.c 904    891    3195736064 65 5.71  244     621     46.8  23.9  920461312 3 2.14  .561 .004 .858 11.1  2.98  15.3  8.28 432824320 .433 1.88  4.19  .948 1.66  1.58  .856 .223 1.08  1.17  12.0  6.76 363229184 6 .568 1.14  2.73  .656 1.01  .982 .447 .042 .527 .258 2 .496
minepump_spec2_product57_true-unreach-call.cil.c 905    891    2955567104 59 5.00  452     418     331    166    4577607680 18 2.83  16.5   .006 16.9   38.2  83.6   15.9  8.73 407339008 1.12  2.04  3.85  .610 1.85  1.79  1.01  .195 1.21  1.28  13.3  7.74 368205824 11 1.14  1.13  3.24  .581 .990 .965 .646 .061 .778 .534 2 .717
minepump_spec2_product58_true-unreach-call.cil.c 905    892    2950946816 59 4.90  461     409     152    76.7  2914271232 12 2.49  6.00  .005 6.66  26.3  28.3   14.5  7.92 395030528 .854 1.87  3.55  .652 1.65  1.62  1.03  .126 1.16  1.20  11.7  6.70 359030784 7 .695 .796 2.75  .555 .718 .704 .451 .039 .534 .397 2 .499
minepump_spec2_product59_true-unreach-call.cil.c 906    891    3013025792 59 5.14  570     299     164    82.8  3004932096 12 3.28  7.57  .004 8.23  26.6  30.0   16.1  8.73 432955392 .929 2.32  4.11  .656 2.09  2.03  1.06  .358 1.42  1.50  12.0  6.95 353013760 7 .663 1.24  2.79  .553 1.13  1.12  .498 .044 .597 .417 2 .932
minepump_spec2_product60_true-unreach-call.cil.c 906    892    3018571776 55 4.68  494     376     149    75.3  2732097536 11 2.75  6.53  .006 6.05  28.4  24.0   12.8  7.08 379568128 .795 1.47  2.89  .569 1.30  1.26  .742 .125 .867 .916 12.0  6.94 344604672 7 .668 1.30  2.79  .493 1.19  1.17  .466 .056 .569 .419 2 .531
minepump_spec2_product61_true-unreach-call.cil.c 905    890    3275739136 63 5.98  54.3   809     42.2  21.6  917012480 1 1.88  .001 3.76  .692 9.62 1.67  17.4  9.36 446492672 .672 1.91  5.06  1.03  1.58  1.48  .865 .148 1.01  1.06  13.6  7.56 362139648 6 .775 1.28  3.35  .690 .733 .696 .467 .049 .559 .392 2 .525
minepump_spec2_product62_true-unreach-call.cil.c 905    891    3345309696 64 5.74  46.4   816     42.1  21.6  910143488 1 2.08  .00  4.05  .202 9.49 1.97  18.4  9.85 453656576 .624 2.94  5.52  .944 2.16  2.06  1.26  .187 1.44  1.51  13.9  7.80 368975872 7 .981 1.09  3.22  .799 .904 .880 .620 .060 .729 .472 3 .692
minepump_spec2_product63_true-unreach-call.cil.c 905    891    3470020608 63 6.51  390     469     46.9  23.9  890085376 2 1.72  .322 .005 1.20  11.3  2.21  16.9  9.17 432779264 .594 2.01  4.88  .915 1.76  1.72  1.11  .182 1.29  1.36  15.5  8.78 379392000 9 1.04  1.62  4.25  .799 1.48  1.44  .718 .069 .864 .727 3 .796
minepump_spec2_product64_true-unreach-call.cil.c 904    890    3236515840 59 5.81  206     658     49.8  25.3  892903424 2 2.17  .197 .005 1.91  11.7  2.61  17.7  9.56 440827904 .565 2.53  5.30  1.17  1.99  1.94  1.18  .239 1.42  1.46  15.4  8.85 372490240 8 .952 1.32  4.34  1.30  1.13  1.11  .767 .063 .886 .624 2 .845
minepump_spec3_product33_true-unreach-call.cil.c 907    894    5384511488 114 4.74  82.4   775     21.8  11.3  566882304 1 .635 .035 1.85  .059 4.02 .965 9.37 5.20 353390592 .556 .594 1.17  .288 .492 .471 .278 .063 .341 .272 8.51 4.79 315158528 4 .307 .083 1.09  .586 .009 .003 .00  .00  .021 .116 2
minepump_spec3_product34_true-unreach-call.cil.c 907    894    5222469632 110 4.66  94.2   764     24.4  12.7  672866304 1 1.38  .146 2.29  .336 4.17 .882 8.86 4.96 354365440 .484 .458 1.06  .282 .379 .369 .203 .044 .247 .170 9.05 5.11 312332288 4 .287 .092 1.33  .789 .019 .002 .00  .00  .029 .124 2
minepump_spec3_product37_true-unreach-call.cil.c 905    892    3481702400 80 4.79  59.9   807     28.5  14.7  624021504 1 1.47  .166 2.24  .103 5.84 .970 11.9  6.57 380395520 .592 1.21  2.30  .444 1.11  1.09  .621 .206 .827 .636 9.67 5.46 339656704 4 .448 .131 1.57  .429 .017 .001 .00  .00  .044 .156 2
minepump_spec3_product38_true-unreach-call.cil.c 905    892    3293220864 75 5.02  51.3   815     26.5  13.6  619044864 1 1.16  .285 .005 .133 5.15 1.01  11.7  6.43 374476800 .551 1.09  2.21  .496 .982 .954 .519 .192 .711 .574 9.30 5.21 336809984 4 .342 .126 1.54  .860 .026 .001 .00  .00  .032 .165 2
minepump_spec3_product41_true-unreach-call.cil.c 906    889    5189541888 98 4.81  75.4   778     26.0  13.5  598880256 1 1.15  .246 2.10  .500 5.11 .990 10.5  5.81 361381888 .521 .907 1.64  .325 .816 .793 .436 .121 .557 .373 8.88 5.00 327487488 4 .332 .091 1.24  .345 .013 .00  .00  .00  .020 .139 2
minepump_spec3_product42_true-unreach-call.cil.c 906    891    5134413824 94 4.99  70.7   786     23.0  12.0  587591680 1 .702 .142 2.02  .064 4.44 1.02  9.98 5.55 360525824 .505 .935 1.70  .377 .822 .800 .465 .109 .574 .375 8.83 4.96 320503808 4 .324 .099 1.22  .646 .018 .002 .00  .00  .026 .164 2
minepump_spec3_product45_true-unreach-call.cil.c 905    891    3420004352 71 5.19  54.7   811     30.5  15.7  701358080 1 1.16  .065 2.55  .165 6.82 1.59  10.2  5.72 363061248 .553 .779 1.74  .414 .670 .648 .417 .079 .496 .285 9.78 5.46 329523200 4 .459 .139 1.60  .819 .015 .003 .00  .00  .029 .189 2
minepump_spec3_product46_true-unreach-call.cil.c 905    890    3255439360 67 5.09  55.6   810     32.4  16.8  748572672 1 1.26  .084 2.72  .484 6.78 1.72  10.3  5.77 364728320 .643 .846 1.78  .414 .714 .685 .431 .088 .519 .361 9.54 5.36 334577664 4 .445 .099 1.62  .408 .017 .001 .00  .00  .028 .194 2
minepump_spec3_product49_true-unreach-call.cil.c 905    892    3548614656 78 4.94  242     622     28.2  14.5  651935744 1 1.17  .131 2.47  .129 5.90 1.50  10.2  5.60 369561600 .676 .593 1.37  .359 .482 .466 .262 .045 .307 .241 10.8  6.13 354439168 6 .864 .150 1.83  .511 .025 .001 .00  .00  .074 .369 1
minepump_spec3_product50_true-unreach-call.cil.c 905    892    3554709504 77 5.07  247     617     29.7  15.3  717832192 1 1.29  .612 .004 .404 6.16 1.09  9.10 5.13 362258432 .509 .467 1.29  .379 .391 .360 .180 .022 .202 .140 9.83 5.56 343805952 4 .498 .167 1.60  .362 .017 .001 .00  .00  .043 .208 1
minepump_spec3_product53_true-unreach-call.cil.c 906    891    3233095680 65 5.73  324     540     37.5  19.3  800215040 1 1.97  .037 3.35  .057 8.36 1.42  12.0  6.61 374280192 .195 1.18  2.63  .677 .555 .526 .299 .040 .339 .262 12.8  7.17 358436864 6 1.01  .212 2.58  .707 .073 .005 .00  .00  .053 .486 1
minepump_spec3_product54_true-unreach-call.cil.c 906    891    3173109760 63 5.35  327     538     37.3  19.1  826155008 1 2.50  .285 3.26  .175 7.77 1.30  11.2  6.13 378531840 .609 .781 2.12  .602 .604 .585 .373 .037 .410 .324 13.1  7.25 363880448 6 1.19  .166 2.56  .681 .041 .001 .00  .00  .079 .552 1
minepump_spec3_product57_true-unreach-call.cil.c 906    892    2958458880 56 4.60  563     308     29.8  15.3  703479808 1 1.34  .065 2.50  .055 6.47 1.93  11.3  6.30 365920256 .577 .784 1.97  .454 .659 .627 .382 .079 .461 .327 19.8  13.0  374546432 25 3.62  .191 5.76  .769 .045 .005 .00  .00  .459 3.48  1
minepump_spec3_product58_true-unreach-call.cil.c 905    891    3007283200 54 4.48  583     288     30.2  15.5  715059200 1 1.26  .085 2.59  .097 6.94 1.28  10.8  5.99 375500800 .602 .813 1.86  .409 .670 .653 .415 .064 .479 .360 10.9  6.32 348749824 7 .811 .169 2.13  .492 .019 .002 .00  .00  .055 .461 2
minepump_spec3_product61_true-unreach-call.cil.c 904    891    3059204096 51 5.64  508     361     35.9  18.4  844152832 1 1.42  .274 3.00  .210 8.49 1.26  12.6  6.85 390729728 .203 1.00  3.09  1.06  .829 .806 .498 .099 .597 .433 12.7  7.24 366534656 7 1.09  .201 2.79  1.16  .035 .004 .00  .00  .057 .531 2
minepump_spec3_product62_true-unreach-call.cil.c 905    890    3065163776 52 5.35  502     366     36.8  18.9  877318144 1 1.39  .211 .005 .612 8.16 1.70  11.5  6.32 380256256 .184 .878 2.88  .985 .682 .649 .407 .076 .483 .324 14.1  7.95 371740672 6 1.23  .255 3.16  .805 .040 .002 .00  .00  .076 .537 1
minepump_spec4_product01_true-unreach-call.cil.c 906    893    5232406528 228 5.27  .012 878     9.82 5.34 356442112 1 .507 .00  .005 .058 7.96 4.42 332353536 .500 .146 .491 .144 .091 .078 .029 .001 .030 .033 8.08 4.47 297955328 2 .092 .055 .411 .165 .007 .003 .00  .00  .002 .027 2
minepump_spec4_product02_true-unreach-call.cil.c 906    893    5091274752 195 4.93  .010 879     10.0  5.39 353120256 1 .743 .005 8.06 4.51 335642624 .389 .126 .482 .149 .084 .079 .025 .001 .026 .032 7.55 4.21 303431680 2 .101 .064 .419 .150 .007 .001 .00  .00  .005 .033 2
minepump_spec4_product03_true-unreach-call.cil.c 906    891    5119328256 198 5.09  .010 877     10.3  5.52 346304512 1 .546 .00  .013 .030 8.05 4.54 335073280 .497 .147 .498 .170 .105 .096 .039 .003 .042 .039 7.50 4.18 308068352 2 .097 .056 .437 .159 .015 .001 .00  .00  .003 .030 2
minepump_spec4_product04_true-unreach-call.cil.c 906    892    5117038592 189 5.03  .009 878     9.87 5.32 359936000 1 .862 .012 7.64 4.30 333873152 .425 .164 .489 .143 .098 .090 .041 .001 .042 .039 7.77 4.33 297320448 2 .090 .064 .386 .177 .008 .001 .00  .00  .003 .029 2
minepump_spec4_product05_true-unreach-call.cil.c 906    891    5114183680 223 5.34  .011 875     10.0  5.42 356909056 1 .540 .00  .005 .029 9.34 5.25 341929984 .537 .335 .872 .231 .231 .221 .114 .011 .125 .097 8.37 4.67 316198912 4 .240 .075 1.08  .643 .022 .001 .00  .00  .025 .105 2
minepump_spec4_product06_true-unreach-call.cil.c 906    892    5099470848 200 5.06  .011 878     9.57 5.18 362233856 1 .536 .00  .004 .036 8.71 4.86 350384128 .462 .334 .863 .216 .249 .240 .126 .010 .136 .104 8.53 4.79 314925056 5 .232 .094 1.23  .265 .013 .004 .00  .00  .010 .141 3
minepump_spec4_product07_true-unreach-call.cil.c 906    892    5119406080 204 5.35  .017 876     9.98 5.37 351150080 1 .700 .00  .004 .022 8.80 4.87 343789568 .459 .346 .886 .246 .261 .247 .126 .020 .146 .109 8.70 4.82 316239872 5 .294 .065 1.16  .253 .009 .003 .00  .00  .011 .126 3
minepump_spec4_product08_true-unreach-call.cil.c 906    888    5195653120 201 5.56  .013 872     10.6  5.71 361705472 1 .491 .005 .006 .051 8.24 4.65 350117888 .474 .341 .837 .209 .271 .261 .147 .020 .167 .116 8.17 4.52 314380288 4 .258 .097 1.07  .621 .020 .001 .00  .00  .022 .121 2
minepump_spec4_product09_true-unreach-call.cil.c 906    890    5129732096 222 5.25  .015 875     9.71 5.23 341217280 1 .716 .005 7.89 4.41 332464128 .481 .159 .522 .178 .106 .099 .040 .001 .041 .046 7.56 4.24 304205824 2 .102 .051 .387 .172 .005 .001 .00  .00  .002 .028 2
minepump_spec4_product10_true-unreach-call.cil.c 906    892    5130715136 197 4.85  .009 878     10.3  5.57 340140032 1 .566 .00  .010 .041 7.63 4.27 335458304 .333 .175 .476 .133 .109 .102 .035 .002 .037 .040 7.58 4.23 299413504 2 .094 .461 .808 .164 .006 .001 .00  .00  .003 .031 2
minepump_spec4_product11_true-unreach-call.cil.c 906    892    5103501312 199 5.20  .020 877     10.0  5.35 347951104 1 .629 .001 .008 .062 8.29 4.58 334721024 .523 .178 .500 .146 .124 .116 .055 .00  .055 .052 7.62 4.27 305176576 2 .092 .048 .366 .152 .007 .002 .00  .00  .003 .033 2
minepump_spec4_product12_true-unreach-call.cil.c 905    892    3681026048 185 5.07  .006 877     10.2  5.49 343019520 1 .638 .001 .011 .046 8.32 4.59 340140032 .490 .157 .546 .170 .114 .096 .043 .003 .046 .043 7.85 4.37 301187072 2 .105 .063 .778 .566 .005 .001 .00  .00  .003 .030 2
minepump_spec4_product13_true-unreach-call.cil.c 906    891    5113839616 223 5.34  .015 875     9.39 5.07 343339008 1 .598 .001 .004 .051 8.29 4.58 339984384 .570 .286 .729 .198 .222 .214 .116 .008 .124 .096 8.48 4.72 312823808 4 .738 .081 .679 .239 .019 .002 .00  .00  .026 .106 2
minepump_spec4_product14_true-unreach-call.cil.c 906    892    5120053248 198 5.05  .005 877     10.2  5.53 340963328 1 .573 .004 8.89 4.91 336723968 .585 .353 .810 .213 .279 .269 .150 .011 .161 .113 8.71 4.85 308482048 5 .236 .073 1.23  .226 .014 .002 .00  .00  .013 .141 3
minepump_spec4_product15_true-unreach-call.cil.c 906    888    5193592832 210 5.55  .015 869     9.95 5.36 359391232 1 .784 .017 8.21 4.56 352137216 .520 .347 .825 .220 .285 .276 .151 .017 .168 .120 8.31 4.65 315219968 5 .594 .081 .704 .240 .009 .001 .00  .00  .013 .119 3
minepump_spec4_product16_true-unreach-call.cil.c 906    892    5130743808 201 5.46  .012 877     9.79 5.28 340938752 1 .649 .014 8.50 4.72 344580096 .480 .359 .853 .225 .286 .270 .135 .017 .152 .108 8.47 4.75 324042752 4 .292 .083 1.10  .244 .022 .002 .00  .00  .023 .118 2
minepump_spec4_product17_true-unreach-call.cil.c 906    888    5235511296 225 5.40  .013 872     9.68 5.21 350441472 1 .368 .008 9.36 5.18 345214976 .469 .368 .918 .244 .289 .272 .135 .011 .146 .107 8.42 4.69 317566976 5 .288 .093 1.15  .647 .011 .001 .00  .00  .023 .158 3
minepump_spec4_product18_true-unreach-call.cil.c 906    889    5175848960 191 4.87  .017 875     10.1  5.44 361889792 1 .632 .001 .020 .023 8.87 4.94 351150080 .559 .341 .836 .224 .262 .248 .123 .008 .131 .091 8.41 4.74 318599168 4 .280 .087 1.19  .244 .010 .002 .00  .00  .022 .117 2
minepump_spec4_product19_true-unreach-call.cil.c 906    892    5098049536 202 5.38  .018 876     9.91 5.31 362385408 1 .589 .007 8.55 4.77 338046976 .534 .410 .942 .238 .332 .323 .153 .031 .184 .149 8.57 4.76 328728576 5 .243 .086 1.15  .260 .009 .001 .00  .00  .010 .130 3
minepump_spec4_product20_true-unreach-call.cil.c 906    890    5141032960 203 5.54  .014 874     10.0  5.40 351240192 1 .738 .005 8.44 4.67 350904320 .481 .345 .872 .235 .284 .277 .140 .024 .164 .112 8.65 4.88 316383232 4 .310 .067 1.11  .620 .012 .001 .00  .00  .025 .131 2
minepump_spec4_product21_true-unreach-call.cil.c 907    890    5203595264 226 5.65  .009 873     9.93 5.33 364568576 1 .247 .005 9.90 5.50 374452224 .290 .470 1.61  .346 .374 .350 .189 .013 .202 .134 9.22 5.14 329695232 4 .352 .090 1.42  .378 .025 .001 .00  .00  .026 .154 2
minepump_spec4_product22_true-unreach-call.cil.c 906    892    5113077760 195 5.29  .014 877     10.8  5.77 365150208 1 .912 .00  .011 .112 9.94 5.50 358088704 .435 .501 1.36  .392 .371 .358 .197 .012 .209 .129 9.03 5.07 323022848 4 .777 .109 .970 .355 .009 .001 .00  .00  .466 .160 2
minepump_spec4_product23_true-unreach-call.cil.c 906    889    5155328000 203 5.66  .011 874     11.0  5.86 351170560 1 .711 .00  .005 .079 9.63 5.42 361668608 .551 .486 1.25  .346 .396 .378 .216 .030 .246 .153 9.19 5.16 326230016 4 .344 .110 1.43  .324 .025 .001 .00  .00  .028 .168 2
minepump_spec4_product24_true-unreach-call.cil.c 906    891    5136867328 198 5.64  .006 875     11.8  6.33 350609408 1 .698 .00  .005 .022 9.54 5.35 356052992 .612 .418 1.24  .365 .339 .322 .191 .030 .221 .143 9.18 5.07 324009984 4 .360 .520 1.30  .304 .017 .002 .00  .00  .020 .145 2
minepump_spec4_product25_true-unreach-call.cil.c 906    892    5161005056 224 5.39  .017 876     9.32 5.01 349265920 1 .528 .005 8.38 4.68 343691264 .467 .311 .869 .280 .237 .229 .109 .009 .118 .088 8.69 4.85 314245120 5 .301 .108 1.19  .255 .012 .003 .00  .00  .022 .124 3
minepump_spec4_product26_true-unreach-call.cil.c 906    891    5115670528 195 5.14  .011 877     9.64 5.20 348868608 1 .483 .005 8.73 4.84 349196288 .553 .387 .851 .203 .316 .305 .156 .012 .168 .132 8.36 4.67 316182528 4 .282 .080 1.07  .246 .010 .001 .00  .00  .023 .125 2
minepump_spec4_product27_true-unreach-call.cil.c 906    891    5108039680 206 5.48  .017 876     9.98 5.36 359116800 1 .434 .012 8.98 5.01 346906624 .573 .386 .882 .197 .301 .290 .143 .026 .169 .114 8.91 4.90 316035072 5 .270 .097 1.34  .257 .017 .004 .00  .00  .013 .156 3
minepump_spec4_product28_true-unreach-call.cil.c 907    892    5118230528 199 5.41  .022 876     10.1  5.42 340271104 1 .606 .001 .015 .063 8.59 4.77 345137152 .504 .384 .877 .243 .287 .275 .151 .025 .176 .128 8.57 4.80 316846080 4 .319 .079 1.12  .246 .017 .00  .00  .00  .024 .110 2
minepump_spec4_product29_true-unreach-call.cil.c 906    890    5206351872 226 6.11  .014 872     10.5  5.69 363950080 1 .399 .013 9.22 5.15 361062400 .581 .416 1.13  .281 .341 .334 .173 .011 .184 .114 8.88 5.01 323031040 4 .716 .093 .926 .384 .011 .002 .00  .00  .024 .124 2
minepump_spec4_product30_true-unreach-call.cil.c 906    892    5128073216 197 4.57  .014 877     10.7  5.84 371507200 1 .401 .006 9.53 5.27 357543936 .640 .436 1.17  .330 .355 .336 .198 .023 .221 .159 8.64 4.90 323293184 4 .681 .092 .917 .305 .007 .001 .00  .00  .023 .144 2
minepump_spec4_product31_true-unreach-call.cil.c 906    889    5172875264 195 5.36  .017 874     10.7  5.79 360468480 1 .862 .002 .008 .049 9.96 5.55 359563264 .484 .512 1.28  .308 .411 .395 .217 .041 .258 .193 9.07 5.06 323465216 4 .759 .088 .959 .311 .018 .003 .00  .00  .034 .158 2
minepump_spec4_product32_true-unreach-call.cil.c 906    892    5092839424 204 5.58  .015 876     11.0  5.87 360112128 1 1.20  .006 9.30 5.17 358592512 .646 .500 1.15  .273 .417 .397 .206 .024 .230 .150 9.12 5.13 326823936 4 .368 .099 1.43  .309 .011 .001 .00  .00  .022 .164 2
minepump_spec4_product49_true-unreach-call.cil.c 906    889    5168111616 93 5.43  92.3   763     180    90.7  3150860288 15 3.02  3.69  .010 8.47  29.2  38.8   9.76 5.35 356974592 .595 .553 1.37  .328 .482 .466 .255 .046 .301 .140 9.86 5.67 339316736 5 .596 .149 1.76  .488 .015 .002 .00  .00  .059 .281 1
minepump_spec4_product50_true-unreach-call.cil.c 906    891    5115121664 91 5.72  88.2   769     241    121    4078383104 17 3.23  5.10  .025 11.6   30.8  62.7   9.82 5.47 371200000 .548 .559 1.39  .345 .461 .447 .258 .029 .287 .129 8.97 5.03 327958528 3 .371 .468 1.44  .428 .014 .002 .00  .00  .027 .131 1
minepump_spec4_product51_true-unreach-call.cil.c 907    893    3657801728 82 5.34  418     443     230    116    3965968384 16 3.04  13.0   .012 10.5   28.0  54.8   11.2  6.18 385073152 .608 .880 1.99  .488 .748 .727 .398 .080 .478 .202 9.66 5.40 334012416 4 .466 .111 1.56  .808 .012 .002 .00  .00  .034 .158 1
minepump_spec4_product52_true-unreach-call.cil.c 904    891    3327643648 75 5.06  312     551     139    70.1  2245005312 11 3.19  4.19  .011 5.57  24.5  25.5   10.8  5.98 384180224 .543 .941 1.99  .459 .799 .688 .418 .080 .498 .214 10.1  5.71 348073984 3 .606 .149 1.63  .474 .028 .004 .00  .00  .031 .121 0
minepump_spec4_product53_true-unreach-call.cil.c 905    892    3732959232 78 5.86  61.0   799     148    74.8  2718486528 12 3.07  2.74  .006 6.61  25.6  29.6   13.0  7.09 377946112 .789 .986 2.34  .499 .839 .806 .466 .077 .543 .253 11.8  6.64 360988672 5 .755 .154 2.34  .671 .040 .003 .00  .00  .059 .349 1
minepump_spec4_product54_true-unreach-call.cil.c 905    891    3714043904 77 6.12  67.8   790     176    88.7  2995793920 13 3.14  3.52  .017 8.21  28.8  37.4   12.8  7.01 406687744 .244 1.41  3.30  .996 1.23  1.18  .743 .166 .909 .480 9.88 5.54 344739840 3 .419 .124 1.87  .941 .021 .001 .00  .00  .034 .146 1
minepump_spec4_product55_true-unreach-call.cil.c 906    892    3637100544 74 5.97  385     474     141    71.2  2515992576 10 3.30  4.34  .012 5.61  23.3  26.7   13.2  7.17 401891328 .621 1.36  3.01  .641 1.20  1.17  .779 .114 .893 .287 9.97 5.57 341389312 3 .423 .585 1.77  .505 .032 .001 .00  .00  .041 .150 1
minepump_spec4_product56_true-unreach-call.cil.c 904    891    3320840192 68 5.53  316     547     176    88.7  3227058176 12 2.88  6.52  .006 9.07  27.8  35.0   11.9  6.49 382189568 .261 1.11  2.69  .440 .949 .915 .551 .128 .679 .300 11.8  6.68 356573184 6 .834 .131 2.38  1.13  .022 .002 .00  .00  .046 .374 1
minepump_spec4_product57_true-unreach-call.cil.c 905    891    3689918464 78 5.71  61.5   798     241    121    3806273536 16 2.64  4.94  .004 12.0   35.3  59.0   11.4  6.30 371458048 .609 1.00  2.10  .465 .851 .828 .509 .097 .606 .247 9.56 5.39 335065088 3 .443 .153 1.55  .391 .048 .002 .00  .00  .031 .141 1
minepump_spec4_product58_true-unreach-call.cil.c 906    892    3683807232 77 5.53  64.1   798     206    103    3668402176 14 2.99  4.83  .017 10.3   29.7  48.0   12.6  6.91 378753024 .719 1.11  2.39  .479 .922 .896 .540 .101 .641 .294 9.98 5.56 342339584 3 .476 .149 1.55  .440 .028 .001 .00  .00  .035 .144 1
minepump_spec4_product59_true-unreach-call.cil.c 907    893    3580981248 74 5.63  415     447     199    100    3237326848 13 3.00  7.77  .010 9.04  26.7  46.5   11.5  6.41 374251520 .656 1.18  2.17  .413 1.06  .990 .643 .122 .765 .294 10.4  5.80 345120768 4 .561 .145 1.75  .378 .023 .003 .00  .00  .037 .239 1
minepump_spec4_product60_true-unreach-call.cil.c 906    891    3203076096 66 5.23  325     539     203    102    3531526144 13 3.01  6.87  .034 9.30  27.4  48.4   11.5  6.37 386019328 .223 1.09  2.66  .837 1.00  .981 .615 .117 .732 .312 10.2  5.65 340938752 3 .510 .108 1.67  .935 .012 .00  .00  .00  .045 .154 1
minepump_spec4_product61_true-unreach-call.cil.c 906    891    3650867200 69 6.11  74.1   786     149    74.9  2712330240 11 3.39  3.09  .012 8.18  26.7  25.2   14.7  7.97 413380608 .272 1.61  3.88  .592 1.45  1.36  .796 .167 .963 .550 10.5  5.90 345223168 3 .449 .593 2.09  .598 .014 .001 .00  .00  .030 .164 1
minepump_spec4_product62_true-unreach-call.cil.c 905    890    3572269056 67 6.46  81.8   778     152    76.8  2606301184 11 3.98  2.83  .007 7.44  29.4  24.5   14.1  7.70 421801984 .244 1.69  3.99  1.13  1.52  1.46  .848 .244 1.09  .550 10.5  5.92 347103232 3 .448 .157 2.10  1.03  .019 .001 .00  .00  .030 .156 1
minepump_spec4_product63_true-unreach-call.cil.c 913    899    5247086592 110    55.7  2333605888 8 3.09  3.62  .006 4.91  22.0  15.0   15.7  8.50 431091712 .264 1.97  4.51  1.16  1.73  1.68  .795 .447 1.24  .783 10.4  5.84 352833536 3 .483 .167 2.02  .541 .029 .003 .00  .00  .028 .178 1
minepump_spec4_product64_true-unreach-call.cil.c 904    890    3485556736 63 6.51  293     567     157    79.5  2722811904 10 2.96  6.03  .004 7.18  26.3  29.3   13.4  7.47 403771392 .282 1.84  3.60  .679 1.40  1.32  .719 .225 .944 .613 10.5  5.88 357105664 3 .505 .193 1.91  .788 .015 .001 .00  .00  .029 .189 1
minepump_spec5_product01_true-unreach-call.cil.c 906    892    5097181184 191 4.76  .012 878     10.2  5.46 344145920 1 .476 .001 .005 .092 8.05 4.47 338948096 .404 .231 .650 .206 .183 .173 .095 .006 .101 .115 8.23 4.61 316084224 1 .047 .748 1.20  .231 .678 .668 .567 .014 .583 .023 0 .589
minepump_spec5_product02_true-unreach-call.cil.c 905    891    5108150272 179 5.02  .021 877     9.98 5.39 363708416 1 .619 .00  .006 .041 7.86 4.42 343351296 .430 .254 .674 .230 .208 .194 .101 .009 .110 .121 8.25 4.61 313528320 1 .047 .803 1.29  .231 .722 .715 .637 .011 .650 .029 0 .653
minepump_spec5_product03_true-unreach-call.cil.c 905    889    5141774336 183 4.86  .015 875     12.1  6.46 384008192 1 .578 .00  .014 .023 8.20 4.57 341000192 .413 .291 .673 .175 .232 .219 .111 .008 .119 .133 8.13 4.58 311054336 1 .047 .644 1.18  .276 .580 .569 .090 .004 .095 .027 0 .109
minepump_spec5_product04_true-unreach-call.cil.c 905    891    3691892736 173 5.04  .014 877     11.9  6.28 345800704 1 .893 .00  .004 .048 8.34 4.69 340914176 .485 .279 .682 .193 .224 .207 .107 .006 .113 .131 7.95 4.47 310976512 1 .039 .255 1.15  .262 .195 .193 .111 .009 .122 .031 0 .126
minepump_spec5_product05_true-unreach-call.cil.c 906    892    5113929728 196 5.39  .010 877     9.69 5.18 355135488 1 .349 .006 8.86 4.96 337461248 .513 .402 .878 .213 .308 .300 .191 .012 .203 .217 8.65 4.79 315514880 1 .045 .351 1.37  .267 .294 .280 .176 .013 .190 .030 0 .195
minepump_spec5_product06_true-unreach-call.cil.c 905    891    3699761152 173 4.73  .009 877     11.1  5.94 353800192 1 .660 .00  .005 .057 8.40 4.69 336453632 .467 .371 .853 .232 .310 .292 .163 .015 .178 .192 9.23 5.05 310206464 1 .049 .376 1.48  .257 .313 .299 .190 .017 .208 .029 0 .214
minepump_spec5_product07_true-unreach-call.cil.c 906    890    5156306944 184 5.17  .009 875     12.4  6.60 391757824 1 .593 .00  .005 .036 8.44 4.74 342401024 .459 .384 .858 .226 .312 .303 .205 .012 .217 .230 8.02 4.52 315379712 1 .051 .366 1.19  .258 .317 .299 .187 .008 .196 .031 0 .204
minepump_spec5_product08_true-unreach-call.cil.c 906    893    5137575936 177 5.12  .012 878     12.0  6.45 365473792 1 .797 .00  .009 .075 8.74 4.85 338518016 .525 .400 .863 .245 .312 .303 .178 .013 .191 .216 8.63 4.83 314654720 1 .044 .366 1.44  .260 .273 .266 .149 .011 .161 .044 0 .166
minepump_spec5_product09_true-unreach-call.cil.c 906    891    5108625408 189 4.93  .007 877     10.3  5.54 352563200 1 .595 .001 .005 .057 7.91 4.46 336580608 .353 .265 .676 .207 .196 .185 .099 .008 .107 .118 8.03 4.44 303685632 1 .039 .260 1.15  .231 .198 .193 .097 .008 .106 .038 0 .113
minepump_spec5_product10_true-unreach-call.cil.c 906    892    5322633216 179 5.16  .011 877     10.3  5.57 341204992 1 .766 .00  .010 .084 8.24 4.63 334168064 .434 .289 .703 .206 .232 .223 .117 .009 .126 .140 7.81 4.38 307326976 1 .048 .629 1.06  .184 .558 .550 .463 .009 .473 .023 0 .480
minepump_spec5_product11_true-unreach-call.cil.c 906    892    5119651840 183 4.65  .014 878     10.5  5.62 351772672 1 .947 .013 8.46 4.71 338214912 .543 .258 .721 .219 .201 .188 .096 .007 .103 .119 8.35 4.69 305295360 1 .044 .731 1.25  .256 .659 .641 .109 .007 .117 .026 0 .122
minepump_spec5_product12_true-unreach-call.cil.c 906    892    3667542016 172 5.21  .012 878     11.7  6.18 352477184 1 .735 .001 .013 .022 7.97 4.49 343535616 .420 .269 .666 .202 .211 .206 .096 .007 .103 .119 7.94 4.36 308428800 1 .039 .643 1.13  .242 .557 .552 .473 .010 .485 .040 0 .488
minepump_spec5_product13_true-unreach-call.cil.c 906    892    5114486784 192 5.13  .013 877     10.6  5.71 365129728 1 .477 .00  .003 .056 8.49 4.73 344403968 .462 .339 .840 .238 .274 .263 .161 .012 .173 .184 8.31 4.64 313372672 1 .046 .353 1.39  .701 .296 .288 .183 .011 .195 .037 0 .201
minepump_spec5_product14_true-unreach-call.cil.c 906    892    5135319040 177 4.93  .013 878     10.8  5.80 361889792 1 .730 .001 .009 .078 8.76 4.86 340783104 .494 .338 .828 .245 .284 .278 .165 .015 .180 .193 8.51 4.72 315854848 1 .047 .396 1.43  .239 .323 .321 .173 .016 .190 .032 0 .200
minepump_spec5_product15_true-unreach-call.cil.c 906    892    5141508096 182 5.12  .012 878     10.9  5.88 351961088 1 .761 .00  .009 .387 8.05 4.49 340967424 .390 .352 .867 .281 .285 .279 .167 .013 .180 .198 8.39 4.73 306720768 1 .048 .358 1.32  .258 .288 .278 .169 .012 .182 .031 0 .192
minepump_spec5_product16_true-unreach-call.cil.c 906    892    5142224896 180 5.42  .010 877     11.3  6.00 346800128 1 .649 .001 .005 .081 8.51 4.82 350691328 .392 .370 .885 .246 .283 .277 .168 .011 .179 .197 8.34 4.71 313262080 1 .046 .731 1.31  .233 .663 .645 .509 .013 .523 .031 0 .533
minepump_spec5_product17_true-unreach-call.cil.c 906    888    5188898816 195 5.23  .010 873     10.8  5.78 373063680 1 .605 .00  .014 .023 8.83 4.90 344961024 .484 .401 .919 .245 .335 .328 .199 .017 .216 .232 8.72 4.90 314417152 1 .055 .369 1.40  .272 .305 .300 .199 .013 .214 .036 0 .219
minepump_spec5_product18_true-unreach-call.cil.c 910    894    5173440512 176 4.70  .009 881     10.3  5.54 362782720 1 .791 .005 8.86 4.96 340332544 .518 .386 .882 .220 .319 .310 .197 .013 .210 .220 8.62 4.85 308224000 1 .057 .420 1.52  .804 .325 .317 .199 .009 .210 .041 0 .215
minepump_spec5_product19_true-unreach-call.cil.c 906    889    5204885504 181 5.50  .019 874     11.9  6.34 354787328 1 .587 .001 .011 .030 8.74 4.89 354967552 .464 .434 .967 .250 .381 .368 .222 .028 .250 .268 8.73 4.87 310599680 1 .052 .929 1.54  .252 .824 .812 .721 .015 .737 .044 0 .739
minepump_spec5_product20_true-unreach-call.cil.c 906    888    5206736896 185 5.37  .014 873     11.2  6.05 374566912 1 .778 .00  .008 .099 8.86 4.94 349044736 .552 .513 1.04  .257 .430 .417 .260 .023 .283 .292 8.68 4.84 310067200 1 .053 .382 1.37  .264 .311 .299 .173 .011 .186 .032 0 .198
minepump_spec5_product21_true-unreach-call.cil.c 906    890    5134893056 192 5.31  .010 872     11.3  6.01 342376448 1 .895 .011 9.50 5.32 348663808 .088 .497 1.69  .358 .388 .375 .244 .023 .267 .283 9.66 5.35 332771328 1 .056 .564 1.81  .804 .461 .436 .295 .021 .318 .043 0 .321
minepump_spec5_product22_true-unreach-call.cil.c 905    887    5208567808 180 5.49  .010 872     11.7  6.30 379412480 1 1.05  .00  .019 .100 9.08 5.09 349995008 .489 .549 1.23  .325 .444 .430 .260 .017 .277 .288 9.29 5.18 326180864 1 .055 .531 1.68  .773 .394 .373 .235 .020 .256 .041 0 .262
minepump_spec5_product23_true-unreach-call.cil.c 906    892    5132849152 180 5.51  .013 876     12.1  6.46 387649536 1 1.04  .001 .006 .040 9.05 5.06 349786112 .439 .518 1.15  .256 .437 .426 .283 .019 .302 .317 9.55 5.30 329732096 1 .056 .503 1.80  .899 .392 .376 .253 .020 .274 .044 0 .281
minepump_spec5_product24_true-unreach-call.cil.c 906    892    5136318464 181 5.53  .006 877     11.9  6.34 382943232 1 1.06  .00  .014 .151 9.13 5.07 349081600 .568 .560 1.18  .295 .469 .450 .279 .018 .297 .316 9.55 5.32 334794752 1 .057 .504 1.70  .839 .414 .399 .262 .021 .285 .042 0 .289
minepump_spec5_product25_true-unreach-call.cil.c 906    892    5117915136 196 5.24  .012 877     9.96 5.39 360345600 1 .740 .00  .008 .122 9.15 5.07 345149440 .498 .417 .921 .249 .361 .349 .235 .013 .248 .262 8.94 4.97 319295488 1 .048 .466 1.53  .326 .360 .349 .225 .015 .242 .037 0 .244
minepump_spec5_product26_true-unreach-call.cil.c 905    891    3708538880 174 4.84  .012 877     11.0  5.92 352837632 1 .750 .00  .015 .085 8.42 4.73 345079808 .449 .407 .896 .249 .338 .335 .222 .011 .233 .248 8.67 4.83 311070720 1 .049 .414 1.46  .743 .342 .334 .219 .017 .237 .034 0 .240
minepump_spec5_product27_true-unreach-call.cil.c 905    888    5222174720 189 5.40  .011 873     12.0  6.38 384757760 1 .739 .00  .009 .078 7.98 4.49 341483520 .384 .387 .860 .237 .322 .314 .191 .012 .203 .219 8.51 4.77 314744832 1 .050 .760 1.38  .288 .693 .685 .586 .014 .601 .034 0 .608
minepump_spec5_product28_true-unreach-call.cil.c 906    888    5221629952 182 5.38  .012 873     11.7  6.28 379379712 1 .979 .001 .004 .097 8.70 4.86 346832896 .486 .378 .882 .221 .298 .286 .157 .013 .170 .186 8.53 4.75 309792768 1 .049 .403 1.38  .264 .332 .322 .227 .014 .242 .036 0 .245
minepump_spec5_product29_true-unreach-call.cil.c 906    891    5130698752 196 5.37  .016 875     11.7  6.24 374779904 1 .840 .001 .009 .027 9.65 5.33 348971008 .506 .649 1.37  .339 .557 .548 .360 .020 .380 .400 9.55 5.30 323420160 1 .057 .686 1.86  .779 .581 .567 .416 .020 .437 .050 0 .451
minepump_spec5_product30_true-unreach-call.cil.c 905    888    5197209600 177 5.29  .006 873     11.8  6.24 357842944 1 .749 .00  .025 .265 9.07 5.04 350539776 .528 .519 1.15  .320 .421 .396 .260 .020 .280 .304 9.52 5.26 331419648 1 .054 .948 1.72  .376 .836 .828 .684 .019 .704 .039 0 .708
minepump_spec5_product31_true-unreach-call.cil.c 905    891    5135753216 183 5.18  .010 876     11.5  6.12 375132160 1 .986 .009 9.44 5.23 349634560 .429 .655 1.29  .283 .562 .553 .383 .023 .406 .420 9.68 5.38 323325952 1 .061 .491 1.75  .831 .398 .381 .251 .021 .274 .042 0 .276
minepump_spec5_product32_true-unreach-call.cil.c 906    888    5257560064 181 5.15  .017 872     12.9  6.84 398938112 1 .986 .001 .005 .049 8.88 4.92 354185216 .538 .503 1.14  .295 .417 .410 .261 .019 .280 .302 9.27 5.19 322174976 1 .054 .546 1.72  .720 .440 .420 .283 .020 .304 .042 0 .310
minepump_spec5_product33_true-unreach-call.cil.c 909    894    5215121408 116 4.80  83.3   775     23.8  12.4  591372288 1 .827 .060 2.32  .153 4.60 .861 8.87 4.93 350531584 .461 .410 1.03  .272 .328 .317 .161 .027 .188 .210 9.53 5.40 333987840 6 .872 .476 1.32  .303 .411 .400 .254 .017 .310 .236 1 .279
minepump_spec5_product34_true-unreach-call.cil.c 907    892    5101244416 105 4.70  65.8   793     23.6  12.3  615116800 1 .860 .095 2.00  .043 4.36 .957 8.73 4.87 352722944 .519 .463 1.02  .252 .386 .377 .190 .037 .227 .252 8.91 5.05 320352256 3 .323 .294 1.38  .695 .234 .221 .136 .012 .184 .111 1 .151
minepump_spec5_product35_true-unreach-call.cil.c 906    893    5113446400 104 5.02  75.9   783     62.8  31.8  1193754624 6 1.83  1.77  9.13  2.27  12.3  8.10  9.03 5.03 347824128 .511 .590 1.16  .241 .502 .481 .281 .057 .338 .361 9.18 5.14 322179072 3 .298 .814 1.45  .261 .714 .704 .149 .014 .187 .111 1 .168
minepump_spec5_product36_true-unreach-call.cil.c 905    892    1925718016 60 3.45  703     172     55.3  28.1  1033682944 4 1.84  1.78  5.49  1.93  10.7  6.34  13.2  7.31 387104768 .866 1.85  2.98  .401 1.72  1.68  .929 .303 1.23  1.31  13.2  8.28 362897408 20 1.57  1.19  3.42  .468 1.08  1.07  .854 .034 1.02  1.28  1 .904
minepump_spec5_product37_true-unreach-call.cil.c 904    892    2905546752 65 4.52  561     309     30.0  15.5  661860352 1 1.40  .110 2.68  .339 6.29 1.21  12.4  6.87 385724416 .568 1.53  2.81  .503 1.30  1.25  .717 .165 .882 .931 14.1  8.48 367190016 14 1.39  .931 3.55  .577 .817 .786 .567 .045 .723 1.01  1 .624
minepump_spec5_product38_true-unreach-call.cil.c 906    892    2921250816 64 4.65  556     315     27.6  14.2  688541696 1 1.09  .100 .006 .079 5.26 2.10  13.4  7.23 394772480 .693 1.71  3.02  .515 1.56  1.52  .831 .228 1.06  1.13  13.7  8.35 358588416 14 1.55  .907 3.42  .572 .790 .764 .538 .037 .707 .992 1 .583
minepump_spec5_product39_true-unreach-call.cil.c 904    891    2942156800 62 4.29  601     268     68.0  34.5  1331023872 5 2.34  1.51  9.56  1.99  13.9  8.86  13.1  7.25 381267968 .672 1.69  2.99  .485 1.53  1.50  .872 .248 1.12  1.19  14.2  8.64 358133760 14 1.39  .964 3.75  .958 .831 .806 .572 .048 .740 1.07  1 .630
minepump_spec5_product40_true-unreach-call.cil.c 905    892    2142195712 57 4.30  668     205     421    212    4662988800 20 3.50  38.4   .005 20.5   38.8  101     12.5  6.87 389263360 .568 1.63  2.84  .460 1.48  1.44  .868 .228 1.10  1.17  12.0  7.02 353730560 10 .926 .859 2.81  .517 .748 .719 .492 .040 .583 .575 1 .539
minepump_spec5_product41_true-unreach-call.cil.c 905    892    3516014592 84 4.30  439     426     26.9  13.9  602103808 1 .961 .043 2.26  .148 5.44 .987 10.3  5.72 367943680 .482 1.08  1.91  .314 .967 .949 .582 .118 .700 .728 9.47 5.38 326545408 3 .359 .444 1.60  .325 .350 .339 .221 .018 .265 .128 1 .247
minepump_spec5_product42_true-unreach-call.cil.c 907    888    3601924096 83 4.51  430     431     24.2  12.5  614031360 1 .858 .127 2.06  .131 3.21 2.90  11.2  6.24 367595520 .617 1.10  2.14  .412 .960 .940 .532 .118 .650 .686 10.3  5.99 338231296 6 .590 .573 2.03  .353 .473 .455 .314 .021 .389 .315 1 .343
minepump_spec5_product43_true-unreach-call.cil.c 907    893    3231801344 76 4.43  489     378     66.0  33.5  1175670784 5 2.18  2.17  8.91  2.73  12.9  7.65  11.1  6.15 367345664 .595 1.27  2.16  .390 1.16  1.12  .648 .155 .803 .863 12.0  7.16 358100992 11 1.42  .775 2.32  .462 .633 .621 .439 .029 .536 .605 2 .474
minepump_spec5_product44_true-unreach-call.cil.c 905    892    1972707328 55 3.40  692     183     44.2  22.5  896372736 3 1.54  1.17  .006 1.44  7.72 5.52  13.4  7.56 390955008 .710 2.23  3.43  .482 2.06  2.04  1.20  .369 1.57  1.64  17.8  11.8  378540032 21 4.07  1.14  4.24  .585 1.03  1.01  .727 .056 1.01  1.88  0 .794
minepump_spec5_product45_true-unreach-call.cil.c 905    892    2064257024 52 4.26  675     199     33.2  17.1  730206208 1 1.27  .821 2.96  .318 7.18 1.57  13.1  7.20 395165696 .632 1.66  3.07  .605 1.49  1.46  .872 .201 1.07  1.14  15.8  9.77 363167744 14 1.88  1.66  4.36  .627 1.44  1.43  .682 .054 .865 1.31  1 .748
minepump_spec5_product46_true-unreach-call.cil.c 905    892    2046054400 51 4.24  670     205     27.9  14.4  660959232 1 1.34  .113 2.27  .097 5.94 1.24  14.3  7.99 405118976 .887 2.18  3.72  .513 1.99  1.96  1.32  .225 1.55  1.59  16.1  9.77 374644736 14 2.09  1.58  4.16  .545 1.41  1.40  .764 .050 .928 1.30  1 1.21 
minepump_spec5_product47_true-unreach-call.cil.c 905    891    2129080320 50 4.62  693     179     84.5  42.7  1557684224 6 2.78  2.07  .012 2.77  16.5  11.4   16.5  9.01 425435136 1.01  2.59  4.16  .469 2.38  2.33  1.49  .390 1.88  1.93  13.5  8.02 367632384 10 1.06  .966 3.52  1.08  .802 .785 .531 .047 .649 .841 1 .583
minepump_spec5_product48_true-unreach-call.cil.c 906    891    3014717440 54 4.60  616     254     226    114    3390763008 15 3.69  19.3   .008 10.8   30.3  40.8   12.7  7.09 388050944 .603 1.78  3.08  .507 1.66  1.65  .924 .322 1.25  1.29  13.1  7.88 359178240 10 1.12  1.36  3.34  .533 .832 .790 .576 .049 .695 .791 1 .632
minepump_spec5_product49_true-unreach-call.cil.c 906    893    5126254592 91 5.03  73.3   786     27.7  14.3  632975360 1 1.16  .078 2.53  .116 5.62 1.20  11.3  6.26 382406656 .571 1.15  2.22  .321 1.02  .982 .578 .087 .665 .710 9.93 5.58 329957376 3 .324 .933 1.85  .397 .808 .795 .664 .020 .710 .137 1 .691
minepump_spec5_product50_true-unreach-call.cil.c 906    892    5121679360 89 5.47  78.4   779     29.1  15.0  662024192 1 1.17  .112 2.60  .124 6.33 1.18  11.4  6.32 383238144 .607 1.10  2.29  .456 .975 .934 .490 .100 .590 .660 11.4  6.50 352714752 5 .617 .716 2.51  .455 .606 .574 .401 .035 .506 .432 1 .445
minepump_spec5_product51_true-unreach-call.cil.c 908    893    5143244800 90 5.84  99.6   757     60.2  30.6  1041088512 3 2.44  1.76  6.12  1.38  12.8  6.38  11.4  6.36 374075392 .721 1.10  2.15  .411 .977 .958 .533 .118 .651 .696 11.4  6.52 334032896 6 .630 .650 2.50  .911 .547 .530 .353 .034 .441 .422 2 .407
minepump_spec5_product52_true-unreach-call.cil.c 904    892    2944012288 60 4.50  610     261     61.8  31.4  1037090816 3 2.22  1.40  6.05  1.68  12.8  6.78  11.3  6.28 372670464 .570 1.09  2.21  .496 .952 .920 .503 .121 .624 .657 14.3  8.82 364855296 13 1.49  1.00  3.90  .664 .878 .854 .620 .047 .772 1.14  1 .675
minepump_spec5_product53_true-unreach-call.cil.c 906    893    5203808256 78 6.03  77.5   782     33.0  16.9  804737024 1 1.48  .390 3.04  .237 7.35 1.13  14.1  7.59 401190912 .372 1.38  3.48  .696 1.20  1.16  .663 .148 .811 .849 10.5  5.97 345522176 3 .398 .575 2.25  .942 .476 .457 .323 .021 .367 .185 1 .351
minepump_spec5_product54_true-unreach-call.cil.c 905    891    3763580928 75 6.22  64.5   793     35.7  18.3  812285952 1 2.03  .795 2.85  .221 7.30 1.09  14.7  7.86 401428480 .388 1.59  3.90  1.14  1.34  1.29  .753 .173 .926 .975 12.5  7.26 366194688 5 .748 1.22  3.08  .708 1.06  1.05  .440 .043 .534 .377 1 .910
minepump_spec5_product55_true-unreach-call.cil.c 906    891    5246029824 78 6.49  73.8   783     72.3  36.6  1451524096 5 2.60  2.36  .004 1.51  16.6  6.94  14.4  7.86 403410944 .663 1.87  3.57  .606 1.69  1.64  .885 .315 1.20  1.26  12.6  7.30 370466816 5 .827 .780 3.03  .685 .640 .611 .434 .033 .520 .360 1 .476
minepump_spec5_product56_true-unreach-call.cil.c 904    890    3074801664 56 5.47  537     330     59.0  29.8  1028972544 3 2.43  1.04  5.71  1.32  13.1  5.67  14.3  7.82 414220288 .230 1.65  3.74  1.08  1.49  1.45  .897 .203 1.10  1.14  14.9  8.64 381685760 8 1.27  1.56  3.98  .831 1.38  1.34  .666 .051 .788 .677 1 .721
minepump_spec5_product57_true-unreach-call.cil.c 905    891    2997850112 58 4.93  557     311     32.8  16.8  808603648 1 1.33  .166 3.12  .479 7.13 1.88  12.1  6.66 377188352 .657 1.24  2.42  .475 1.12  1.09  .663 .092 .755 .809 11.7  6.76 349650944 5 .794 .724 2.58  .475 .606 .591 .411 .036 .526 .381 1 .454
minepump_spec5_product58_true-unreach-call.cil.c 904    891    2969849856 58 4.84  594     275     31.4  16.2  717971456 1 1.26  .077 .005 .083 7.58 1.33  11.2  6.18 376287232 .511 1.11  2.23  .411 .953 .933 .495 .105 .600 .643 11.9  6.83 355926016 5 .732 1.41  2.72  .490 1.25  1.23  1.05  .037 1.14  .349 1 1.09 
minepump_spec5_product59_true-unreach-call.cil.c 905    891    3017904128 57 5.15  615     253     63.0  32.1  1175068672 4 2.50  2.51  .006 1.38  13.6  5.44  11.0  6.14 366407680 .591 1.15  2.17  .339 1.00  .979 .568 .105 .673 .707 12.0  6.82 350248960 6 .834 .754 2.64  .948 .645 .632 .434 .037 .529 .370 2 .480
minepump_spec5_product60_true-unreach-call.cil.c 904    891    2986418176 55 4.73  555     314     253    127    4128813056 14 3.00  15.6   .013 10.8   29.2  61.2   12.2  6.70 372383744 .726 1.20  2.31  .442 1.06  1.01  .600 .139 .739 .778 12.5  7.12 349827072 5 .767 .773 2.82  1.07  .689 .675 .491 .038 .594 .393 1 .535
minepump_spec5_product61_true-unreach-call.cil.c 905    891    3058290688 55 5.69  495     372     42.9  21.9  891396096 1 2.45  .780 4.13  .335 8.09 2.75  14.8  8.05 415129600 .308 1.56  3.91  1.23  1.37  1.32  .766 .177 .943 1.00  11.8  6.62 362262528 3 .896 .700 2.37  .651 .534 .507 .357 .033 .420 .311 1 .397
minepump_spec5_product62_true-unreach-call.cil.c 905    891    3078393856 55 5.30  517     350     42.5  21.8  998920192 1 1.96  .852 3.90  .187 8.84 2.93  14.1  7.56 415444992 .263 1.54  3.63  .766 1.37  1.34  .883 .094 .977 1.01  13.8  7.92 367714304 5 .924 .999 3.63  .745 .869 .829 .578 .045 .681 .519 1 .627
minepump_spec5_product63_true-unreach-call.cil.c 905    891    3053686784 54 5.95  589     275     61.5  31.2  1046536192 3 2.74  .979 7.00  1.16  14.7  4.87  15.4  8.30 386637824 .291 1.83  4.32  .793 1.64  1.55  .901 .214 1.11  1.17  14.1  8.01 369418240 5 .884 .988 3.64  1.25  .810 .783 .574 .049 .683 .495 1 .627
minepump_spec5_product64_true-unreach-call.cil.c 904    890    3070738432 51 5.65  519     347     289    145    4451389440 14 3.42  15.9   .003 16.5   37.7  63.0   13.8  7.54 399405056 .731 1.53  3.34  .772 1.31  1.27  .783 .145 .928 .960 14.3  8.20 371257344 5 .915 .954 3.75  .766 .815 .764 .522 .048 .628 .546 1 .586
minepump_spec5_productSimulator_true-unreach-call.cil.c 905    888    2367770624 45 9.91  665     196     95.0  48.0  1703079936 4 4.49  1.29  .005 1.17  25.3  6.32  22.9  13.0  586473472 .776 3.68  8.53  1.97  3.19  3.11  1.68  .703 2.38  2.48  27.8  17.6  631816192 21 4.54  2.20  9.31  1.95  1.87  1.82  1.30  .136 1.60  2.79  2 1.46 
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)
total tasks 357 236000 231000 1178820411392 39570 1780   32300    166000    357 105000 64200 921585393664 883 610   343    7540 372    2320 3600   357 113000 109000 377078599680 861 44300 45700 666 44200 44200 1420 42200 43600 43500 357 78700 74900 424366759936 2143 6610 485   11000 570 406   391   211   125   518   9430 552 340  
    correct results 41 1110 681 27773865984 280 157   9.48 7.73 270 19200 9730 339821944832 865 515   342    2390 372    2320 3600   239 4270 2930 102134771712 534 1130 1540 188 1090 1080 424 544 969 760 251 5640 4110 111896027136 1374 823 356   2340 305 309   300   161   92.6 290   1390 390 257  
        correct true 28 590 318 16492355584 243 94.2 5.71 5.30 257 17000 8640 304165896192 828 440   338    1930 367    2030 3510   239 4270 2930 102134771712 534 1130 1540 188 1090 1080 424 544 969 760 242 4610 3330 94193483776 1326 632 257   1860 203 220   214   116   60.1 211   1190 384 179  
        correct false 13 522 362 11281510400 37 62.8 3.77 2.43 13 2180 1100 35656048640 37 74.9 4.11 465 4.66 294 85.7 0 9 1030 774 17702543360 48 191 99.8 477 101 88.7 86.3 44.6 32.5 79.0 197 6 77.2
    incorrect results 0 0 0 0
        incorrect true 0 0 0 0
        incorrect false 0 0 0 0
score (357 tasks, max score: 615) 69 527 478 493
Run set bmc-bitprecise.BMC.ProductLines k-induction-bitprecise.k-Induction.ProductLines predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines impact-bitprecise.Impact.ProductLines