Tool CPAchecker 1.6.1-svn 24567
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-67-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-03-23 21:32:39 CET
Run set princess-q_auflia princess-qf_auflia princess-qf_uflia princess-q_uflia
Options -setprop cpa.predicate.encodeOverflowsWithUFs=true -setprop cpa.predicate.addRangeConstraintsForNondet=true -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -predicateAnalysis-heaparray -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop solver.solver=princess -heap 13000M -stack 100M -setprop cpa.predicate.useQuantifiersOnArrays=true -setprop cpa.predicate.encodeOverflowsWithUFs=true -setprop cpa.predicate.addRangeConstraintsForNondet=true -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -predicateAnalysis-heaparray -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop solver.solver=princess -heap 13000M -stack 100M -setprop cpa.predicate.encodeOverflowsWithUFs=true -setprop cpa.predicate.addRangeConstraintsForNondet=true -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -predicateAnalysis-PredAbsRefiner-ABEl -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop solver.solver=princess -heap 13000M -stack 100M -setprop cpa.predicate.encodeOverflowsWithUFs=true -setprop cpa.predicate.addRangeConstraintsForNondet=true -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -predicateAnalysis-PredAbsRefiner-ABEl -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop solver.solver=princess -heap 13000M -stack 100M -setprop cpa.predicate.useQuantifiersOnArrays=true -setprop cpa.predicate.maxArrayLength=-1
../sv-benchmarks/c/ status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 915    516    10900 8220   968    519    11700 7920   901    746    8300 10800   901    741    7870 12700  
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 901    754    6800 12100   901    763    6930 10300   903    760    6930 12700   901    728    7560 11000  
array-examples/sorting_bubblesort_false-unreach-call_ground.i 901    750    6860 8410   901    768    7050 11200   901    748    6990 10900   901    745    7090 10400  
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 901    726    8410 11200   901    716    8340 10300   901    708    8140 11300   901    707    8470 9930  
array-examples/sorting_selectionsort_false-unreach-call_ground.i 901    726    8240 12500   901    722    8280 10600   901    722    8100 10500   901    729    8360 11000  
array-examples/standard_allDiff2_false-unreach-call_ground.i 901    810    6070 11600   901    810    6230 13400   901    814    6200 10800   901    810    6190 10400  
array-examples/standard_copy1_false-unreach-call_ground.i 901    723    8420 9740   901    714    8210 10100   901    736    7390 12400   901    679    8910 9120  
array-examples/standard_copy2_false-unreach-call_ground.i 901    689    8340 9540   901    707    8430 12600   901    817    6170 10900   901    651    9010 10400  
array-examples/standard_copy3_false-unreach-call_ground.i 902    693    8570 11800   901    701    8540 9970   901    838    5280 11700   901    652    9210 10300  
array-examples/standard_copy4_false-unreach-call_ground.i 902    694    8610 10500   901    692    8450 10100   901    803    5290 11300   901    648    9240 9500  
array-examples/standard_copy5_false-unreach-call_ground.i 901    694    8510 10600   901    702    8530 9100   901    749    5690 12400   901    619    9180 9660  
array-examples/standard_copy6_false-unreach-call_ground.i 901    676    8730 12200   901    683    8870 11300   901    626    6170 10200   901    630    9130 10500  
array-examples/standard_copy7_false-unreach-call_ground.i 943    678    8970 10500   902    660    8820 9270   901    624    7040 8930   902    637    9800 9280  
array-examples/standard_copy8_false-unreach-call_ground.i 901    671    8960 9890   901    668    8970 11100   902    522    8860 10100   943    613    9810 9880  
array-examples/standard_copy9_false-unreach-call_ground.i 941    675    9130 9660   901    660    9080 9360   903    501    9940 8120   941    631    9680 10900  
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 901    651    8530 9260   901    676    8610 11300   906    714    7880 12600   901    642    8950 9470  
array-examples/standard_init1_false-unreach-call_ground.i 901    714    8430 9590   902    719    8420 11500   903    656    8070 9120   901    669    9310 10500  
array-examples/standard_init2_false-unreach-call_ground.i 901    686    8770 11200   901    699    8900 10900   908    654    8090 9710   901    636    9430 8700  
array-examples/standard_init3_false-unreach-call_ground.i 901    683    8950 10100   901    676    9010 9660   901    642    8310 9860   901    627    9470 10700  
array-examples/standard_init4_false-unreach-call_ground.i 902    677    8920 9830   942    687    9030 10000   901    628    8420 9890   901    627    9620 9100  
array-examples/standard_init5_false-unreach-call_ground.i 901    653    9210 9810   934    667    9160 12100   901    630    8370 10700   902    631    9810 11300  
array-examples/standard_init6_false-unreach-call_ground.i 901    656    9290 10100   907    641    9130 11300   901    625    8680 10500   930    614    9680 10100  
array-examples/standard_init7_false-unreach-call_ground.i 902    633    9130 9780   915    651    9180 10600   901    637    8720 8850   901    603    9960 8590  
array-examples/standard_init8_false-unreach-call_ground.i 901    633    9190 8580   902    655    9230 9790   901    625    9190 9860   901    590    9920 8290  
array-examples/standard_init9_false-unreach-call_ground.i 901    614    9340 8650   901    612    9240 11000   901    627    9110 9720   902    594    9940 9080  
array-examples/standard_minInArray_false-unreach-call_ground.i 901    717    8250 10500   902    716    8170 12100   901    727    8210 9950   901    705    8360 9550  
array-examples/standard_partition_false-unreach-call_ground.i 902    699    8190 10900   901    693    8230 10100   901    823    6030 11800   905    648    8500 10200  
array-examples/standard_running_false-unreach-call.i 902    691    8230 9410   901    701    8610 9940   901    749    7190 11500   901    684    8800 10200  
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 35.6  11.4  1270 321   36.9  11.7  1600 359   42.7  15.9  1950 389   43.5  16.0  1820 381  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 901    700    9970 9810   901    709    9200 10300   901    762    8150 10700   901    751    8630 11900  
array-examples/relax_true-unreach-call.i 902    784    7410 12200   921    783    7680 12600   901    762    7790 12700   901    760    7780 11200  
array-examples/sanfoundry_02_true-unreach-call_ground.i 901    717    8500 11200   901    715    8620 8980   901    705    8630 10300   901    713    8640 10200  
array-examples/sanfoundry_10_true-unreach-call_ground.i 901    736    7710 10300   901    735    7810 10600   901    715    6770 10900   901    749    7520 10600  
array-examples/sanfoundry_24_true-unreach-call.i 294    255    3330 4050   300    262    4790 3580   340    302    2220 5090   333    294    2530 4060  
array-examples/sanfoundry_27_true-unreach-call_ground.i 918    727    8280 11400   901    724    8220 10600   901    704    8230 9850   917    717    8220 10700  
array-examples/sanfoundry_43_true-unreach-call_ground.i 2.58 1.15 261 23.7 2.45 1.11 263 21.8 2.54 1.15 265 22.4 2.67 1.12 271 27.4
array-examples/sorting_bubblesort_true-unreach-call_ground.i 901    760    6970 10500   901    751    6850 12800   904    754    7010 10400   901    748    7130 11200  
array-examples/sorting_selectionsort_true-unreach-call_ground.i 907    716    8260 10700   915    724    8220 9590   901    722    8150 10700   901    726    8300 9550  
array-examples/standard_compareModified_true-unreach-call_ground.i 902    723    9240 10400   902    710    9210 9390   901    809    6420 11900   902    647    9390 10600  
array-examples/standard_compare_true-unreach-call_ground.i 901    709    8160 11400   902    730    8110 10200   901    709    8100 11100   902    721    8420 11500  
array-examples/standard_copy1_true-unreach-call_ground.i 901    731    8210 9870   911    714    8360 9940   904    743    7540 12000   922    668    8870 9610  
array-examples/standard_copy2_true-unreach-call_ground.i 902    694    8470 10500   902    703    8350 11300   901    815    6120 12100   901    651    8990 9170  
array-examples/standard_copy3_true-unreach-call_ground.i 902    705    8650 11400   902    695    8670 9120   901    835    5300 13100   901    646    9200 9240  
array-examples/standard_copy4_true-unreach-call_ground.i 901    693    8490 11300   926    691    8640 10900   901    801    5320 12500   902    628    9090 10200  
array-examples/standard_copy5_true-unreach-call_ground.i 901    682    8450 9980   901    689    8660 9270   901    744    5680 11900   901    630    9170 8700  
array-examples/standard_copy6_true-unreach-call_ground.i 902    682    8730 9770   902    689    8690 10100   902    639    6150 9750   901    627    9340 9380  
array-examples/standard_copy7_true-unreach-call_ground.i 940    678    8940 9410   943    690    8920 9450   901    604    7090 8970   902    609    9580 8050  
array-examples/standard_copy8_true-unreach-call_ground.i 929    676    8990 9190   938    671    8890 10000   901    519    8450 9080   920    596    9600 9860  
array-examples/standard_copy9_true-unreach-call_ground.i 901    674    9300 11000   901    681    9240 7940   901    493    9270 7710   901    620    9510 9020  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 902    655    8770 8920   939    689    8790 10300   914    716    7940 10800   901    653    9040 9350  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 916    674    8220 11200   937    692    8520 9640   915    717    8010 11000   901    671    8060 10900  
array-examples/standard_copyInitSum_true-unreach-call_ground.i 901    699    8300 9460   930    696    8540 8800   901    730    7570 9870   901    689    7990 10000  
array-examples/standard_copyInit_true-unreach-call_ground.i 901    697    8450 9220   901    693    8520 11500   901    742    7520 11800   902    655    9290 9700  
array-examples/standard_find_true-unreach-call_ground.i 901    712    8690 12300   902    713    8710 11300   901    661    8240 9270   901    663    9050 9870  
array-examples/standard_init1_true-unreach-call_ground.i 901    719    8530 9960   901    711    8460 10500   901    663    7690 9430   901    657    9200 11000  
array-examples/standard_init2_true-unreach-call_ground.i 901    701    8810 11100   901    698    8810 9170   901    673    6970 11200   901    647    9520 9360  
array-examples/standard_init3_true-unreach-call_ground.i 901    689    9020 7890   902    687    8910 9790   902    649    8330 10600   901    626    9460 10500  
array-examples/standard_init4_true-unreach-call_ground.i 901    686    9020 10000   901    685    9090 9960   901    624    8450 9400   913    619    9530 9010  
array-examples/standard_init5_true-unreach-call_ground.i 941    674    9290 9800   902    654    9040 9650   911    636    8720 10500   901    636    9650 10300  
array-examples/standard_init6_true-unreach-call_ground.i 901    663    8990 9820   902    642    9170 11000   902    621    8670 9650   901    629    9850 8730  
array-examples/standard_init7_true-unreach-call_ground.i 901    629    9010 9260   901    639    9300 10100   902    620    8840 10000   902    615    9920 9900  
array-examples/standard_init8_true-unreach-call_ground.i 902    652    9210 10600   901    635    9090 9390   901    621    8920 8170   901    603    10000 9480  
array-examples/standard_init9_true-unreach-call_ground.i 902    637    9410 9360   901    618    9440 8490   901    633    8810 9970   931    594    10000 8670  
array-examples/standard_maxInArray_true-unreach-call_ground.i 902    711    8270 10300   901    729    8300 9830   901    720    8360 9840   902    709    8230 10400  
array-examples/standard_minInArray_true-unreach-call_ground.i 918    724    8300 12600   910    722    8160 11200   901    723    8320 10500   901    725    8420 12000  
array-examples/standard_palindrome_true-unreach-call_ground.i 901    665    8410 10200   901    673    8290 10500   901    663    8600 10800   901    649    8530 11300  
array-examples/standard_partial_init_true-unreach-call_ground.i 901    732    8050 10800   901    722    7870 10100   901    829    5900 13000   902    708    8270 10000  
array-examples/standard_partition_original_true-unreach-call_ground.i 901    730    7960 11100   901    736    7950 10600   901    829    5930 10400   901    706    8430 12200  
array-examples/standard_partition_true-unreach-call_ground.i 902    690    8170 9580   902    696    8160 11300   901    731    7830 9820   901    683    8540 10400  
array-examples/standard_password_true-unreach-call_ground.i 901    718    8120 12000   901    720    8190 10000   901    731    8200 9450   901    717    8250 11100  
array-examples/standard_reverse_true-unreach-call_ground.i 911    623    8410 9440   901    659    8390 11600   901    714    8170 9820   902    669    8360 11900  
array-examples/standard_running_true-unreach-call.i 901    689    8450 10300   901    688    8280 9930   901    732    7800 9980   903    663    8770 10100  
array-examples/standard_sentinel_true-unreach-call_true-termination.i 901    841    5170 10700   901    820    5140 11900   442    244    9600 3450   901    816    5240 12900  
array-examples/standard_seq_init_true-unreach-call_ground.i 901    678    8810 10000   901    645    8530 9060   902    685    8330 11200   901    666    8460 11000  
array-examples/standard_strcmp_true-unreach-call_ground.i 901    746    7690 9710   901    751    7600 11000   932    207    13900 4560   936    204    14100 3850  
array-examples/standard_strcpy_original_true-unreach-call.i 901    717    8450 10600   901    709    8430 12000   901    753    6720 10000   901    684    8980 9060  
array-examples/standard_strcpy_true-unreach-call_ground.i 901    715    8620 10200   901    721    8640 10200   901    746    7210 12200   902    656    8920 11600  
array-examples/standard_two_index_01_true-unreach-call.i 901    730    7870 10200   901    741    7860 10700   917    732    7440 11300   901    712    8390 10300  
array-examples/standard_two_index_02_true-unreach-call.i 957    551    10500 8590   925    531    10300 9230   901    637    8490 11500   923    519    10400 7970  
array-examples/standard_two_index_03_true-unreach-call.i 960    549    10400 7810   944    533    10300 9160   901    609    8510 10400   949    528    10500 8190  
array-examples/standard_two_index_04_true-unreach-call.i 902    541    10400 8140   908    509    10100 7940   901    645    8600 8570   901    493    10300 7210  
array-examples/standard_two_index_05_true-unreach-call.i 938    535    10300 8180   905    518    10300 7940   901    637    8580 9670   926    512    10500 8750  
array-examples/standard_two_index_06_true-unreach-call.i 967    569    10700 9030   929    535    10400 7970   901    639    8500 9660   901    540    10700 9290  
array-examples/standard_two_index_07_true-unreach-call.i 957    550    10400 8200   901    543    10200 9210   901    638    8490 10000   915    526    10400 9500  
array-examples/standard_two_index_08_true-unreach-call.i 932    534    10500 8470   944    533    10300 7810   901    615    8960 9520   901    496    10400 7540  
array-examples/standard_two_index_09_true-unreach-call.i 935    534    10400 9150   950    565    10700 8180   905    631    8500 9430   905    499    10300 7270  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 901    830    5210 12100   901    826    5200 11700   901    831    5170 10800   901    834    5200 11000  
array-examples/standard_vector_difference_true-unreach-call_ground.i 901    699    7860 9750   901    700    7990 9620   901    810    5990 11600   901    724    7770 10700  
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 901    711    8670 11000   901    715    8430 10800   901    660    7760 9060   902    660    9120 11000  
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 5.96 1.95 483 51.0 901    866    5070 12100   902    661    8270 9730   901    659    9040 9740  
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 901    697    7750 11600   901    695    7670 9540   901    690    7560 9480   901    690    7960 11500  
array-industry-pattern/array_range_init_false-unreach-call.i 5.33 1.87 432 40.7 901    870    5050 10500   903    709    7550 11500   902    668    8940 9990  
array-industry-pattern/array_single_elem_init_false-unreach-call.i 905    697    7980 10000   901    697    7910 9920   903    758    6950 11900   901    644    8230 9580  
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 954    416    12600 7190   944    408    12700 7480   901    521    11100 7360   905    531    11500 9200  
array-industry-pattern/array_monotonic_true-unreach-call.i 901    711    8750 9440   901    710    8580 10100   901    741    7040 11600   901    643    9560 10100  
array-industry-pattern/array_mul_init_true-unreach-call.i 901    864    4950 11900   901    862    4950 12700   901    683    7670 10400   901    862    4940 12200  
array-industry-pattern/array_of_struct_break_true-unreach-call.i 6.95 2.21 509 55.8 901    863    5100 10600   905    243    13200 5230   901    704    8570 10100  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 5.22 1.84 410 45.8 901    872    5030 13500   901    698    7440 10300   910    600    9490 8560  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 901    706    8130 9090   901    701    8210 10500   901    736    7310 10900   901    691    8450 11600  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 4.94 1.80 387 37.7 901    873    5040 11600   901    687    7780 9820   935    605    10100 8680  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 9.44 2.80 581 73.6 901    858    5210 8190   901    603    7790 8670   901    854    5040 12000  
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 6.63 2.16 489 50.8 911    874    4390 6000   901    610    7770 9350   901    620    9470 8750  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 5.12 1.86 420 42.7 901    872    5070 11200   918    661    8290 10600   901    639    9200 9330  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 5.43 1.91 417 44.5 901    872    5060 11100   901    793    6100 11000   901    704    7700 9320  
array-industry-pattern/array_shadowinit_true-unreach-call.i 901    804    5880 13200   901    806    5840 9980   901    791    6040 10700   901    804    5810 11500  
reducercommutativity/rangesum05_false-unreach-call.i 909    198    14300 4920   921    217    14300 4870   930    219    14400 5680   939    203    14200 5710  
reducercommutativity/rangesum10_false-unreach-call.i 934    195    14300 5360   935    215    14300 4920   924    221    14300 5500   916    173    14200 4670  
reducercommutativity/rangesum20_false-unreach-call.i 909    187    14300 5320   913    192    14300 4760   930    206    14400 4860   953    180    14200 4280  
reducercommutativity/rangesum40_false-unreach-call.i 944    194    14200 4690   938    199    14300 5070   928    211    14200 5330   921    177    14200 5140  
reducercommutativity/rangesum60_false-unreach-call.i 921    213    14200 4680   951    193    14300 4520   904    203    14300 4950   917    172    14200 4860  
reducercommutativity/rangesum_false-unreach-call.i 901    834    4220 11400   901    848    4920 11400   901    853    4920 11100   901    834    4120 13900  
reducercommutativity/avg05_true-unreach-call.i 901    835    1330 12300   901    837    2620 13400   901    838    2400 10700   901    835    1540 8920  
reducercommutativity/avg10_true-unreach-call.i 901    836    2230 11400   901    834    3330 13300   901    837    3440 13800   901    837    2580 10800  
reducercommutativity/avg20_true-unreach-call.i 901    836    1190 11400   901    835    2750 10700   901    838    2780 11900   901    836    3400 11600  
reducercommutativity/avg40_true-unreach-call.i 901    834    2250 11900   901    836    1290 11500   901    835    2450 13500   901    835    1550 11700  
reducercommutativity/avg60_true-unreach-call.i 901    850    2550 11200   901    850    2350 10500   901    856    2300 12000   901    853    2580 11000  
reducercommutativity/avg_true-unreach-call.i 918    179    14300 4260   968    181    14200 4540   949    217    14300 5150   901    200    14200 4720  
reducercommutativity/max05_true-unreach-call_true-termination.i 901    810    5370 11200   901    800    5530 10900   901    775    6050 13000   901    793    5420 10800  
reducercommutativity/max10_true-unreach-call_true-termination.i 907    554    8090 8650   901    500    8050 8860   901    537    8290 8170   901    574    8390 9960  
reducercommutativity/max20_true-unreach-call.i 901    668    8380 9650   901    676    8440 9450   901    668    9100 9230   901    651    9110 11800  
reducercommutativity/max40_true-unreach-call.i 901    685    8190 11300   901    702    8280 11900   902    696    8370 10900   902    708    8190 10300  
reducercommutativity/max60_true-unreach-call.i 901    684    8370 10300   901    704    8320 11200   901    683    8380 12000   901    697    8070 10300  
reducercommutativity/max_true-unreach-call.i 60.6  29.5  2540 607   62.1  30.9  3240 612   38.9  11.8  1630 349   43.5  13.5  1230 327  
reducercommutativity/sep05_true-unreach-call.i 901    802    5610 11100   901    806    5640 11700   901    699    7710 10800   901    730    6760 10500  
reducercommutativity/sep10_true-unreach-call.i 906    797    6390 12500   901    787    6580 10200   901    787    6770 11200   901    779    6790 9860  
reducercommutativity/sep20_true-unreach-call.i 901    811    6070 9890   901    805    6320 11000   901    801    6510 13100   901    809    6380 13200  
reducercommutativity/sep40_true-unreach-call.i 901    808    6120 10800   901    808    6120 11200   901    803    6440 11600   901    804    6500 11400  
reducercommutativity/sep60_true-unreach-call.i 901    807    6120 11100   901    808    6120 10100   901    804    6350 11300   901    801    6460 10900  
reducercommutativity/sep_true-unreach-call.i 871    770    5690 11600   858    755    5660 10800   901    723    6890 11800   901    775    6020 10600  
reducercommutativity/sum05_true-unreach-call_true-termination.i 901    678    6790 9920   901    691    6970 11300   901    786    6030 10200   901    646    7230 9990  
reducercommutativity/sum10_true-unreach-call.i 902    562    9070 8720   902    565    9310 8640   945    645    9080 11600   902    658    9040 10300  
reducercommutativity/sum20_true-unreach-call.i 901    733    7370 10700   901    745    7250 11600   922    710    7980 10600   901    745    7360 9800  
reducercommutativity/sum40_true-unreach-call.i 902    738    7300 10600   901    745    7310 11800   901    726    7580 11700   901    720    7170 10500  
reducercommutativity/sum60_true-unreach-call.i 901    752    7260 12300   910    735    7410 10500   901    731    7730 10300   901    745    7130 11900  
reducercommutativity/sum_true-unreach-call.i 901    852    3690 11300   901    849    3740 13600   206    170    3350 2330   399    355    4050 5630  
bitvector/byte_add_false-unreach-call_true-no-overflow.i 964    249    14200 5900   968    255    14300 5760   964    259    14300 6000   966    247    14200 5030  
bitvector/sum02_false-unreach-call_true-no-overflow.i 968    290    14200 5830   968    283    14200 5450   968    287    14300 5890   968    285    14200 6260  
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 966    253    14200 6030   963    258    14300 5230   965    255    14300 5580   964    254    14200 6290  
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 965    253    14200 5730   966    253    14300 5220   968    272    14200 5840   964    251    14300 5280  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 901    701    5390 9560   901    692    5390 10400   901    676    5650 10400   901    697    5440 9700  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 901    864    4940 11100   901    863    4940 12900   901    862    4940 13100   901    862    4960 10900  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 901    242    14000 5330   918    246    13800 5730   944    251    13800 5960   904    248    14000 5360  
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 901    838    4960 13300   901    845    4930 11900   901    846    4960 13400   901    855    4930 12600  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 913    354    12700 7600   951    295    11800 5340   951    335    12300 6310   924    336    12200 6470  
bitvector/jain_1_true-unreach-call_true-no-overflow.i 11.4  3.32 494 93.4 11.0  3.17 476 84.5 11.0  3.14 524 91.8 10.6  3.09 505 84.4
bitvector/jain_2_true-unreach-call_true-no-overflow.i 21.4  5.78 731 173   17.9  4.82 744 144   19.5  5.24 735 151   20.1  5.34 761 185  
bitvector/jain_4_true-unreach-call_true-no-overflow.i 54.7  19.7  3140 470   53.7  19.6  2920 467   60.9  21.9  2770 486   56.2  20.2  2690 509  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 901    765    6890 10800   901    747    6930 10000   901    764    6870 9700   901    761    6840 12200  
bitvector/jain_6_true-unreach-call_true-no-overflow.i 922    429    12700 7560   923    428    12300 8090   963    416    11400 6920   919    413    11600 6550  
bitvector/jain_7_true-unreach-call_true-no-overflow.i 917    444    12600 7410   930    419    12400 7070   968    430    11400 7150   922    426    11700 7180  
bitvector/modulus_true-unreach-call_true-no-overflow.i 968    230    14200 4600   967    234    14100 5620   968    228    14200 4390   907    226    14000 4540  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 901    832    5800 12600   901    831    5790 13500   901    827    5810 11500   901    838    5700 11500  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 901    819    5750 10400   901    834    5610 11300   901    832    5700 13000   901    819    5800 11800  
bitvector/parity_true-unreach-call_true-no-overflow.i 901    830    5030 11500   901    833    5040 13400   901    837    5040 11600   901    844    5040 11300  
bitvector/sum02_true-unreach-call_true-no-overflow.i 968    292    14200 5430   968    286    14200 6410   968    288    14200 6720   968    298    14200 5930  
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 901    858    5000 10700   901    858    5070 11800   901    855    5050 13500   901    855    5100 11200  
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 901    851    2890 13500   901    852    2680 13100   901    852    3040 12100   901    852    2730 10900  
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 901    830    5380 11300   901    823    5460 11500   901    827    5380 13200   901    827    5410 11400  
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 901    855    5050 11000   901    858    5040 14200   901    855    5020 11700   901    857    5060 10700  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 901    849    3100 11500   901    853    2940 12700   901    851    2960 11600   901    852    2500 11600  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 901    849    3180 11200   901    848    3040 10900   901    847    2730 12200   901    847    2740 11100  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 937    476    10800 8720   923    476    10800 7300   921    465    10600 8110   961    491    12300 7540  
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 901    853    2590 12300   901    852    2690 11500   901    852    2580 11400   901    852    2540 11500  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 901    856    4440 13300   901    859    4980 11400   901    858    4520 11600   901    861    4960 11500  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 901    860    4970 10300   901    857    4500 12100   901    857    4560 10500   901    857    4120 12500  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 929    451    10600 7770   957    482    10500 8290   924    475    9810 8070   960    468    9970 8570  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 923    477    9680 7910   937    476    9430 8310   941    476    9690 8960   932    475    10700 7990  
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 968    424    11800 8180   923    402    10400 7610   932    420    11600 7930   923    406    10400 6800  
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 914    431    12200 7300   968    443    11800 7800   950    429    12200 7660   967    430    12000 7040  
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 959    440    12300 7760   918    433    12000 7700   912    435    12300 6920   918    436    11400 8280  
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 931    419    11500 5910   934    429    11600 7910   917    408    10800 8530   923    422    12300 7540  
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 932    447    12300 8100   912    445    12300 7330   912    442    12400 8760   919    438    11700 8050  
bitvector-regression/implicitfloatconversion_false-unreach-call.c 3.71 1.48 314 33.2 3.60 1.55 307 31.7 3.53 1.49 307 33.5 3.54 1.50 306 30.2
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 3.52 1.45 311 31.4 3.54 1.49 306 28.5 3.39 1.43 304 31.5 3.48 1.49 309 30.4
bitvector-regression/integerpromotion_false-unreach-call.c 6.43 2.11 363 48.5 6.05 1.99 372 50.7 5.87 2.02 366 45.8 6.26 2.08 388 45.6
bitvector-regression/recHanoi03_false-unreach-call.c 2.48 1.12 263 23.2 2.49 1.13 269 24.6 2.51 1.12 260 22.4 2.69 1.18 262 24.8
bitvector-regression/signextension2_false-unreach-call.c 3.64 1.49 313 30.6 3.61 1.49 304 32.7 3.69 1.48 317 30.6 3.58 1.52 314 31.4
bitvector-regression/signextension_false-unreach-call.c 4.03 1.56 325 37.2 3.58 1.48 296 31.7 3.71 1.48 315 29.7 3.97 1.68 317 36.0
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 3.22 1.39 293 28.6 3.41 1.50 307 29.7 3.53 1.44 309 29.8 3.41 1.52 293 29.9
bitvector-regression/integerpromotion_true-unreach-call.c 6.89 2.15 351 60.2 7.51 2.26 409 58.4 6.97 2.26 406 54.0 6.91 2.16 411 58.9
bitvector-regression/signextension2_true-unreach-call.c 5.23 1.88 340 42.5 4.88 1.80 347 40.6 5.33 1.87 346 45.1 5.18 1.81 356 38.7
bitvector-regression/signextension_true-unreach-call.c 5.13 1.85 347 37.5 5.37 1.92 369 41.6 5.21 1.84 340 43.5 5.11 1.80 357 39.5
bitvector-loops/diamond_false-unreach-call2.i 229    183    3300 3080   238    191    2730 2980   250    204    2560 3490   237    192    2640 2870  
bitvector-loops/overflow_false-unreach-call1.i 901    756    8150 10500   927    751    8310 12400   901    761    8060 11800   901    748    8160 11700  
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 958    755    7520 11800   912    762    7370 9650   911    829    5630 11600   911    735    6880 11200  
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 901    849    3020 14000   901    852    3730 13600   901    848    2820 12300   901    853    3150 11900  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 901    860    5050 12200   901    858    5040 9280   901    858    5050 12000   901    857    5040 13800  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 901    858    5040 12000   901    858    5040 11200   901    857    5070 13400   901    858    5060 13600  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 901    815    5700 12900   901    826    5520 11300   901    831    5420 10700   907    817    5710 12600  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 901    851    3140 11000   901    848    3000 12500   901    846    2860 12100   901    849    3230 11000  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 901    861    4260 12300   901    861    4590 12100   901    857    3910 12400   901    861    4840 12300  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 901    854    5040 13100   901    855    5050 11500   901    857    5040 12600   901    856    5030 13000  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 901    857    5060 9290   901    856    5060 12600   901    858    5060 11600   901    857    5070 12600  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 35.7  13.8  1650 370   35.4  13.8  2200 334   35.5  13.7  1660 332   33.9  13.9  1880 294  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 85.2  57.4  3220 1000   86.2  59.1  3020 828   84.4  57.0  3180 879   87.2  59.9  3210 953  
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 901    852    2470 11500   901    853    2440 12400   901    853    2610 13400   901    852    2360 11600  
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 901    852    2580 11600   901    852    2520 13900   901    852    2650 11900   901    852    2610 11600  
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 901    849    2810 11800   901    849    2750 12800   901    849    2920 12700   901    850    2740 12400  
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 901    849    2510 13500   901    851    2560 13900   901    851    2470 12600   901    852    2580 11900  
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 45.0  18.0  2770 376   45.3  17.8  2320 380   45.6  17.8  2200 398   45.2  17.7  2420 395  
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 901    851    4320 11300   901    850    3710 13200   901    852    3960 13300   901    849    3800 11800  
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 901    848    4760 11800   901    852    4770 11500   901    851    4970 11800   901    856    4960 12600  
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 901    850    3330 11300   901    855    3970 11800   901    852    4250 11800   901    852    3830 11600  
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 901    855    3160 10300   901    852    2880 10800   901    852    2840 11500   901    852    3010 13300  
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 901    849    2920 11100   901    846    3400 12300   901    847    2710 11700   901    843    2560 11800  
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 901    856    2890 11600   901    858    2890 12300   901    853    2690 13500   901    858    2840 11900  
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 40.2  16.7  2200 325   38.1  16.5  2330 329   39.2  16.7  2170 351   38.9  16.3  2400 345  
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 901    852    2480 11500   901    851    2740 11700   901    853    2410 11000   901    851    2490 14700  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 901    852    2670 14300   901    853    2420 13600   901    852    2580 11900   901    851    2580 13300  
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 901    849    2660 11800   901    852    2490 13100   901    850    2600 11000   901    850    2630 10600  
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 901    853    2570 11300   901    851    2440 11800   901    852    2510 11900   901    850    2860 11800  
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 901    848    2620 10600   901    853    4040 10300   901    848    2930 11800   901    848    3090 12600  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 901    851    2390 10900   901    850    3230 11600   901    845    2550 13900   901    849    2550 11700  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 17.6  4.78 731 148   16.1  4.28 746 133   17.0  4.55 704 144   15.7  4.22 740 132  
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 901    853    2650 12000   901    857    2780 13700   901    854    2700 10200   901    855    2900 11600  
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 901    851    3680 11500   901    849    3350 10900   901    851    4000 13300   901    852    3950 12500  
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 901    856    2600 11900   901    854    2850 12100   901    855    2690 12900   901    855    2670 13200  
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 901    848    2890 12100   901    846    2950 11500   901    847    3080 11400   901    847    3070 11100  
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 901    837    4960 12300   901    831    5480 13400   901    827    5580 11100   909    837    5480 10700  
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 901    853    3120 13800   901    854    3080 13600   901    857    2830 12900   901    856    3200 10300  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 38.9  14.2  1980 329   42.1  14.6  1970 348   41.6  15.2  2180 336   39.9  15.0  1930 381  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 39.1  13.8  2170 363   38.5  13.3  2100 328   41.6  14.3  2040 345   40.8  14.3  1920 348  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 36.9  15.4  1790 362   35.5  15.2  1300 307   28.0  9.50 1330 236   36.3  15.5  2340 324  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 901    846    3770 11400   901    845    3410 12100   901    778    6220 10600   901    845    4270 10600  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 66.7  39.0  3360 703   63.3  36.9  3130 754   63.5  34.7  2400 657   58.9  33.8  3260 635  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 901    856    4990 10400   901    852    5080 12200   901    849    5040 11600   901    853    5040 10700  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 134    101    4800 1420   106    76.6  4800 1200   98.9  69.0  4460 1080   119    86.8  4380 1390  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 901    852    5070 11900   901    850    5090 10800   901    856    5000 11000   901    853    5050 12600  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 10.2  2.91 405 81.2 9.70 2.79 485 71.2 10.8  3.07 525 93.1 10.1  2.90 492 71.1
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 18.4  4.92 720 151   16.8  4.49 720 137   18.4  4.92 696 130   18.2  4.88 507 146  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 17.2  4.62 647 137   16.8  4.54 497 143   15.8  4.44 646 130   16.7  4.48 626 122  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 30.5  9.08 1170 263   34.2  9.62 1430 290   41.3  13.4  1520 310   32.8  9.70 1330 248  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 105    72.7  2760 1060   103    71.7  2600 1090   97.1  69.8  3090 1190   102    71.6  3110 1120  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 901    854    5110 12800   901    853    5130 12200   901    854    5100 13100   901    847    4670 10200  
ntdrivers/diskperf_false-unreach-call.i.cil.c 901    852    5030 13800   901    850    5040 10800   901    852    5080 11300   901    847    5080 10900  
ntdrivers/floppy_false-unreach-call.i.cil.c 920    398    12400 8000   921    405    12700 7240   961    470    11700 9540   921    381    13000 6900  
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 901    815    5630 9810   901    811    5730 12100   901    831    5370 12200   901    814    5520 11400  
ntdrivers/parport_false-unreach-call.i.cil.c 901    848    2300 10200   901    845    2310 13500   901    850    2520 10800   901    847    2330 13200  
ntdrivers/cdaudio_true-unreach-call.i.cil.c 901    845    3740 11600   901    848    3640 12200   901    851    3450 13800   901    846    3530 12200  
ntdrivers/diskperf_true-unreach-call.i.cil.c 901    854    5050 11600   901    850    5020 11800   901    853    5050 11600   901    851    5040 13900  
ntdrivers/floppy2_true-unreach-call.i.cil.c 901    833    5220 12500   901    844    5050 13000   901    846    5050 12400   901    842    5030 11600  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 920    395    12700 7060   921    395    12300 7530   939    453    11600 7280   923    383    13000 7910  
ntdrivers/parport_true-unreach-call.i.cil.c 901    847    2380 11900   901    845    2420 11500   901    850    2500 11700   901    847    2500 12800  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 901    825    5310 12500   901    826    5280 11800   901    833    5160 12300   901    850    4670 11800  
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 901    851    5050 13800   901    854    5000 11500   901    846    5010 10600   901    849    3990 12100  
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 901    856    4940 10400   901    856    4880 11000   901    858    4990 12500   901    854    4980 13100  
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 901    854    5040 12700   901    851    5020 12100   901    850    5000 11500   901    850    4440 11700  
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 901    861    4970 13100   901    860    4970 11200   901    857    2820 13300   901    857    3130 11400  
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 901    847    3680 11600   901    847    3570 11600   901    855    3110 10800   901    855    3060 11000  
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 901    846    3460 10600   901    847    3550 13300   901    856    3080 11800   901    856    3250 11700  
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 901    846    3410 10800   901    847    3410 11200   901    855    2940 12300   901    855    3110 13000  
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 901    824    5290 11900   901    824    5380 9840   901    848    2750 13300   901    852    2710 11000  
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 901    843    3820 8890   901    843    3820 13200   901    860    3400 11100   901    856    3270 13400  
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 901    814    5510 10300   901    816    5340 12200   901    851    2490 12700   901    855    2730 14300  
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 901    845    3720 10800   901    844    3760 12100   901    859    3240 13800   901    858    3240 11000  
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 901    812    5370 10600   901    815    5330 11000   901    850    2910 13400   901    853    2770 10600  
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 901    858    4990 10800   901    855    4970 11200   901    852    3290 12900   901    858    3230 12200  
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 901    821    5330 11300   901    825    5280 11800   901    850    2600 10200   901    853    2680 10900  
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 901    854    5010 11200   901    858    5020 14000   901    862    4040 13400   901    857    3100 12500  
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 901    823    5230 11800   901    822    5260 11700   901    849    2590 11500   901    859    3070 11600  
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 901    814    5580 10800   901    820    5590 11100   901    851    2560 10800   901    856    2630 12700  
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 901    822    5340 10400   901    823    5300 11700   901    849    2750 11400   901    858    2630 13800  
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 901    858    5040 14200   901    856    5000 12800   901    853    4870 11300   901    852    5020 12500  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 901    851    5020 10400   901    852    5000 11700   901    850    5020 11300   901    850    4990 10300  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 901    857    5020 13500   901    853    5050 11900   901    844    5000 13700   901    849    4340 12000  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 901    853    5010 12800   901    853    5020 11400   901    850    4990 10800   901    851    4990 11100  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 901    858    4970 11200   901    855    5020 10400   901    852    2970 11900   901    858    3150 11200  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 901    848    4020 11600   901    844    2980 12500   901    856    3120 10500   901    856    3120 11400  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 901    853    4990 12400   901    856    4960 12500   901    860    3490 12100   901    856    2890 11600  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 901    845    3800 11300   901    844    3450 11400   901    859    3060 12500   901    855    3020 11500  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 901    853    4990 13000   901    857    5010 11400   901    859    3230 11100   901    853    3230 12200  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 901    840    3700 12100   901    845    3920 10000   901    857    3320 14100   901    860    3530 11600  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 901    856    5000 12700   901    857    4940 13900   901    857    3080 11800   901    852    3140 11700  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 901    856    5010 11300   901    857    5000 11900   901    853    3010 11400   901    856    3310 12400  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 901    854    4990 13100   901    853    5030 11400   901    860    3620 13500   901    853    3110 11800  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 901    857    5000 10700   901    857    5020 11700   901    860    3500 12600   901    858    3680 11300  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 901    854    5010 12200   901    856    5010 14000   901    861    3580 11900   901    853    3060 11900  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 901    857    4760 12700   901    858    5010 10800   901    854    2890 12600   901    854    3040 12700  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 901    856    5030 12200   901    855    5040 10200   901    860    3590 11400   901    853    3080 12700  
eca-rers2012/Problem01_label15_false-unreach-call.c 901    849    4950 11700   901    848    4980 11300   901    847    4990 11500   901    849    4990 12100  
eca-rers2012/Problem01_label20_false-unreach-call.c 901    851    4980 13700   901    853    4950 13200   901    852    4980 12200   901    854    4970 12800  
eca-rers2012/Problem01_label21_false-unreach-call.c 901    852    4980 12000   901    852    4950 12100   901    857    4960 11400   901    853    4960 11500  
eca-rers2012/Problem01_label32_false-unreach-call.c 901    848    5030 10800   901    853    4970 12800   901    852    5000 13000   901    851    4990 12200  
eca-rers2012/Problem01_label33_false-unreach-call.c 901    851    5040 11000   901    853    5000 11300   901    853    5000 12600   901    850    5030 12600  
eca-rers2012/Problem01_label35_false-unreach-call.c 901    852    4960 12600   901    853    4990 12700   901    849    4980 10800   901    848    4970 10500  
eca-rers2012/Problem01_label37_false-unreach-call.c 901    850    4990 11100   901    850    4960 12100   901    849    4970 11500   901    850    4960 11700  
eca-rers2012/Problem01_label38_false-unreach-call.c 901    847    4970 11700   901    853    4980 11600   901    851    4970 10700   901    853    4960 10800  
eca-rers2012/Problem01_label44_false-unreach-call.c 901    852    5030 11600   901    853    5040 11500   901    851    5010 10200   901    854    5010 12300  
eca-rers2012/Problem01_label47_false-unreach-call.c 901    852    4980 13000   901    852    4970 13200   901    851    4960 11400   901    850    4960 11800  
eca-rers2012/Problem01_label50_false-unreach-call.c 901    854    4970 11100   901    854    4960 12500   901    851    4970 13700   901    854    4950 10900  
eca-rers2012/Problem01_label56_false-unreach-call.c 901    853    5030 11100   901    851    5040 12900   901    855    5050 13000   901    850    5040 12700  
eca-rers2012/Problem01_label57_false-unreach-call.c 901    850    5020 14300   901    854    5060 12200   901    852    5020 11100   901    855    4990 10100  
eca-rers2012/Problem02_label13_false-unreach-call.c 901    828    5480 12000   901    826    5470 12100   901    829    5420 10900   901    830    5350 13800  
eca-rers2012/Problem02_label16_false-unreach-call.c 901    826    5600 10400   901    829    5390 11500   901    830    5390 13300   901    827    5400 13100  
eca-rers2012/Problem02_label43_false-unreach-call.c 901    820    5510 11000   923    724    7130 10500   901    819    5490 11800   904    746    6450 12000  
eca-rers2012/Problem02_label44_false-unreach-call.c 901    827    5400 12100   901    825    5560 12000   901    830    5450 11300   901    821    5550 14000  
eca-rers2012/Problem02_label45_false-unreach-call.c 901    848    5000 12800   901    838    5100 12900   901    846    5060 11800   901    840    5090 13300  
eca-rers2012/Problem02_label50_false-unreach-call.c 901    847    4990 11200   901    847    5000 11700   901    845    4970 12100   901    846    5000 13700  
eca-rers2012/Problem02_label59_false-unreach-call.c 901    768    6500 10800   901    759    6370 12900   901    764    6440 10700   901    770    6330 11300  
eca-rers2012/Problem03_label09_false-unreach-call.c 901    818    5110 12800   901    819    5120 11600   901    823    5120 10500   901    819    5100 11500  
eca-rers2012/Problem03_label13_false-unreach-call.c 901    825    5120 10700   901    822    5120 10800   901    820    5120 11500   901    822    5120 11100  
eca-rers2012/Problem03_label26_false-unreach-call.c 901    825    5130 13300   901    821    5100 11300   901    823    5110 11800   901    823    5120 13100  
eca-rers2012/Problem03_label27_false-unreach-call.c 901    828    5360 11700   901    831    5340 11500   901    830    5290 10500   901    830    5340 10800  
eca-rers2012/Problem03_label28_false-unreach-call.c 901    832    5330 11300   901    824    5350 13500   901    831    5310 11500   901    828    5370 11500  
eca-rers2012/Problem03_label31_false-unreach-call.c 901    816    5120 11900   901    819    5140 11600   901    818    5110 13500   901    820    5160 11200  
eca-rers2012/Problem03_label35_false-unreach-call.c 901    820    5160 11700   901    822    5150 11300   901    821    5150 11400   901    820    5100 9090  
eca-rers2012/Problem03_label37_false-unreach-call.c 901    627    7710 9420   901    625    7610 10200   901    642    7610 8910   901    641    7640 9850  
eca-rers2012/Problem03_label39_false-unreach-call.c 901    821    5090 12900   901    821    5120 13300   901    822    5120 11900   901    822    5120 12400  
eca-rers2012/Problem03_label43_false-unreach-call.c 901    822    5290 11500   901    819    5360 11300   901    824    5280 10000   901    822    5310 11300  
eca-rers2012/Problem03_label45_false-unreach-call.c 901    820    5110 12700   901    822    5110 14200   901    820    5120 11700   901    817    5130 11100  
eca-rers2012/Problem03_label50_false-unreach-call.c 901    828    5100 12100   901    822    5110 11700   901    824    5150 11100   901    824    5160 11500  
eca-rers2012/Problem03_label52_false-unreach-call.c 901    604    7930 9460   909    586    8070 10100   917    576    8310 7900   903    611    7970 9520  
eca-rers2012/Problem04_label04_false-unreach-call.c 901    612    6840 7380   901    626    6750 10100   902    629    6820 9580   901    629    6500 10400  
eca-rers2012/Problem04_label06_false-unreach-call.c 901    622    7040 8750   902    610    6850 10500   901    633    6490 8650   901    614    6790 9630  
eca-rers2012/Problem04_label09_false-unreach-call.c 901    620    6850 9560   901    624    6640 9660   901    625    6550 9150   901    630    6490 11300  
eca-rers2012/Problem04_label11_false-unreach-call.c 901    617    6740 11000   901    615    6640 9270   901    611    7070 9050   902    631    6520 10200  
eca-rers2012/Problem04_label12_false-unreach-call.c 901    608    6680 8580   901    622    6730 8170   901    629    6730 10000   901    619    6710 11100  
eca-rers2012/Problem04_label13_false-unreach-call.c 901    623    6830 10700   902    623    6450 9810   901    620    6600 10500   901    615    6780 7460  
eca-rers2012/Problem04_label14_false-unreach-call.c 902    615    6940 9380   902    611    6880 9320   901    634    6830 8680   901    624    6620 8500  
eca-rers2012/Problem04_label15_false-unreach-call.c 901    622    6720 9450   902    622    6590 9310   901    606    6440 9350   901    620    6600 9480  
eca-rers2012/Problem04_label17_false-unreach-call.c 901    628    6500 9550   901    618    6800 9480   901    631    6490 9550   901    629    6520 9340  
eca-rers2012/Problem04_label18_false-unreach-call.c 901    616    6910 8620   901    611    6840 9650   901    623    6450 10100   901    620    6570 8820  
eca-rers2012/Problem04_label19_false-unreach-call.c 903    617    6900 8690   902    615    6600 8780   902    632    6490 7560   901    636    6460 10200  
eca-rers2012/Problem04_label26_false-unreach-call.c 901    601    7160 10300   902    627    6790 10500   901    615    7080 9620   901    623    6650 9300  
eca-rers2012/Problem04_label27_false-unreach-call.c 901    626    6670 9180   901    626    6600 9950   901    626    6570 8760   902    630    6410 9430  
eca-rers2012/Problem04_label31_false-unreach-call.c 901    615    6600 10600   901    622    6710 10400   901    610    6720 9460   901    630    6460 9440  
eca-rers2012/Problem04_label32_false-unreach-call.c 901    615    6550 8760   901    614    6810 10700   901    616    7070 10500   901    623    6620 11100  
eca-rers2012/Problem04_label35_false-unreach-call.c 901    611    6650 10500   901    616    6730 9940   902    626    6700 9130   902    628    6700 10200  
eca-rers2012/Problem04_label36_false-unreach-call.c 901    638    6620 8320   901    608    6670 11100   901    615    6550 9090   901    613    6700 8690  
eca-rers2012/Problem04_label38_false-unreach-call.c 901    613    6640 9100   901    620    6470 8830   901    628    6450 9730   901    616    6850 9880  
eca-rers2012/Problem04_label39_false-unreach-call.c 901    615    6810 9650   901    614    6520 10300   902    618    6670 9690   901    632    6750 9300  
eca-rers2012/Problem04_label40_false-unreach-call.c 901    651    6530 10600   901    645    6890 9940   901    650    7170 9220   901    655    6580 9760  
eca-rers2012/Problem04_label45_false-unreach-call.c 902    606    6740 9520   901    630    6490 9900   901    610    6780 9500   902    638    6400 9650  
eca-rers2012/Problem04_label52_false-unreach-call.c 902    623    6620 10100   901    605    6860 9120   901    621    6540 8560   901    610    6850 8720  
eca-rers2012/Problem04_label55_false-unreach-call.c 901    617    7530 9540   902    636    6690 10200   901    651    6540 9250   901    654    6640 9620  
eca-rers2012/Problem04_label58_false-unreach-call.c 901    684    7280 9340   901    684    6640 11000   901    682    6440 10900   901    688    7180 9320  
eca-rers2012/Problem05_label00_false-unreach-call.c 902    396    9240 7240   901    424    9040 6860   919    416    9490 7300   916    420    9220 6970  
eca-rers2012/Problem05_label01_false-unreach-call.c 902    333    10800 7270   901    374    9720 7340   901    365    9890 6750   902    357    10900 7030  
eca-rers2012/Problem05_label11_false-unreach-call.c 902    354    10500 6520   902    337    10200 7330   901    362    10800 7510   901    366    10700 6600  
eca-rers2012/Problem05_label13_false-unreach-call.c 901    409    9540 6970   902    400    9370 7690   919    405    9210 7250   902    404    9220 6380  
eca-rers2012/Problem05_label15_false-unreach-call.c 901    409    9350 6340   901    430    9740 7860   903    413    9370 8680   902    400    9530 7380  
eca-rers2012/Problem05_label18_false-unreach-call.c 904    364    10300 7330   902    371    10700 6620   902    348    11000 6340   902    344    10900 7210  
eca-rers2012/Problem05_label24_false-unreach-call.c 903    408    9350 8060   902    412    9550 7730   921    414    9420 7530   903    409    9040 6780  
eca-rers2012/Problem05_label26_false-unreach-call.c 902    370    9970 6630   902    361    11000 6260   902    357    11000 7110   902    367    9800 6600  
eca-rers2012/Problem05_label30_false-unreach-call.c 902    413    9290 6470   902    429    9470 7200   901    407    9230 7640   903    400    9490 7300  
eca-rers2012/Problem05_label32_false-unreach-call.c 901    366    10000 6980   901    347    10500 7020   911    367    10600 7360   901    391    10100 7590  
eca-rers2012/Problem05_label33_false-unreach-call.c 901    402    9280 7270   915    418    9780 7790   901    404    9320 7170   901    418    8910 6980  
eca-rers2012/Problem05_label36_false-unreach-call.c 912    414    9240 7290   906    418    9300 8360   901    405    9540 6650   902    421    8950 7020  
eca-rers2012/Problem05_label37_false-unreach-call.c 902    334    10900 6520   903    363    10800 7540   901    358    10800 7250   906    335    11200 6640  
eca-rers2012/Problem05_label38_false-unreach-call.c 902    399    9480 7990   903    412    9140 7460   903    411    9400 7460   902    418    10200 8160  
eca-rers2012/Problem05_label39_false-unreach-call.c 901    365    10400 6700   902    364    10300 6680   901    353    10600 6740   902    369    10400 7090  
eca-rers2012/Problem05_label40_false-unreach-call.c 901    405    9270 6970   907    415    9320 6770   901    410    9260 8220   908    406    9530 6690  
eca-rers2012/Problem05_label41_false-unreach-call.c 902    331    11100 6120   902    359    10300 7440   901    356    10400 6650   902    361    10400 6070  
eca-rers2012/Problem05_label44_false-unreach-call.c 901    376    10100 7110   921    360    9880 6560   901    341    11000 6090   918    339    10900 6020  
eca-rers2012/Problem05_label47_false-unreach-call.c 902    400    9430 7400   904    418    9150 7840   902    406    9610 6990   901    401    9060 6760  
eca-rers2012/Problem05_label48_false-unreach-call.c 904    374    10400 8120   909    362    10500 6630   901    350    11100 7830   927    334    11000 7340  
eca-rers2012/Problem05_label51_false-unreach-call.c 903    377    9960 6880   901    349    9990 6930   901    360    9920 6350   902    356    11100 6430  
eca-rers2012/Problem05_label55_false-unreach-call.c 917    362    10300 7080   902    360    10400 6480   903    365    10600 6150   925    373    10900 7090  
eca-rers2012/Problem05_label57_false-unreach-call.c 904    363    10400 6780   902    360    11200 6800   901    367    10300 7330   903    366    10900 6820  
eca-rers2012/Problem05_label58_false-unreach-call.c 912    366    11100 8090   934    364    11000 7200   914    371    11100 7800   904    356    10500 6930  
eca-rers2012/Problem06_label00_false-unreach-call.c 901    394    11400 7960   902    393    12000 7960   923    395    11700 7020   903    390    11400 7190  
eca-rers2012/Problem06_label01_false-unreach-call.c 901    721    7050 10400   901    710    6650 10500   901    713    6700 10800   901    714    6720 9710  
eca-rers2012/Problem06_label02_false-unreach-call.c 901    715    6730 9480   901    708    6700 10200   902    702    6840 9900   902    706    6850 10700  
eca-rers2012/Problem06_label04_false-unreach-call.c 901    427    9800 7610   901    430    10000 8200   901    425    9900 7480   902    429    9760 7310  
eca-rers2012/Problem06_label05_false-unreach-call.c 902    421    9690 6520   901    411    9840 7990   909    433    9820 7440   902    392    10600 7970  
eca-rers2012/Problem06_label09_false-unreach-call.c 902    710    6640 10000   902    713    6730 11000   901    707    6750 10600   901    713    6760 12300  
eca-rers2012/Problem06_label10_false-unreach-call.c 904    388    12500 7150   903    391    12000 6590   902    387    11800 7050   901    385    12100 7640  
eca-rers2012/Problem06_label11_false-unreach-call.c 901    446    9770 6150   902    423    9840 7920   902    422    9820 6930   906    435    9630 7780  
eca-rers2012/Problem06_label12_false-unreach-call.c 901    383    11600 7100   901    377    12000 6860   902    389    11500 6590   904    381    12000 6330  
eca-rers2012/Problem06_label15_false-unreach-call.c 907    499    9900 9010   935    508    9760 8220   901    511    9970 9130   902    512    9900 8950  
eca-rers2012/Problem06_label20_false-unreach-call.c 901    512    9860 9050   901    502    10000 8580   902    513    9990 9300   901    522    9890 8470  
eca-rers2012/Problem06_label21_false-unreach-call.c 901    519    9850 8600   902    502    10000 9180   902    514    9640 7650   901    509    10000 9120  
eca-rers2012/Problem06_label24_false-unreach-call.c 922    428    9710 8330   901    421    9890 8030   906    431    9800 7390   902    429    9790 8270  
eca-rers2012/Problem06_label27_false-unreach-call.c 901    389    11400 7490   902    397    11900 8070   901    395    11600 7010   903    393    12200 7090  
eca-rers2012/Problem06_label29_false-unreach-call.c 901    496    9120 8420   901    509    9350 8210   901    519    8810 9400   902    512    9410 8360  
eca-rers2012/Problem06_label33_false-unreach-call.c 962    510    9750 9980   903    511    8750 8400   901    528    8760 9050   901    509    9650 8110  
eca-rers2012/Problem06_label36_false-unreach-call.c 902    708    6770 9330   902    711    6720 11300   901    716    6710 10200   901    705    6920 12000  
eca-rers2012/Problem06_label37_false-unreach-call.c 948    524    8770 10300   902    496    8840 8960   901    506    8940 7610   902    505    8850 8790  
eca-rers2012/Problem06_label38_false-unreach-call.c 906    503    8760 8730   901    506    9070 8170   902    503    8730 7690   901    517    9260 9300  
eca-rers2012/Problem06_label44_false-unreach-call.c 901    503    9980 8560   904    503    9920 9330   903    513    9580 8770   901    493    9980 9400  
eca-rers2012/Problem06_label47_false-unreach-call.c 902    493    9390 8130   903    520    9710 8740   901    489    10000 8490   924    500    9810 8220  
eca-rers2012/Problem06_label48_false-unreach-call.c 953    504    9760 7910   901    500    10200 9480   901    489    10100 7080   901    511    9740 9350  
eca-rers2012/Problem06_label56_false-unreach-call.c 902    499    10100 8620   928    496    10100 7260   920    486    9820 9010   901    518    9670 9010  
eca-rers2012/Problem06_label58_false-unreach-call.c 902    505    8810 8000   902    501    8860 8520   902    504    8710 8120   901    496    8870 8670  
eca-rers2012/Problem06_label59_false-unreach-call.c 901    703    6740 10100   902    705    6940 9240   902    713    6870 10000   902    706    6690 10900  
eca-rers2012/Problem07_label03_false-unreach-call.c 918    381    11900 6900   922    365    12100 7030   916    381    11900 7980   943    378    11800 8150  
eca-rers2012/Problem07_label05_false-unreach-call.c 926    369    12600 7060   935    386    11600 7820   916    375    11800 6520   925    374    11900 8040  
eca-rers2012/Problem07_label06_false-unreach-call.c 924    381    11800 8240   947    379    11700 7810   918    365    11500 7630   923    358    11800 7200  
eca-rers2012/Problem07_label07_false-unreach-call.c 922    360    11800 6880   928    379    11700 7060   926    373    11600 8340   923    364    12100 7610  
eca-rers2012/Problem07_label09_false-unreach-call.c 917    373    11900 7050   958    388    11900 7940   920    367    11600 6880   929    369    12400 7580  
eca-rers2012/Problem07_label11_false-unreach-call.c 917    377    11600 8120   925    367    12100 6980   920    372    12100 7000   953    376    11800 7170  
eca-rers2012/Problem07_label15_false-unreach-call.c 918    359    12200 7260   925    372    11700 6400   921    360    11500 7370   921    363    11900 6640  
eca-rers2012/Problem07_label18_false-unreach-call.c 915    376    11900 7370   918    377    11400 7030   947    378    11600 7050   956    369    11500 6670  
eca-rers2012/Problem07_label19_false-unreach-call.c 920    369    12100 7240   936    378    11500 6320   918    376    11500 6300   934    378    11600 6710  
eca-rers2012/Problem07_label20_false-unreach-call.c 944    365    11800 7430   929    368    11600 7080   955    381    11500 6520   951    355    11700 6170  
eca-rers2012/Problem07_label23_false-unreach-call.c 917    370    11600 7900   944    382    11900 6550   941    375    11700 7790   920    374    12100 6820  
eca-rers2012/Problem07_label30_false-unreach-call.c 937    380    11800 8170   916    365    11400 6760   948    379    11800 7150   929    373    11600 6920  
eca-rers2012/Problem07_label31_false-unreach-call.c 956    385    11700 7650   954    397    11500 7460   940    378    11800 7710   918    373    11500 7720  
eca-rers2012/Problem07_label35_false-unreach-call.c 963    378    12000 7920   940    378    11600 7900   940    385    11600 6800   923    370    12100 6940  
eca-rers2012/Problem07_label36_false-unreach-call.c 930    370    12600 7190   935    380    11600 8340   946    358    11700 7160   915    374    11600 6460  
eca-rers2012/Problem07_label37_false-unreach-call.c 919    364    11900 5690   947    383    11600 7170   925    379    11800 7100   941    363    11200 8180  
eca-rers2012/Problem07_label39_false-unreach-call.c 917    374    11500 7090   916    368    11600 7770   918    374    11900 6750   924    371    12700 6970  
eca-rers2012/Problem07_label40_false-unreach-call.c 942    382    11600 7570   937    366    12000 6980   956    391    11700 7730   925    373    12100 7590  
eca-rers2012/Problem07_label42_false-unreach-call.c 916    380    11900 6650   953    355    12500 7190   916    380    12100 6470   925    369    11600 7160  
eca-rers2012/Problem07_label44_false-unreach-call.c 957    386    11700 7150   922    368    12700 6200   925    378    11900 7530   923    369    11600 6970  
eca-rers2012/Problem07_label46_false-unreach-call.c 929    374    12300 7260   921    372    11700 6860   917    372    11600 7750   923    378    12000 7160  
eca-rers2012/Problem07_label47_false-unreach-call.c 915    386    11900 8010   932    366    11700 6110   918    375    11500 6790   922    381    11500 6660  
eca-rers2012/Problem07_label48_false-unreach-call.c 932    376    11600 7030   915    380    11600 6830   931    377    11600 7970   923    374    11800 7300  
eca-rers2012/Problem07_label58_false-unreach-call.c 924    354    12700 6690   918    378    11900 7220   957    364    11700 6850   921    381    11500 7260  
eca-rers2012/Problem08_label01_false-unreach-call.c 919    348    12400 6520   916    336    12500 6520   916    337    12400 7750   914    306    11900 5740  
eca-rers2012/Problem08_label02_false-unreach-call.c 915    339    12600 6380   905    306    11900 6100   914    336    12400 6450   915    337    12500 7210  
eca-rers2012/Problem08_label04_false-unreach-call.c 905    304    11900 5680   913    323    12000 6120   904    302    11900 6600   916    335    12500 7070  
eca-rers2012/Problem08_label05_false-unreach-call.c 938    308    11900 6600   920    306    11800 6870   918    347    12000 6630   916    335    12500 6930  
eca-rers2012/Problem08_label06_false-unreach-call.c 917    343    12100 7130   916    333    12600 5970   917    344    12500 7310   915    334    12500 7120  
eca-rers2012/Problem08_label07_false-unreach-call.c 915    334    12500 6360   907    306    11900 6930   915    334    12400 6750   903    303    11800 6470  
eca-rers2012/Problem08_label10_false-unreach-call.c 916    334    12200 5870   917    341    12500 6540   914    333    12500 7420   917    339    12100 6100  
eca-rers2012/Problem08_label13_false-unreach-call.c 915    335    12600 7260   915    339    12100 6450   919    349    12000 7160   918    346    12300 7930  
eca-rers2012/Problem08_label15_false-unreach-call.c 915    330    12500 6690   913    322    12000 6160   913    322    12400 6350   906    305    12000 5960  
eca-rers2012/Problem08_label24_false-unreach-call.c 916    342    12400 7100   917    341    12400 6750   915    324    12300 6340   916    334    11900 6860  
eca-rers2012/Problem08_label25_false-unreach-call.c 903    308    11800 6090   917    332    12200 6660   916    330    12400 6770   914    321    12400 6240  
eca-rers2012/Problem08_label26_false-unreach-call.c 918    342    12400 6990   917    341    12100 6820   917    339    12300 5910   917    342    12400 6180  
eca-rers2012/Problem08_label28_false-unreach-call.c 915    334    12400 6370   913    320    12100 6380   914    327    12300 6000   915    333    12500 7410  
eca-rers2012/Problem08_label29_false-unreach-call.c 915    331    12500 6840   914    322    12100 6980   916    334    11800 6560   915    341    12400 6410  
eca-rers2012/Problem08_label34_false-unreach-call.c 904    313    12700 6410   917    344    12200 6090   917    332    12100 7260   916    329    12400 6460  
eca-rers2012/Problem08_label37_false-unreach-call.c 916    331    12100 6370   918    330    11900 6420   914    326    12100 6590   918    343    12500 7070  
eca-rers2012/Problem08_label43_false-unreach-call.c 905    306    12000 5910   915    332    12400 6580   919    345    12100 6790   920    339    12000 6390  
eca-rers2012/Problem08_label46_false-unreach-call.c 915    337    12500 6190   935    337    11900 7670   915    334    12500 6810   913    324    12000 6520  
eca-rers2012/Problem08_label48_false-unreach-call.c 916    335    12000 6580   917    343    12300 6800   915    337    12400 6390   919    346    12200 6370  
eca-rers2012/Problem08_label49_false-unreach-call.c 916    329    12500 6800   915    344    12500 6880   916    341    12100 6540   916    343    12400 6420  
eca-rers2012/Problem08_label50_false-unreach-call.c 913    327    12000 6180   920    343    11800 6780   915    332    12100 5890   912    325    11900 6660  
eca-rers2012/Problem08_label51_false-unreach-call.c 912    306    11900 6120   915    341    12500 7850   914    333    12400 6800   915    326    12200 5890  
eca-rers2012/Problem08_label55_false-unreach-call.c 902    306    12000 6250   915    333    12300 6510   916    338    12500 5950   917    341    12100 6310  
eca-rers2012/Problem08_label59_false-unreach-call.c 904    311    11900 6530   914    330    12300 6420   916    332    12200 6540   903    314    11900 5940  
eca-rers2012/Problem09_label02_false-unreach-call.c 918    320    12700 6140   918    316    12900 6530   956    309    12300 6150   921    332    13500 5850  
eca-rers2012/Problem09_label03_false-unreach-call.c 943    307    12500 6880   932    302    12600 5930   916    302    12200 5610   968    303    12800 6210  
eca-rers2012/Problem09_label06_false-unreach-call.c 917    313    12800 6400   917    316    12600 6470   942    327    12800 6560   933    311    12500 7040  
eca-rers2012/Problem09_label08_false-unreach-call.c 916    299    12200 6000   921    308    12700 5880   921    333    12200 6470   916    298    12500 5910  
eca-rers2012/Problem09_label10_false-unreach-call.c 931    307    12800 6090   947    311    12500 6280   949    316    12600 6560   918    312    12300 6120  
eca-rers2012/Problem09_label11_false-unreach-call.c 921    322    12900 6680   952    307    12700 6240   966    305    12800 6540   929    306    12600 6420  
eca-rers2012/Problem09_label15_false-unreach-call.c 919    321    12200 6300   922    304    12200 5920   917    313    12700 5580   920    312    12100 6050  
eca-rers2012/Problem09_label19_false-unreach-call.c 921    316    12400 7030   918    307    12600 5950   915    309    12500 6570   917    304    12600 5900  
eca-rers2012/Problem09_label20_false-unreach-call.c 933    304    12800 6190   917    307    12200 6170   921    320    12900 7030   915    301    12900 6030  
eca-rers2012/Problem09_label32_false-unreach-call.c 926    306    12800 5660   916    308    12600 6620   915    304    12800 7010   961    312    12800 6410  
eca-rers2012/Problem09_label34_false-unreach-call.c 947    313    12600 6300   929    306    12500 6680   925    305    12500 6840   918    320    12100 6100  
eca-rers2012/Problem09_label35_false-unreach-call.c 968    332    13300 6580   952    309    12700 7360   920    314    12700 7080   920    317    12600 6420  
eca-rers2012/Problem09_label36_false-unreach-call.c 918    320    12300 6590   916    307    12200 5490   917    307    12500 6910   916    307    12300 6010  
eca-rers2012/Problem09_label38_false-unreach-call.c 920    337    12400 6730   919    313    12800 7040   917    308    12400 6820   943    308    12900 5640  
eca-rers2012/Problem09_label41_false-unreach-call.c 919    307    12100 6760   918    306    12500 6940   944    306    12900 6830   919    320    12000 6530  
eca-rers2012/Problem09_label44_false-unreach-call.c 941    309    12700 7130   921    301    12600 5910   919    311    12500 6590   947    309    12900 5130  
eca-rers2012/Problem09_label46_false-unreach-call.c 960    307    12800 6900   967    307    12200 6770   918    312    12300 6370   919    314    12300 5770  
eca-rers2012/Problem09_label47_false-unreach-call.c 920    309    12600 6510   968    306    12600 5830   920    316    12200 6720   915    301    12800 5660  
eca-rers2012/Problem09_label51_false-unreach-call.c 923    325    12400 7200   932    307    12700 6390   917    305    12700 6420   919    318    12100 6100  
eca-rers2012/Problem09_label53_false-unreach-call.c 921    323    12900 6920   919    335    13500 6830   929    335    13700 7420   947    310    12600 6780  
eca-rers2012/Problem09_label54_false-unreach-call.c 918    308    12200 5760   942    310    12600 6540   940    303    12900 7170   919    312    12400 5950  
eca-rers2012/Problem09_label56_false-unreach-call.c 920    306    12400 6290   917    306    12400 6780   961    312    12600 6860   917    308    12100 5930  
eca-rers2012/Problem09_label57_false-unreach-call.c 940    304    12500 6070   940    302    12200 5630   927    303    12300 5730   921    317    12900 6360  
eca-rers2012/Problem09_label59_false-unreach-call.c 942    308    12300 5680   960    312    12800 5950   947    313    12800 6260   919    327    12100 7570  
eca-rers2012/Problem10_label12_false-unreach-call.c 911    881    1810 13100   911    881    1880 12500   911    881    2070 12700   911    881    1800 12300  
eca-rers2012/Problem10_label15_false-unreach-call.c 911    881    1810 12700   911    881    1860 13400   911    881    2020 14800   911    880    1730 12000  
eca-rers2012/Problem10_label24_false-unreach-call.c 911    880    1820 12400   911    880    1810 15700   911    881    1840 11600   911    880    1900 12500  
eca-rers2012/Problem10_label26_false-unreach-call.c 911    880    1840 12400   911    880    1720 12600   911    880    1710 11200   911    881    1670 13400  
eca-rers2012/Problem10_label28_false-unreach-call.c 911    881    1730 13100   911    880    1850 11900   911    881    1900 13800   911    880    1610 12300  
eca-rers2012/Problem10_label29_false-unreach-call.c 911    880    1730 10700   911    881    1780 13900   911    881    1800 12500   911    880    1770 14600  
eca-rers2012/Problem10_label41_false-unreach-call.c 911    880    1770 12300   911    879    2120 12600   911    879    1740 14300   911    880    1560 12900  
eca-rers2012/Problem10_label42_false-unreach-call.c 911    881    1740 14200   911    880    1740 12900   911    880    1900 12000   911    880    1640 12400  
eca-rers2012/Problem10_label46_false-unreach-call.c 911    879    1840 13300   911    880    1730 12400   911    880    1970 12100   911    881    1650 13700  
eca-rers2012/Problem10_label47_false-unreach-call.c 911    880    1640 11700   911    880    1920 11800   911    879    1710 12800   911    879    2000 12800  
eca-rers2012/Problem10_label48_false-unreach-call.c 911    881    1710 13600   911    881    1750 12500   911    881    1660 10900   911    881    1740 13900  
eca-rers2012/Problem10_label50_false-unreach-call.c 911    881    1680 13700   911    882    1910 11300   911    881    1790 15400   911    881    1770 14000  
eca-rers2012/Problem10_label55_false-unreach-call.c 911    880    1710 12600   911    879    1790 14100   911    880    1710 12200   911    880    1770 14000  
eca-rers2012/Problem10_label57_false-unreach-call.c 911    881    1740 12300   911    881    1710 12600   911    881    1720 11500   911    881    2020 14200  
eca-rers2012/Problem10_label58_false-unreach-call.c 911    881    1690 12500   911    880    1790 13000   911    880    1760 11500   911    880    1820 12300  
eca-rers2012/Problem11_label00_false-unreach-call.c 911    882    1530 11500   911    883    1600 14200   911    883    1560 12500   911    883    1360 12500  
eca-rers2012/Problem11_label08_false-unreach-call.c 911    881    1560 12000   911    882    1510 14100   911    881    1490 11400   911    882    1360 13600  
eca-rers2012/Problem11_label14_false-unreach-call.c 911    880    1700 11300   911    881    1600 11700   911    881    1690 11800   911    882    1610 15300  
eca-rers2012/Problem11_label15_false-unreach-call.c 911    882    1570 12000   911    881    1540 12400   911    882    1400 11700   911    882    1490 11800  
eca-rers2012/Problem11_label20_false-unreach-call.c 911    882    1750 12100   911    882    1490 12300   911    882    1890 12900   911    884    1620 11500  
eca-rers2012/Problem11_label29_false-unreach-call.c 911    882    1570 13700   911    881    1580 11600   911    880    1610 12300   911    882    1560 11400  
eca-rers2012/Problem11_label31_false-unreach-call.c 911    883    1520 13800   911    884    1530 11600   911    882    1690 12300   911    883    1760 13400  
eca-rers2012/Problem11_label34_false-unreach-call.c 911    883    1590 11800   911    882    1450 11900   911    883    1440 9810   911    883    1720 12300  
eca-rers2012/Problem11_label36_false-unreach-call.c 911    882    1590 14000   911    883    1770 12200   911    882    2070 12900   911    882    1640 12700  
eca-rers2012/Problem11_label39_false-unreach-call.c 911    882    1660 11900   911    883    1620 12000   911    882    1670 10900   911    882    1560 13000  
eca-rers2012/Problem11_label42_false-unreach-call.c 911    882    1890 13300   911    882    1650 12800   911    881    1490 12300   911    880    1560 12000  
eca-rers2012/Problem11_label43_false-unreach-call.c 911    881    1500 12800   911    881    1840 11700   911    882    1520 11800   911    881    1720 12700  
eca-rers2012/Problem11_label49_false-unreach-call.c 911    881    1550 11100   911    881    1920 13400   911    882    1730 10900   911    881    1470 14400  
eca-rers2012/Problem11_label51_false-unreach-call.c 911    883    1630 12000   911    883    1800 12100   911    882    1400 13400   911    882    1520 13100  
eca-rers2012/Problem11_label58_false-unreach-call.c 911    882    1530 11900   911    882    1520 13900   911    881    1670 13200   911    881    1690 11900  
eca-rers2012/Problem12_label00_false-unreach-call.c 911    878    2260 12600   911    877    2130 13000   911    875    2350 12400   911    877    1400 12700  
eca-rers2012/Problem12_label03_false-unreach-call.c 911    878    1920 11000   911    879    2260 11800   911    875    1380 11500   911    879    2270 13000  
eca-rers2012/Problem12_label06_false-unreach-call.c 911    876    2220 11600   911    877    2090 13500   911    878    2460 12000   911    874    1360 13000  
eca-rers2012/Problem12_label07_false-unreach-call.c 911    879    2310 12200   911    879    2560 10800   911    878    2770 11800   911    877    1950 13800  
eca-rers2012/Problem12_label08_false-unreach-call.c 911    876    2390 12300   911    875    2110 11700   911    877    2760 14100   911    876    3210 13400  
eca-rers2012/Problem12_label10_false-unreach-call.c 911    877    2080 13400   911    876    2240 11900   911    877    2840 12200   911    877    2690 12000  
eca-rers2012/Problem12_label13_false-unreach-call.c 911    877    2380 14500   911    872    2440 12500   911    876    2420 11100   911    877    2300 11700  
eca-rers2012/Problem12_label19_false-unreach-call.c 911    877    1410 12600   911    875    2250 12500   911    879    1960 13600   911    879    2460 13900  
eca-rers2012/Problem12_label20_false-unreach-call.c 911    874    1980 11600   911    879    2430 12800   911    876    1410 11200   911    875    2180 13600  
eca-rers2012/Problem12_label21_false-unreach-call.c 911    877    2490 12100   911    876    2410 14800   911    879    2250 12300   911    879    2370 12900  
eca-rers2012/Problem12_label25_false-unreach-call.c 911    878    2240 12100   911    873    2430 13500   911    878    2220 11800   911    878    2950 11700  
eca-rers2012/Problem12_label28_false-unreach-call.c 911    876    2340 11400   911    877    2200 12200   911    877    1970 13700   911    878    2190 12100  
eca-rers2012/Problem12_label30_false-unreach-call.c 911    878    2890 13400   911    877    2450 12900   911    876    2240 14200   911    877    2430 11900  
eca-rers2012/Problem12_label34_false-unreach-call.c 911    879    1370 13400   911    879    2810 12100   911    879    2290 14200   911    877    1380 12400  
eca-rers2012/Problem12_label35_false-unreach-call.c 911    877    2290 13600   911    879    2220 14500   911    878    2210 14400   911    878    2310 11500  
eca-rers2012/Problem12_label37_false-unreach-call.c 911    878    2300 11700   911    877    1950 11300   911    876    2230 11100   911    877    1310 12600  
eca-rers2012/Problem12_label38_false-unreach-call.c 911    876    2340 13200   911    878    2160 11200   911    876    2800 10800   911    878    2330 13400  
eca-rers2012/Problem12_label39_false-unreach-call.c 911    878    2240 12300   911    877    2320 11900   911    876    2410 11600   911    873    2150 12500  
eca-rers2012/Problem12_label40_false-unreach-call.c 911    879    2250 14700   911    878    3100 12600   911    879    2260 11900   911    879    2060 11200  
eca-rers2012/Problem12_label42_false-unreach-call.c 911    870    2300 11700   911    874    1430 11600   911    872    2240 12600   911    878    2330 12300  
eca-rers2012/Problem12_label48_false-unreach-call.c 911    879    1860 13000   911    879    2160 14200   911    880    2490 12000   911    879    1360 12300  
eca-rers2012/Problem12_label50_false-unreach-call.c 911    876    2300 13600   911    879    2040 11700   911    872    2280 13700   911    879    2150 12400  
eca-rers2012/Problem12_label51_false-unreach-call.c 911    876    1390 11300   911    878    1410 13200   911    879    2360 14100   911    877    3500 12300  
eca-rers2012/Problem12_label52_false-unreach-call.c 911    877    2530 12200   911    875    2320 11800   911    878    2260 12300   911    876    2320 13600  
eca-rers2012/Problem12_label55_false-unreach-call.c 911    879    2360 12600   911    878    2140 11200   911    879    3090 10700   911    879    3160 11900  
eca-rers2012/Problem13_label04_false-unreach-call.c 911    880    1540 13300   911    881    1510 13000   911    880    1450 12000   911    880    1550 14000  
eca-rers2012/Problem13_label06_false-unreach-call.c 911    881    2710 12000   911    879    1470 13100   911    880    1420 11000   911    880    1390 11900  
eca-rers2012/Problem13_label07_false-unreach-call.c 911    879    1530 11200   911    880    1630 12600   911    880    1480 15100   911    880    1730 13100  
eca-rers2012/Problem13_label11_false-unreach-call.c 911    880    1610 12400   911    879    1530 11600   911    879    1570 12100   911    880    1420 13800  
eca-rers2012/Problem13_label12_false-unreach-call.c 911    882    1400 12200   911    882    1390 12800   911    881    1480 12300   911    882    1480 12400  
eca-rers2012/Problem13_label16_false-unreach-call.c 911    879    1560 12900   911    880    1390 11200   911    879    1480 13000   911    879    1560 12600  
eca-rers2012/Problem13_label19_false-unreach-call.c 911    880    1370 13100   911    881    1510 13200   911    882    1340 11600   911    880    1500 11300  
eca-rers2012/Problem13_label21_false-unreach-call.c 911    880    1420 13600   911    880    1610 13300   911    881    1430 13000   911    880    1510 12000  
eca-rers2012/Problem13_label23_false-unreach-call.c 911    882    1560 12700   911    881    1500 13100   911    881    1490 13300   911    880    1540 13500  
eca-rers2012/Problem13_label24_false-unreach-call.c 911    880    1450 11700   911    880    1520 11900   911    879    1450 11700   911    880    1320 13600  
eca-rers2012/Problem13_label25_false-unreach-call.c 911    880    1440 12400   911    879    1450 14200   911    880    1430 11200   911    881    1690 13500  
eca-rers2012/Problem13_label28_false-unreach-call.c 911    878    1500 12700   911    881    1570 12300   911    881    1450 13400   911    880    1380 11900  
eca-rers2012/Problem13_label29_false-unreach-call.c 911    881    1410 12300   911    881    1540 12600   911    881    1530 14300   911    878    1530 11700  
eca-rers2012/Problem13_label30_false-unreach-call.c 911    881    1460 13900   911    880    1410 11500   911    882    1270 11700   911    880    1490 12000  
eca-rers2012/Problem13_label32_false-unreach-call.c 911    882    1430 11900   911    881    1500 12900   911    881    1510 13200   911    881    1430 12400  
eca-rers2012/Problem13_label35_false-unreach-call.c 911    882    1410 13200   911    881    1510 13000