Tool CPAchecker 1.6.1-svn 26725 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:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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-bnb.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-bnb.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-bnb.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-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.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.6 270 21 0 .54 43 0 .023 4.8 0 1.1  49 0 .0012 .30 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 2.5 270 25 0 .55 43 0 .023 4.9 0 1.1  51 0 .0011 .30 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 2.6 270 23 0 .53 41 0 .025 4.8 0 1.0  52 0 .0035 .30 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 2.8 290 26 0 .55 41 0 .023 4.8 0 1.0  51 0 .0012 .32 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 2.8 290 28 0 .53 43 0 .023 5.0 0 .94 47 0 .0012 .34 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 2.5 270 23 0 .66 44 0 .021 4.8 0 1.0  50 0 .0011 .30 - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 2.5 270 24 0 .55 41 0 .019 4.9 0 1.1  49 0 .0011 .27 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 2.5 260 20 0 .55 43 0 .022 4.8 0 1.1  48 0 .0012 .33 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 2.6 270 23 0 .53 41 0 .023 4.8 0 .92 49 0 .0032 .26 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 2.6 270 24 0 .55 43 0 .019 4.9 0 .95 48 0 .0013 .26 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 2.6 270 23 0 .55 43 0 .023 4.8 0 .84 49 0 .0012 .34 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 2.5 270 23 0 .69 44 0 .023 4.8 0 .96 49 0 .0027 .29 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 2.5 270 23 0 .54 41 0 .022 5.0 0 1.1  47 0 .0013 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 2.6 270 25 0 .54 43 0 .021 4.9 0 .92 50 0 .0013 .26 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 2.6 270 21 0 .72 44 0 .024 4.9 0 .84 48 0 .0013 .30 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 2.5 270 25 0 .52 43 0 .022 5.0 0 1.1  50 0 .0013 .29 - -
array-examples/standard_init1_false-unreach-call_ground.i 0 2.4 270 22 0 .61 41 0 .022 4.9 0 1.0  47 0 .0016 .26 - -
array-examples/standard_init2_false-unreach-call_ground.i 0 2.7 290 23 0 .53 41 0 .024 5.0 0 .94 47 0 .0013 .30 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 2.6 260 24 0 .54 44 0 .020 4.9 0 .87 47 0 .0012 .34 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 2.6 270 25 0 .54 41 0 .023 4.8 0 .87 49 0 .0016 .23 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 2.7 290 26 0 .56 41 0 .022 4.8 0 .89 49 0 .0013 .33 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 2.7 290 23 0 .52 41 0 .023 4.8 0 .80 49 0 .0014 .30 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 2.7 270 22 0 .60 43 0 .022 5.0 0 .71 49 0 .0015 .26 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 2.7 270 21 0 .53 43 0 .023 4.9 0 1.0  47 0 .0012 .34 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 2.7 270 23 0 .56 42 0 .022 4.8 0 1.0  53 0 .0011 .31 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 2.5 270 22 0 .61 43 0 .020 4.9 0 .96 49 0 .0014 .26 - -
array-examples/standard_partition_false-unreach-call_ground.i 0 2.4 270 23 0 .56 43 0 .022 4.9 0 1.0  49 0 .0012 .36 - -
array-examples/standard_running_false-unreach-call.i 0 3.0 290 26 0 .53 41 0 .026 4.8 0 .93 47 0 .0012 .29 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 2.5 260 24 - - - - 0 .69 44 0 .024 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .59 44 0 .022 4.8
array-examples/relax_true-unreach-call.i 0 8.1 440 61 - - - - 0 .54 43 0 .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 2.6 270 25 - - - - 0 .69 44 0 .022 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900   4100 8100 - - - - 0 .64 43 0 .019 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 0 2.7 290 25 - - - - 0 .61 43 0 .020 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 2.5 270 26 - - - - 0 .53 42 0 .021 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 2.8 280 29 - - - - 2 3.6  260 2 5.1   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 3.0 290 25 - - - - 0 .58 43 0 .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 2.5 270 20 - - - - 0 .56 43 0 .018 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .65 43 0 .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i 0 2.9 290 24 - - - - 0 .65 42 0 .020 4.8
array-examples/standard_copy1_true-unreach-call_ground.i 0 2.5 270 23 - - - - 0 .53 43 0 .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .54 41 0 .020 4.9
array-examples/standard_copy3_true-unreach-call_ground.i 0 2.7 270 20 - - - - 0 .56 42 0 .019 5.0
array-examples/standard_copy4_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .68 44 0 .017 4.9
array-examples/standard_copy5_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .51 41 0 .019 4.8
array-examples/standard_copy6_true-unreach-call_ground.i 0 2.5 270 25 - - - - 0 .65 43 0 .019 4.9
array-examples/standard_copy7_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .69 44 0 .024 5.0
array-examples/standard_copy8_true-unreach-call_ground.i 0 2.6 270 22 - - - - 0 .51 41 0 .022 4.8
array-examples/standard_copy9_true-unreach-call_ground.i 0 2.6 270 22 - - - - 0 .69 41 0 .022 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 2.5 270 25 - - - - 0 .59 42 0 .019 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .55 43 0 .019 5.0
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 2.6 270 24 - - - - 0 .69 43 0 .021 5.0
array-examples/standard_copyInit_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .54 43 0 .022 4.9
array-examples/standard_find_true-unreach-call_ground.i 0 2.6 270 25 - - - - 0 .56 44 0 .024 4.8
array-examples/standard_init1_true-unreach-call_ground.i 0 2.5 260 22 - - - - 0 .69 44 0 .022 4.9
array-examples/standard_init2_true-unreach-call_ground.i 0 2.4 270 21 - - - - 0 .52 44 0 .021 4.9
array-examples/standard_init3_true-unreach-call_ground.i 0 2.5 270 22 - - - - 0 .70 44 0 .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i 0 2.5 270 25 - - - - 0 .55 44 0 .022 4.8
array-examples/standard_init5_true-unreach-call_ground.i 0 2.6 270 23 - - - - 0 .73 44 0 .019 4.9
array-examples/standard_init6_true-unreach-call_ground.i 0 2.8 290 23 - - - - 0 .65 44 0 .020 4.8
array-examples/standard_init7_true-unreach-call_ground.i 0 2.7 290 24 - - - - 0 .53 41 0 .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i 0 2.6 270 21 - - - - 0 .71 43 0 .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i 0 2.6 260 22 - - - - 0 .52 43 0 .019 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 2.4 270 22 - - - - 0 .51 41 0 .022 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i 0 2.6 270 25 - - - - 0 .56 43 0 .020 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i 0 2.5 270 23 - - - - 0 .60 43 0 .023 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i 0 2.8 300 24 - - - - 0 .53 44 0 .020 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i 0 2.6 270 21 - - - - 0 .55 43 0 .019 4.8
array-examples/standard_partition_true-unreach-call_ground.i 0 2.8 290 24 - - - - 0 .51 44 0 .018 4.8
array-examples/standard_password_true-unreach-call_ground.i 0 2.5 270 21 - - - - 0 .54 41 0 .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i 0 2.4 260 22 - - - - 0 .75 43 0 .019 4.8
array-examples/standard_running_true-unreach-call.i 0 2.8 290 26 - - - - 0 .74 41 0 .022 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 2.5 270 24 - - - - 0 .52 41 0 .018 5.0
array-examples/standard_seq_init_true-unreach-call_ground.i 0 2.6 270 22 - - - - 0 .58 43 0 .019 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i 0 2.6 270 26 - - - - 0 .56 44 0 .023 4.9
array-examples/standard_strcpy_original_true-unreach-call.i 0 2.7 270 22 - - - - 0 .73 43 0 .020 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i 0 2.5 260 24 - - - - 0 .53 41 0 .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i 0 2.7 270 25 - - - - 0 .53 43 0 .019 4.8
array-examples/standard_two_index_02_true-unreach-call.i 0 2.7 300 24 - - - - 0 .67 43 0 .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i 0 2.7 290 27 - - - - 0 .57 44 0 .021 5.0
array-examples/standard_two_index_04_true-unreach-call.i 0 2.6 270 23 - - - - 0 .53 43 0 .019 5.0
array-examples/standard_two_index_05_true-unreach-call.i 0 2.5 270 24 - - - - 0 .55 44 0 .023 5.0
array-examples/standard_two_index_06_true-unreach-call.i 0 2.6 270 24 - - - - 0 .57 43 0 .019 5.0
array-examples/standard_two_index_07_true-unreach-call.i 0 2.5 270 25 - - - - 0 .58 42 0 .018 4.9
array-examples/standard_two_index_08_true-unreach-call.i 0 2.5 270 23 - - - - 0 .55 42 0 .020 4.8
array-examples/standard_two_index_09_true-unreach-call.i 0 2.6 270 24 - - - - 0 .55 44 0 .024 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 2.7 290 24 - - - - 0 .53 41 0 .022 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 2.8 290 26 - - - - 0 .53 41 0 .024 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 2.6 270 22 0 .52 41 0 .018 4.8 0 .99 49 0 .0012 .26 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 900   4200 8400 0 .51 41 0 .017 4.8 0 .98 49 0 .0014 .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 2.5 270 22 0 .55 43 0 .025 4.9 0 .93 49 0 .0012 .32 - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 2.6 270 25 0 .53 42 0 .019 4.9 0 .88 50 0 .0012 .30 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 2.6 270 23 0 .61 43 0 .018 4.9 0 1.0  49 0 .0036 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   5600 9300 0 .54 41 0 .020 4.8 0 1.1  50 0 .0011 .29 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 2.5 270 23 - - - - 0 .68 41 0 .023 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 2.5 270 22 - - - - 0 .69 44 0 .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 900   4200 9500 - - - - 0 .65 41 0 .026 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900   4000 12000 - - - - 0 .53 41 0 .019 5.0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 900   5700 8800 - - - - 0 .65 41 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900   3900 11000 - - - - 0 .57 43 0 .018 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900   4200 7800 - - - - 0 .71 46 0 .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 900   4300 8800 - - - - 0 .56 46 0 .019 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 900   4300 12000 - - - - 0 .60 41 0 .019 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900   3900 12000 - - - - 0 .66 41 0 .019 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 900   11000 6600 - - - - 0 .63 45 0 .019 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 6.2 400 60 -32 3.7  260 1 74     4900   0 3.9  210 1 .62   19    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 7.6 430 65 -32 4.3  270 0 88     7000   0 3.8  220 1 .61   20    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 9.5 580 67 -32 4.6  260 0 88     7000   0 3.8  220 1 .61   21    - -
reducercommutativity/rangesum40_false-unreach-call.i 0 900   5400 11000 0 .56 43 0 .018 5.0 0 .95 47 0 .0032 .34 - -
reducercommutativity/rangesum60_false-unreach-call.i 0 900   5400 9800 0 .52 41 0 .023 4.8 0 .96 49 0 .0011 .29 - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 1 17   590 120 0 91    2000 1 16     540   0 3.5  210 -32 .58   19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i -16 5.8 370 52 - - - - 0 900    2100 0 75     7000  
reducercommutativity/avg10_true-unreach-call_true-termination.i -16 7.2 420 64 - - - - 0 900    3900 0 100     7000  
reducercommutativity/avg20_true-unreach-call.i -16 9.1 560 81 - - - - 0 900    2100 0 120     7000  
reducercommutativity/avg40_true-unreach-call.i -16 53   2400 530 - - - - 0 900    4900 0 55     7000  
reducercommutativity/avg60_true-unreach-call.i -16 120   4000 1200 - - - - 0 600    7000 0 70     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i 0 900   7800 8000 - - - - 0 .66 43 0 .023 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i -16 8.5 520 72 - - - - 0 3.9  280 0 67     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i -16 14   520 100 - - - - 0 6.0  350 0 79     7000  
reducercommutativity/max20_true-unreach-call.i -16 18   710 140 - - - - 0 14    570 0 63     7000  
reducercommutativity/max40_true-unreach-call.i 0 900   4400 12000 - - - - 0 .63 43 0 .019 4.8
reducercommutativity/max60_true-unreach-call.i 0 900   4400 11000 - - - - 0 .63 44 0 .026 4.8
reducercommutativity/max_true-unreach-call_true-termination.i -16 260   3200 3100 - - - - 0 3.7  280 0 420     7000  
reducercommutativity/sep05_true-unreach-call_true-termination.i -16 13   500 100 - - - - 0 4.3  300 0 76     7000  
reducercommutativity/sep10_true-unreach-call.i -16 34   1200 240 - - - - 0 5.4  330 0 81     7000  
reducercommutativity/sep20_true-unreach-call.i -16 140   3900 1600 - - - - 0 15    520 0 62     7000  
reducercommutativity/sep40_true-unreach-call.i 0 910   9900 6900 - - - - 0 .61 44 0 .019 4.8
reducercommutativity/sep60_true-unreach-call.i 0 910   10000 7700 - - - - 0 .65 44 0 .018 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 0 900   3900 12000 - - - - 0 .65 43 0 .019 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i -16 5.3 320 43 - - - - 0 900    2200 0 94     7000  
reducercommutativity/sum10_true-unreach-call_true-termination.i -16 6.5 360 46 - - - - 0 900    2500 0 96     7000  
reducercommutativity/sum20_true-unreach-call.i -16 8.1 480 68 - - - - 0 900    3600 0 80     7000  
reducercommutativity/sum40_true-unreach-call.i -16 55   2500 480 - - - - 0 900    2700 0 74     7000  
reducercommutativity/sum60_true-unreach-call.i -16 120   3900 1100 - - - - 0 290    7000 0 69     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i -16 93   3600 1000 - - - - 0 7.1  330 0 960     5400  
array-tiling/mlceu_false-unreach-call.i 0 58   2900 560 0 .58 41 0 .021 4.9 0 .90 47 0 .0013 .29 - -
array-tiling/skippedu_false-unreach-call.i 1 3.9 300 34 -32 3.1  260 1 9.3   280   0 3.0  190 -32 .59   19    - -
array-tiling/mbpr2_true-unreach-call.i 0 50   2400 440 - - - - 0 .55 43 0 .024 5.0
array-tiling/mbpr3_true-unreach-call.i 0 56   2500 490 - - - - 0 .64 41 0 .018 5.0
array-tiling/mbpr4_true-unreach-call.i 0 45   1800 380 - - - - 0 .53 41 0 .019 4.8
array-tiling/mbpr5_true-unreach-call.i 0 47   1700 430 - - - - 0 .60 41 0 .025 4.9
array-tiling/nr2_true-unreach-call.i 0 48   1900 430 - - - - 0 .65 45 0 .019 4.9
array-tiling/nr3_true-unreach-call.i 0 45   2000 370 - - - - 0 .53 41 0 .018 5.0
array-tiling/nr4_true-unreach-call.i 0 33   1200 300 - - - - 0 .54 42 0 .019 4.8
array-tiling/nr5_true-unreach-call.i 0 30   1200 240 - - - - 0 .57 43 0 .019 4.8
array-tiling/pnr2_true-unreach-call.i 0 5.1 300 42 - - - - 0 .53 41 0 .019 4.9
array-tiling/pnr3_true-unreach-call.i 0 4.4 310 35 - - - - 0 .61 43 0 .022 5.0
array-tiling/pnr4_true-unreach-call.i 0 4.6 320 40 - - - - 0 .54 44 0 .019 4.9
array-tiling/pnr5_true-unreach-call.i 0 4.7 310 38 - - - - 0 .58 43 0 .023 4.9
array-tiling/poly1_true-unreach-call.i 0 41   1600 370 - - - - 0 .62 41 0 .018 5.0
array-tiling/poly2_true-unreach-call.i 0 100   3800 890 - - - - 0 .70 44 0 .020 5.0
array-tiling/pr2_true-unreach-call.i 0 7.7 430 70 - - - - 0 .55 44 0 .026 4.8
array-tiling/pr3_true-unreach-call.i 0 5.1 330 46 - - - - 0 .68 41 0 .020 4.9
array-tiling/pr4_true-unreach-call.i 0 4.9 310 43 - - - - 0 .59 41 0 .019 4.8
array-tiling/pr5_true-unreach-call.i 0 5.6 340 52 - - - - 0 .53 44 0 .019 4.8
array-tiling/revcpyswp2_true-unreach-call.i 0 4.8 310 44 - - - - 0 .75 44 0 .019 4.8
array-tiling/rew_true-unreach-call.i 0 40   1500 360 - - - - 0 .56 44 0 .019 4.9
array-tiling/rewnif_true-unreach-call.i 0 46   1500 300 - - - - 0 .68 43 0 .021 5.0
array-tiling/rewnifrev2_true-unreach-call.i -16 4.8 300 44 - - - - 0 900    2600 0 130     7000  
array-tiling/rewnifrev_true-unreach-call.i 0 3.6 290 34 - - - - 0 .57 42 0 .019 4.9
array-tiling/rewrev_true-unreach-call.i 0 900   1000 13000 - - - - 0 .59 42 0 .024 4.9
array-tiling/skipped_true-unreach-call.i 0 4.2 310 39 - - - - 0 .59 43 0 .023 5.0
array-tiling/tcpy_true-unreach-call.i 0 3.7 300 37 - - - - 0 .67 43 0 .018 4.8
array-programs/copysome1_false-unreach-call.i 0 2.5 260 21 0 .58 42 0 .024 4.8 0 .87 50 0 .0015 .26 - -
array-programs/copysome2_false-unreach-call.i 0 2.6 270 23 0 .53 44 0 .022 5.0 0 .84 49 0 .0013 .28 - -
array-programs/copysome1_true-unreach-call.i 0 2.5 270 24 - - - - 0 .53 42 0 .020 4.9
array-programs/copysome2_true-unreach-call.i 0 2.6 270 25 - - - - 0 .66 44 0 .025 4.8
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
total 167 -297 21000   200000 220000 44 -128 130 4700 44 3 280 20000 44 0 55 3000 44 -61 3.1 110 123 2 9100   48000 123 2 2800   130000
    correct results 6 7 47   2600 380 0 3 3 99 5800 0 3 3 1.8 60 1 2 3.6 260 1 2 5.1 230
        correct true 1 2 2.8 280 29 0 0 0 0 1 2 3.6 260 1 2 5.1 230
        correct false 5 5 44   2300 350 0 3 3 99 5800 0 3 3 1.8 60 0 0
    incorrect results 19 -304 970   30000 10000 4 -128 16 1000 0 0 2 -64 1.2 37 0 0
        incorrect true 0 4 -128 16 1000 0 0 2 -64 1.2 37 0 0
        incorrect false 19 -304 970   30000 10000 0 0 0 0 0 0
score (167 tasks, max score: 290) -297 -128 3 0 -61 2 2
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays