Tool CPAchecker 1.6.1-svn 26758M 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] 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:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.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 2.5 260 25 0 .56 44 0 .020 4.9 0 .89 49 0 .0012 .26 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 2.5 260 22 0 .56 45 0 .019 4.9 0 .85 49 0 .0013 .26 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 2.5 270 23 0 .55 43 0 .017 5.0 0 .88 49 0 .0013 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 2.6 260 22 0 .53 41 0 .019 4.8 0 .84 49 0 .0013 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 2.5 260 21 0 .59 42 0 .020 4.9 0 .88 49 0 .0013 .27 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 2.5 270 21 0 .53 41 0 .019 4.8 0 .83 49 0 .0013 .26 - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 2.5 270 19 0 .58 42 0 .019 4.9 0 .88 49 0 .0013 .26 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 2.5 270 22 0 .57 43 0 .021 4.8 0 .66 50 0 .0014 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 2.6 270 26 0 .58 44 0 .020 5.0 0 .90 49 0 .0014 .27 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 2.5 270 21 0 .59 44 0 .024 4.9 0 .85 49 0 .0013 .27 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 2.7 270 24 0 .57 41 0 .020 4.9 0 .85 50 0 .0013 .26 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 2.6 270 24 0 .56 41 0 .018 4.9 0 .84 49 0 .0012 .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 2.6 260 23 0 .52 41 0 .018 4.9 0 .85 47 0 .0013 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 2.6 260 25 0 .60 44 0 .019 4.8 0 .88 49 0 .0016 .26 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 2.5 260 26 0 .59 44 0 .020 4.9 0 .85 49 0 .0017 .30 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 2.7 270 26 0 .54 43 0 .020 4.9 0 .87 50 0 .0016 .27 - -
array-examples/standard_init1_false-unreach-call_ground.i 0 2.5 260 21 0 .54 41 0 .024 4.8 0 .90 49 0 .0015 .26 - -
array-examples/standard_init2_false-unreach-call_ground.i 0 2.6 270 25 0 .58 43 0 .019 4.9 0 .87 49 0 .0014 .26 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 2.5 270 23 0 .55 43 0 .020 4.9 0 .87 49 0 .0011 .33 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 2.5 270 23 0 .52 41 0 .018 5.0 0 .88 49 0 .0013 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 2.4 270 22 0 .57 46 0 .020 4.9 0 .83 49 0 .0013 .27 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 2.6 260 25 0 .55 43 0 .019 4.8 0 .82 49 0 .0012 .26 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 2.7 270 21 0 .55 43 0 .020 4.8 0 .86 49 0 .0014 .28 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 2.5 270 22 0 .54 41 0 .020 5.0 0 .87 50 0 .0014 .28 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 2.5 270 22 0 .54 43 0 .019 4.9 0 .89 49 0 .0013 .28 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 2.6 270 24 0 .57 42 0 .019 4.9 0 .85 49 0 .0013 .29 - -
array-examples/standard_partition_false-unreach-call_ground.i 0 2.5 270 21 0 .65 43 0 .018 4.9 0 .81 50 0 .0013 .30 - -
array-examples/standard_running_false-unreach-call.i 0 2.5 270 21 0 .55 43 0 .020 4.8 0 .85 49 0 .0013 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 2.6 260 26 - - - - 0 .67 45 0 .021 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 2.6 270 22 - - - - 0 .64 41 0 .019 4.8
array-examples/relax_true-unreach-call.i 0 5.7 310 48 - - - - 0 .55 43 0 .024 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 2.6 260 25 - - - - 0 .53 43 0 .018 4.8
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900   4100 11000 - - - - 0 .53 41 0 .018 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 0 2.5 260 21 - - - - 0 .66 44 0 .019 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .55 41 0 .018 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 2.7 270 25 - - - - 2 3.7  260 2 7.2   290  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 2.6 260 23 - - - - 0 .68 43 0 .022 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 2.5 270 24 - - - - 0 .56 44 0 .018 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .53 41 0 .024 4.8
array-examples/standard_compare_true-unreach-call_ground.i 0 2.5 260 23 - - - - 0 .67 43 0 .023 4.9
array-examples/standard_copy1_true-unreach-call_ground.i 0 2.5 260 23 - - - - 0 .52 43 0 .022 4.8
array-examples/standard_copy2_true-unreach-call_ground.i 0 2.5 260 25 - - - - 0 .70 44 0 .017 4.9
array-examples/standard_copy3_true-unreach-call_ground.i 0 2.5 260 24 - - - - 0 .55 45 0 .020 5.0
array-examples/standard_copy4_true-unreach-call_ground.i 0 2.6 260 23 - - - - 0 .52 41 0 .020 5.0
array-examples/standard_copy5_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .54 43 0 .023 4.8
array-examples/standard_copy6_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .69 41 0 .020 4.8
array-examples/standard_copy7_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .58 43 0 .018 5.0
array-examples/standard_copy8_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .66 44 0 .021 4.9
array-examples/standard_copy9_true-unreach-call_ground.i 0 2.5 270 23 - - - - 0 .54 45 0 .018 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 2.5 270 23 - - - - 0 .54 41 0 .019 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .57 41 0 .019 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 2.6 270 21 - - - - 0 .65 45 0 .023 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i 0 2.6 270 25 - - - - 0 .53 43 0 .018 4.8
array-examples/standard_find_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .70 44 0 .021 4.8
array-examples/standard_init1_true-unreach-call_ground.i 0 2.5 260 25 - - - - 0 .52 42 0 .018 4.8
array-examples/standard_init2_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .61 44 0 .021 4.9
array-examples/standard_init3_true-unreach-call_ground.i 0 2.6 260 27 - - - - 0 .59 42 0 .020 4.8
array-examples/standard_init4_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .52 44 0 .018 4.9
array-examples/standard_init5_true-unreach-call_ground.i 0 2.5 260 23 - - - - 0 .54 43 0 .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i 0 2.5 260 25 - - - - 0 .54 43 0 .025 4.8
array-examples/standard_init7_true-unreach-call_ground.i 0 2.6 270 26 - - - - 0 .54 41 0 .018 4.9
array-examples/standard_init8_true-unreach-call_ground.i 0 2.7 270 24 - - - - 0 .52 44 0 .019 5.0
array-examples/standard_init9_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .57 44 0 .019 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .65 43 0 .019 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i 0 2.4 260 21 - - - - 0 .56 41 0 .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i 0 2.4 260 21 - - - - 0 .53 41 0 .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .89 43 0 .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .72 43 0 .026 5.0
array-examples/standard_partition_true-unreach-call_ground.i 0 2.5 270 23 - - - - 0 .67 41 0 .019 4.8
array-examples/standard_password_true-unreach-call_ground.i 0 2.5 260 21 - - - - 0 .54 43 0 .021 5.0
array-examples/standard_reverse_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .67 41 0 .018 5.0
array-examples/standard_running_true-unreach-call.i 0 2.5 270 22 - - - - 0 .66 44 0 .023 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 2.5 270 26 - - - - 0 .65 43 0 .024 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i 0 2.5 270 24 - - - - 0 .54 43 0 .019 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .56 42 0 .023 4.8
array-examples/standard_strcpy_original_true-unreach-call.i 0 2.7 270 22 - - - - 0 .57 43 0 .025 5.0
array-examples/standard_strcpy_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .54 43 0 .023 4.8
array-examples/standard_two_index_01_true-unreach-call.i 0 2.5 260 23 - - - - 0 .54 43 0 .024 5.0
array-examples/standard_two_index_02_true-unreach-call.i 0 2.5 270 25 - - - - 0 .70 43 0 .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i 0 2.5 270 23 - - - - 0 .54 41 0 .023 4.8
array-examples/standard_two_index_04_true-unreach-call.i 0 2.4 270 24 - - - - 0 .72 41 0 .021 4.9
array-examples/standard_two_index_05_true-unreach-call.i 0 2.6 270 24 - - - - 0 .55 42 0 .019 4.8
array-examples/standard_two_index_06_true-unreach-call.i 0 2.5 260 23 - - - - 0 .74 43 0 .025 4.8
array-examples/standard_two_index_07_true-unreach-call.i 0 2.5 260 24 - - - - 0 .54 43 0 .023 4.8
array-examples/standard_two_index_08_true-unreach-call.i 0 2.5 270 21 - - - - 0 .53 41 0 .023 4.9
array-examples/standard_two_index_09_true-unreach-call.i 0 2.6 270 25 - - - - 0 .69 41 0 .018 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 2.5 270 22 - - - - 0 .53 42 0 .024 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 2.5 260 22 - - - - 0 .54 41 0 .022 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 2.7 270 24 0 .58 42 0 .019 4.9 0 .86 48 0 .0012 .33 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 900   4200 11000 0 .57 43 0 .019 4.8 0 .80 48 0 .0016 .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 2.5 270 22 0 .55 42 0 .019 4.8 0 .83 47 0 .0011 .29 - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 2.5 260 22 0 .58 42 0 .019 5.0 0 .81 49 0 .0011 .29 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 2.5 270 23 0 .54 41 0 .018 5.0 0 .85 49 0 .0013 .28 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   6400 11000 0 .56 41 0 .019 4.9 0 .88 50 0 .0013 .26 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 2.7 260 23 - - - - 0 .52 41 0 .026 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 2.7 270 22 - - - - 0 .62 41 0 .020 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 900   4200 9900 - - - - 0 .55 44 0 .022 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900   4200 9300 - - - - 0 .52 42 0 .019 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 910   11000 4400 - - - - 0 .61 41 0 .024 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900   4200 9200 - - - - 0 .52 42 0 .021 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900   5100 11000 - - - - 0 .69 41 0 .018 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 900   3800 10000 - - - - 0 .67 44 0 .026 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 900   3900 10000 - - - - 0 .55 43 0 .018 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900   7800 6400 - - - - 0 .55 41 0 .024 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i -16 3.9 290 33 - - - - 0 900    2600 2 4.8   230  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 6.5 410 60 -32 4.5  260 -32 5.1   240   0 3.2  220 1 .60   19    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 7.7 530 58 -32 4.4  290 -32 5.0   230   0 3.6  230 1 .59   20    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 13   740 120 -32 5.2  270 -32 5.3   260   0 4.0  220 1 .65   21    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 92   3700 900 -32 5.6  270 -32 5.6   250   0 3.8  210 1 .65   23    - -
reducercommutativity/rangesum60_false-unreach-call.i 1 210   4600 2200 -32 6.2  270 -32 5.6   260   0 4.1  210 1 .67   26    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 15   650 110 0 92    1900 -32 5.0   230   0 3.3  190 -32 .61   19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i -16 5.5 380 52 - - - - 2 3.4  260 0 960     5400  
reducercommutativity/avg10_true-unreach-call_true-termination.i -16 7.4 450 57 - - - - 2 4.0  260 0 60     7000  
reducercommutativity/avg20_true-unreach-call.i -16 10   680 89 - - - - 2 4.7  270 0 58     7000  
reducercommutativity/avg40_true-unreach-call.i -16 180   3200 1500 - - - - 2 6.0  270 0 67     7000  
reducercommutativity/avg60_true-unreach-call.i -16 630   4600 7000 - - - - 2 5.6  270 0 74     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i -16 5.8 410 50 - - - - 0 900    2300 2 6.3   230  
reducercommutativity/max05_true-unreach-call_true-termination.i -16 5.6 300 51 - - - - 2 4.8  260 0 61     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i -16 7.2 430 64 - - - - 2 5.3  270 0 68     7000  
reducercommutativity/max20_true-unreach-call.i -16 11   540 93 - - - - 2 4.6  270 0 57     7000  
reducercommutativity/max40_true-unreach-call.i -16 370   3000 4800 - - - - 2 5.8  270 0 68     7000  
reducercommutativity/max60_true-unreach-call.i 0 900   4000 12000 - - - - 0 .67 43 0 .023 4.8
reducercommutativity/max_true-unreach-call_true-termination.i -16 9.2 470 75 - - - - 0 900    2500 2 5.0   230  
reducercommutativity/sep05_true-unreach-call_true-termination.i -16 6.5 360 56 - - - - 2 4.1  260 0 370     7000  
reducercommutativity/sep10_true-unreach-call.i -16 14   660 100 - - - - 2 5.4  270 0 74     7000  
reducercommutativity/sep20_true-unreach-call.i -16 63   3200 670 - - - - 2 6.0  270 0 55     7000  
reducercommutativity/sep40_true-unreach-call.i -16 850   9200 7100 - - - - 2 5.8  270 0 66     7000  
reducercommutativity/sep60_true-unreach-call.i 0 910   9700 7300 - - - - 0 .62 41 0 .019 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i -16 880   6700 12000 - - - - 0 900    2800 2 6.2   230  
reducercommutativity/sum05_true-unreach-call_true-termination.i -16 5.2 320 37 - - - - 2 4.6  260 0 960     4900  
reducercommutativity/sum10_true-unreach-call_true-termination.i -16 7.3 430 59 - - - - 2 3.9  260 0 56     7000  
reducercommutativity/sum20_true-unreach-call.i -16 11   620 110 - - - - 2 5.2  270 0 56     7000  
reducercommutativity/sum40_true-unreach-call.i -16 160   3500 1800 - - - - 2 5.5  270 0 66     7000  
reducercommutativity/sum60_true-unreach-call.i -16 630   4500 7200 - - - - 2 5.6  270 0 68     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i -16 4.9 310 41 - - - - 0 900    2300 2 5.0   230  
array-tiling/mlceu_false-unreach-call.i 0 3.4 280 31 0 92    2000 -32 7.6   260   0 2.8  180 -32 .60   19    - -
array-tiling/skippedu_false-unreach-call.i 1 3.6 290 30 0 92    2000 1 7.9   280   0 2.9  210 -32 .59   19    - -
array-tiling/mbpr2_true-unreach-call.i -16 4.0 300 36 - - - - 0 900    2800 2 6.3   260  
array-tiling/mbpr3_true-unreach-call.i -16 4.5 310 38 - - - - 0 900    2800 2 7.5   270  
array-tiling/mbpr4_true-unreach-call.i -16 5.0 310 48 - - - - 0 900    2700 2 7.5   290  
array-tiling/mbpr5_true-unreach-call.i -16 5.6 320 48 - - - - 0 900    2700 2 8.7   310  
array-tiling/nr2_true-unreach-call.i -16 3.8 290 37 - - - - 0 900    2700 0 960     1500  
array-tiling/nr3_true-unreach-call.i -16 3.8 300 34 - - - - 0 900    2800 2 79     830  
array-tiling/nr4_true-unreach-call.i -16 3.8 290 33 - - - - 0 900    2700 2 130     1900  
array-tiling/nr5_true-unreach-call.i -16 3.8 300 37 - - - - 0 900    2800 0 130     7000  
array-tiling/pnr2_true-unreach-call.i -16 3.6 300 33 - - - -