Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 0 .093 22 .78 0 .55 43 0 .023 4.9 0 .84 47 0 .0012 .30 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 31     15000 440    0 .56 44 0 .019 4.9 0 1.0  50 0 .0013 .33 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 33     15000 490    0 .53 41 0 .022 4.8 0 1.0  50 0 .0015 .30 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 33     15000 470    0 .58 42 0 .019 4.9 0 1.0  49 0 .0014 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 33     15000 470    0 .63 42 0 .020 4.8 0 .84 49 0 .0013 .27 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 290     15000 2000    0 .39 43 0 .018 4.8 0 .92 47 0 .0015 .28 - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 31     15000 360    0 .58 43 0 .022 4.8 0 1.0  49 0 .0015 .27 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 31     15000 400    0 .54 43 0 .024 4.8 0 .96 49 0 .0013 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 31     15000 430    0 .54 41 0 .019 4.9 0 .91 49 0 .0016 .26 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 31     15000 460    0 .54 45 0 .022 4.8 0 1.0  49 0 .0013 .30 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 31     15000 390    0 .56 43 0 .019 4.8 0 .83 49 0 .0011 .35 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 31     15000 380    0 .51 41 0 .019 4.9 0 .91 49 0 .0014 .30 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 31     15000 420    0 .56 42 0 .020 4.9 0 1.0  52 0 .0013 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 31     15000 390    0 .54 42 0 .023 4.8 0 .89 49 0 .0011 .33 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 31     15000 490    0 .54 41 0 .019 4.9 0 .92 49 0 .0011 .30 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 33     15000 440    0 .57 43 0 .020 4.8 0 1.2  51 0 .0018 .29 - -
array-examples/standard_init1_false-unreach-call_ground.i -32 32     12000 400    0 92    1900 0 96     940   0 .96 51 0 .068  9.0  - -
array-examples/standard_init2_false-unreach-call_ground.i 0 31     15000 410    0 .52 43 0 .020 4.9 0 .92 49 0 .0015 .26 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 31     15000 400    0 .52 43 0 .019 4.9 0 .90 49 0 .0015 .30 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 31     15000 390    0 .40 41 0 .022 4.8 0 1.0  49 0 .0017 .30 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 31     15000 460    0 .56 41 0 .019 5.0 0 .88 49 0 .0015 .30 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 31     15000 410    0 .52 41 0 .019 4.8 0 .82 49 0 .0012 .32 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 31     15000 470    0 .52 41 0 .025 4.8 0 .96 49 0 .0013 .29 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 31     15000 470    0 .54 43 0 .021 4.8 0 .82 47 0 .0013 .30 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 33     15000 480    0 .53 41 0 .018 4.9 0 .81 49 0 .0013 .26 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 320     15000 2200    0 .54 41 0 .019 4.8 0 .83 49 0 .0012 .35 - -
array-examples/standard_partition_false-unreach-call_ground.i 0 31     15000 380    0 .58 41 0 .020 4.8 0 .89 49 0 .0012 .30 - -
array-examples/standard_running_false-unreach-call.i 0 31     15000 370    0 .58 43 0 .020 4.8 0 .90 49 0 .0011 .34 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 .11  22 .62 - - - - 0 .63 43 0 .026 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 .078 22 .71 - - - - 0 .67 41 0 .019 4.9
array-examples/relax_true-unreach-call.i 0 .18  26 1.6  - - - - 0 .55 42 0 .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 180     15000 1400    - - - - 0 .53 41 0 .019 5.0
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 34     15000 390    - - - - 0 .54 44 0 .022 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 17     5700 190    - - - - 2 6.9  510 2 7.5   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 270     15000 2100    - - - - 0 .57 43 0 .019 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i 0 .074 22 .82 - - - - 0 .65 43 0 .018 5.0
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 31     15000 370    - - - - 0 .61 44 0 .019 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 33     15000 520    - - - - 0 .69 41 0 .032 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i 0 32     15000 450    - - - - 0 .65 43 0 .019 4.8
array-examples/standard_compare_true-unreach-call_ground.i 0 150     15000 1300    - - - - 0 .56 44 0 .035 4.9
array-examples/standard_copy1_true-unreach-call_ground.i 0 33     15000 440    - - - - 0 .70 42 0 .024 4.8
array-examples/standard_copy2_true-unreach-call_ground.i 0 34     15000 430    - - - - 0 .58 44 0 .024 4.9
array-examples/standard_copy3_true-unreach-call_ground.i 0 33     15000 430    - - - - 0 .57 41 0 .018 4.8
array-examples/standard_copy4_true-unreach-call_ground.i 0 33     15000 470    - - - - 0 .58 41 0 .044 4.8
array-examples/standard_copy5_true-unreach-call_ground.i 0 33     15000 440    - - - - 0 .58 43 0 .019 4.9
array-examples/standard_copy6_true-unreach-call_ground.i 0 33     15000 480    - - - - 0 .55 41 0 .020 4.9
array-examples/standard_copy7_true-unreach-call_ground.i 0 33     15000 450    - - - - 0 .54 43 0 .018 4.8
array-examples/standard_copy8_true-unreach-call_ground.i 0 33     15000 520    - - - - 0 .51 44 0 .024 5.0
array-examples/standard_copy9_true-unreach-call_ground.i 0 33     15000 390    - - - - 0 .69 43 0 .020 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 32     15000 500    - - - - 0 .70 41 0 .018 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 32     15000 420    - - - - 0 .57 41 0 .023 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 32     15000 460    - - - - 0 .57 42 0 .020 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i 0 32     15000 390    - - - - 0 .54 44 0 .019 4.9
array-examples/standard_find_true-unreach-call_ground.i 2 40     15000 500    - - - - 0 900    4700 0 960     4700  
array-examples/standard_init1_true-unreach-call_ground.i 2 32     12000 390    - - - - 0 900    4900 0 960     2000  
array-examples/standard_init2_true-unreach-call_ground.i 0 31     15000 380    - - - - 0 .55 41 0 .024 4.8
array-examples/standard_init3_true-unreach-call_ground.i 0 31     15000 410    - - - - 0 .70 44 0 .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i 0 31     15000 470    - - - - 0 .56 45 0 .021 5.0
array-examples/standard_init5_true-unreach-call_ground.i 0 31     15000 400    - - - - 0 .60 41 0 .050 4.9
array-examples/standard_init6_true-unreach-call_ground.i 0 31     15000 400    - - - - 0 .56 41 0 .025 4.9
array-examples/standard_init7_true-unreach-call_ground.i 0 31     15000 490    - - - - 0 .53 42 0 .020 5.0
array-examples/standard_init8_true-unreach-call_ground.i 0 31     15000 440    - - - - 0 .39 43 0 .018 4.9
array-examples/standard_init9_true-unreach-call_ground.i 0 31     15000 450    - - - - 0 .53 43 0 .023 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 260     15000 1900    - - - - 0 .68 41 0 .024 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i 0 310     15000 2100    - - - - 0 .71 43 0 .024 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i 0 34     15000 420    - - - - 0 .54 44 0 .020 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i 0 31     15000 400    - - - - 0 .72 44 0 .018 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i 0 29     15000 370    - - - - 0 .69 44 0 .018 5.0
array-examples/standard_partition_true-unreach-call_ground.i 0 31     15000 400    - - - - 0 .57 43 0 .018 4.8
array-examples/standard_password_true-unreach-call_ground.i 0 150     15000 1400    - - - - 0 .56 44 0 .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i 0 33     15000 510    - - - - 0 .67 41 0 .019 4.9
array-examples/standard_running_true-unreach-call.i 0 31     15000 510    - - - - 0 .56 41 0 .048 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 110     15000 880    - - - - 0 .53 44 0 .048 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i 0 34     15000 420    - - - - 0 .61 43 0 .020 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i -16 75     11000 870    - - - - 0 900    2300 2 5.6   290  
array-examples/standard_strcpy_original_true-unreach-call.i 0 33     15000 410    - - - - 0 .55 43 0 .018 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i 0 33     15000 420    - - - - 0 .66 43 0 .018 4.9
array-examples/standard_two_index_01_true-unreach-call.i 0 250     15000 1600    - - - - 0 .59 43 0 .018 4.9
array-examples/standard_two_index_02_true-unreach-call.i 0 34     15000 440    - - - - 0 .60 44 0 .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i 0 240     15000 1800    - - - - 0 .68 41 0 .035 4.8
array-examples/standard_two_index_04_true-unreach-call.i 0 33     15000 480    - - - - 0 .69 43 0 .018 4.8
array-examples/standard_two_index_05_true-unreach-call.i 0 34     15000 430    - - - - 0 .64 43 0 .023 5.0
array-examples/standard_two_index_06_true-unreach-call.i 0 240     15000 1700    - - - - 0 .58 44 0 .021 4.9
array-examples/standard_two_index_07_true-unreach-call.i 0 34     15000 420    - - - - 0 .69 44 0 .024 4.8
array-examples/standard_two_index_08_true-unreach-call.i 0 34     15000 420    - - - - 0 .62 41 0 .019 5.0
array-examples/standard_two_index_09_true-unreach-call.i 0 34     15000 430    - - - - 0 .66 43 0 .048 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 170     15000 1200    - - - - 0 .69 46 0 .020 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 32     15000 400    - - - - 0 .67 41 0 .019 4.9
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 32     15000 380    0 .51 41 0 .018 4.8 0 .83 48 0 .0016 .26 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 34     15000 500    0 .58 43 0 .019 5.0 0 1.0  49 0 .0011 .35 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 26     15000 330    0 .54 41 0 .022 4.9 0 .87 50 0 .0016 .26 - -
array-industry-pattern/array_range_init_false-unreach-call.i -32 38     15000 460    0 92    2500 0 97     4800   0 .95 51 0 .066  9.0  - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 26     15000 340    0 .54 44 0 .018 4.8 0 .93 51 0 .0013 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 .079 23 .65 0 .60 43 0 .025 4.8 0 1.1  49 0 .0016 .28 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 29     15000 370    - - - - 0 .54 43 0 .018 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 30     15000 370    - - - - 0 .63 46 0 .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 36     13000 390    - - - - 0 900    3800 0 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 110     7000 820    - - - - 0 .54 43 0 .019 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 .16  24 1.6  - - - - 0 .57 43 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 100     7000 830    - - - - 0 .63 43 0 .024 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 34     15000 440    - - - - 0 .53 41 0 .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 26     15000 320    - - - - 0 .64 45 0 .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 130     11000 1200    - - - - 0 .62 43 0 .024 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 2 29     12000 360    - - - - 0 900    4000 0 960     5900  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 900     14000 3700    - - - - 0 .64 42 0 .019 4.8
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 0 .089 22 .64 0 .53 43 0 .024 4.8 0 1.0  49 0 .0014 .31 - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 0 .11  22 .64 0 .54 41 0 .025 4.8 0 .99 49 0 .0030 .26 - -
reducercommutativity/rangesum20_false-unreach-call.i 0 .092 22 .76 0 .55 42 0 .017 4.8 0 .87 49 0 .0015 .27 - -
reducercommutativity/rangesum40_false-unreach-call.i 0 .094 22 .82 0 .55 44 0 .023 4.9 0 .90 49 0 .0013 .27 - -
reducercommutativity/rangesum60_false-unreach-call.i 0 .11  23 .63 0 .57 44 0 .019 4.9 0 .81 48 0 .0014 .28 - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 .097 22 .63 0 .54 43 0 .022 4.9 0 .86 49 0 .0017 .27 - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 110     360 1300    - - - - 0 860    7000 0 960     4600  
reducercommutativity/avg10_true-unreach-call_true-termination.i 0 900     710 12000    - - - - 0 .57 42 0 .019 4.8
reducercommutativity/avg20_true-unreach-call.i 0 900     810 12000    - - - - 0 .53 44 0 .021 5.0
reducercommutativity/avg40_true-unreach-call.i 0 900     890 7700    - - - - 0 .53 43 0 .019 4.9
reducercommutativity/avg60_true-unreach-call.i 0 900     1000 8800    - - - - 0 .68 43 0 .019 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i 0 900     1600 7200    - - - - 0 .61 46 0 .020 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i 2 6.0   89 85    - - - - 0 900    3400 0 960     4100  
reducercommutativity/max10_true-unreach-call_true-termination.i 2 300     480 3800    - - - - 0 900    3400 0 960     3400  
reducercommutativity/max20_true-unreach-call.i 0 900     1000 11000    - - - - 0 .54 41 0 .019 4.9
reducercommutativity/max40_true-unreach-call.i 0 900     1400 9000    - - - - 0 .52 41 0 .031 4.8
reducercommutativity/max60_true-unreach-call.i 0 900     1900 5600    - - - - 0 .54 44 0 .020 4.9
reducercommutativity/max_true-unreach-call_true-termination.i 0 900     2500 3700    - - - - 0 .61 44 0 .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 2.1   69 24    - - - - 0 900    3700 0 960     1700  
reducercommutativity/sep10_true-unreach-call.i 2 3.3   100 41    - - - - 0 900    3400 0 920     7000  
reducercommutativity/sep20_true-unreach-call.i 2 12     280 120    - - - - 0 900    3000 0 910     7000  
reducercommutativity/sep40_true-unreach-call.i 0 900     1400 9300    - - - - 0 .54 44 0 .020 5.0
reducercommutativity/sep60_true-unreach-call.i 0 900     2200 9400    - - - - 0 .54 41 0 .020 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 0 900     10000 7000    - - - - 0 .52 41 0 .018 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 20     170 270    - - - - 0 900    5200 2 380     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i 0 900     760 11000    - - - - 0 .60 44 0 .020 4.9
reducercommutativity/sum20_true-unreach-call.i 0 900     720 8100    - - - - 0 .54 41 0 .018 4.9
reducercommutativity/sum40_true-unreach-call.i 0 900     860 8600    - - - - 0 .55 43 0 .021 4.8
reducercommutativity/sum60_true-unreach-call.i 0 900     1000 6100    - - - - 0 .67 44 0 .020 5.0
reducercommutativity/sum_true-unreach-call_true-termination.i 0 900     1900 8000    - - - - 0 .57 43 0 .020 4.8
array-tiling/mlceu_false-unreach-call.i 0 670     15000 3200    0 .53 41 0 .018 4.8 0 1.1  49 0 .0012 .34 - -
array-tiling/skippedu_false-unreach-call.i 1 .33  38 3.4  1 3.1  260 1 15     300   0 2.9  190 -32 .77   18    - -
array-tiling/mbpr2_true-unreach-call.i 0 510     15000 2500    - - - - 0 .53 41 0 .021 4.8
array-tiling/mbpr3_true-unreach-call.i 0 410     15000 2000    - - - - 0 .60 41 0 .022 4.8
array-tiling/mbpr4_true-unreach-call.i 0 440     15000 2600    - - - - 0 .54 41 0 .019 5.0
array-tiling/mbpr5_true-unreach-call.i 0 900     12000 4400    - - - - 0 .75 42 0 .019 4.8
array-tiling/nr2_true-unreach-call.i 0 680     15000 3300    - - - - 0 .67 41 0 .017 4.8
array-tiling/nr3_true-unreach-call.i 0 490     15000 4500    - - - - 0 .59 41 0 .019 4.9
array-tiling/nr4_true-unreach-call.i 0 400     15000 2100    - - - - 0 .55 41 0 .019 4.9
array-tiling/nr5_true-unreach-call.i 0 590     15000 4100    - - - - 0 .53 44 0 .019 5.0
array-tiling/pnr2_true-unreach-call.i 0 560     15000 3500    - - - - 0 .51 44 0 .017 4.9
array-tiling/pnr3_true-unreach-call.i 0 580     15000 2700    - - - - 0 .57 42 0 .019 4.8
array-tiling/pnr4_true-unreach-call.i 0 530     15000 1800    -