Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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-12-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.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 61     15000 720    0 .45 44 0 .019 4.8 0 .95 49 0 .0016 .29 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 890     11 12000    0 .68 42 0 .023 4.9 0 1.1  51 0 .0015 .26 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 890     11 14000    0 .67 43 0 .019 4.9 0 1.1  49 0 .0014 .29 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 890     12 12000    0 .73 43 0 .019 4.8 0 .66 49 0 .0015 .27 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 890     11 13000    0 .71 41 0 .022 4.8 0 1.1  49 0 .0015 .29 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 890     11 11000    0 .71 43 0 .021 4.9 0 1.1  49 0 .0017 .26 - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 890     130 12000    0 .71 44 0 .019 4.9 0 .87 49 0 .0016 .27 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 890     130 12000    0 .63 41 0 .018 4.9 0 1.1  49 0 .0017 .27 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 900     140 11000    0 .74 42 0 .019 5.0 0 1.1  49 0 .0016 .29 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 890     130 11000    0 .61 41 0 .020 4.8 0 .96 49 0 .0013 .26 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 890     140 12000    0 .73 41 0 .018 4.8 0 .87 49 0 .0015 .27 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 900     130 11000    0 .72 43 0 .019 4.8 0 1.1  49 0 .0014 .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 900     130 12000    0 .68 41 0 .017 4.8 0 .87 49 0 .0017 .27 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 900     130 13000    0 .55 42 0 .023 4.8 0 1.1  49 0 .0015 .26 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 900     130 12000    0 .68 43 0 .020 4.8 0 .96 48 0 .0016 .29 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 33     15000 380    0 .47 43 0 .019 4.9 0 1.1  51 0 .0016 .26 - -
array-examples/standard_init1_false-unreach-call_ground.i 0 26     15000 380    0 .71 41 0 .019 4.8 0 .88 47 0 .0013 .28 - -
array-examples/standard_init2_false-unreach-call_ground.i 0 29     15000 390    0 .71 44 0 .018 4.8 0 .89 49 0 .0013 .28 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 30     15000 370    0 .62 43 0 .019 4.9 0 .86 47 0 .0016 .27 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 32     15000 440    0 .71 43 0 .023 4.8 0 1.1  49 0 .0014 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 34     15000 470    0 .64 43 0 .019 4.9 0 .94 47 0 .0013 .26 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 36     15000 490    0 .45 44 0 .019 4.9 0 .92 47 0 .0016 .27 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 38     15000 470    0 .46 43 0 .022 4.9 0 .89 47 0 .0015 .26 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 40     15000 600    0 .44 44 0 .021 4.8 0 .91 47 0 .0013 .26 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 42     15000 640    0 .66 44 0 .018 4.8 0 .66 49 0 .0013 .28 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 28     15000 410    0 .67 43 0 .020 4.9 0 .68 50 0 .0015 .27 - -
array-examples/standard_partition_false-unreach-call_ground.i -32 6.7   15 83    0 92    1900 0 97     630   0 1.2  51 0 .086  9.0  - -
array-examples/standard_running_false-unreach-call.i 0 36     15000 450    0 .53 41 0 .020 4.9 0 .67 49 0 .0015 .29 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 23     11 340    - - - - 0 920    6100 2 9.5   270  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 2 30     12 470    - - - - 0 920    6100 0 960     1900  
array-examples/relax_true-unreach-call.i 0 .038 11 .48 - - - - 0 .55 41 0 .025 5.0
array-examples/sanfoundry_02_true-unreach-call_ground.i 2 20     11 270    - - - - 0 900    2600 0 960     4900  
array-examples/sanfoundry_10_true-unreach-call_ground.i 2 9.5   11 110    - - - - 0 910    6300 0 960     1100  
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 0 900     330 11000    - - - - 0 .63 43 0 .027 4.8
array-examples/sanfoundry_27_true-unreach-call_ground.i 2 10     11 170    - - - - 0 900    2500 0 960     2400  
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 6.4   12 81    - - - - 2 3.2  260 2 6.1   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 890     11 14000    - - - - 0 .56 44 0 .025 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 900     12 13000    - - - - 0 .54 45 0 .025 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i 2 18     12 260    - - - - 0 900    4600 0 960     2100  
array-examples/standard_compare_true-unreach-call_ground.i 2 11     12 150    - - - - 0 900    6200 0 960     4700  
array-examples/standard_copy1_true-unreach-call_ground.i 0 900     120 11000    - - - - 0 .57 44 0 .019 4.9
array-examples/standard_copy2_true-unreach-call_ground.i 0 890     120 11000    - - - - 0 .55 43 0 .018 5.0
array-examples/standard_copy3_true-unreach-call_ground.i 0 900     120 11000    - - - - 0 .56 45 0 .021 4.8
array-examples/standard_copy4_true-unreach-call_ground.i 0 890     130 14000    - - - - 0 .56 43 0 .024 4.8
array-examples/standard_copy5_true-unreach-call_ground.i 0 900     130 14000    - - - - 0 .56 43 0 .020 4.9
array-examples/standard_copy6_true-unreach-call_ground.i 0 900     130 12000    - - - - 0 .63 42 0 .046 4.9
array-examples/standard_copy7_true-unreach-call_ground.i 0 900     130 11000    - - - - 0 .55 43 0 .018 4.9
array-examples/standard_copy8_true-unreach-call_ground.i 0 900     130 10000    - - - - 0 .57 43 0 .021 4.8
array-examples/standard_copy9_true-unreach-call_ground.i 0 890     130 13000    - - - - 0 .60 44 0 .025 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 15     12 210    - - - - 0 900    2800 0 960     4800  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 18     12 260    - - - - 0 900    3800 0 960     5000  
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 16     46 210    - - - - 0 900    3500 0 960     4800  
array-examples/standard_copyInit_true-unreach-call_ground.i 2 12     12 180    - - - - 0 900    5000 0 960     3900  
array-examples/standard_find_true-unreach-call_ground.i 0 890     130 11000    - - - - 0 .54 45 0 .020 4.8
array-examples/standard_init1_true-unreach-call_ground.i 2 9.1   11 120    - - - - 0 900    5000 0 960     2100  
array-examples/standard_init2_true-unreach-call_ground.i 2 11     11 180    - - - - 0 910    4800 0 960     3700  
array-examples/standard_init3_true-unreach-call_ground.i 2 13     11 170    - - - - 0 900    5500 0 960     4500  
array-examples/standard_init4_true-unreach-call_ground.i 2 15     11 210    - - - - 0 900    4100 0 960     5000  
array-examples/standard_init5_true-unreach-call_ground.i 2 17     11 220    - - - - 0 900    4400 0 960     5200  
array-examples/standard_init6_true-unreach-call_ground.i 2 19     11 250    - - - - 0 900    5000 0 960     5200  
array-examples/standard_init7_true-unreach-call_ground.i 2 21     11 310    - - - - 0 900    5000 0 960     4800  
array-examples/standard_init8_true-unreach-call_ground.i 2 22     12 340    - - - - 0 900    5900 0 960     4800  
array-examples/standard_init9_true-unreach-call_ground.i 2 25     11 260    - - - - 0 900    4700 0 960     5400  
array-examples/standard_maxInArray_true-unreach-call_ground.i 2 10     11 130    - - - - 0 900    2500 0 960     2500  
array-examples/standard_minInArray_true-unreach-call_ground.i 2 11     11 120    - - - - 0 900    4600 0 960     2200  
array-examples/standard_palindrome_true-unreach-call_ground.i 2 5.5   11 89    - - - - 0 910    5400 0 960     1400  
array-examples/standard_partial_init_true-unreach-call_ground.i 2 20     13 250    - - - - 0 900    2300 0 960     4100  
array-examples/standard_partition_original_true-unreach-call_ground.i 2 12     13 140    - - - - 0 900    4200 0 90     7000  
array-examples/standard_partition_true-unreach-call_ground.i 2 8.3   12 110    - - - - 0 910    5600 0 960     5600  
array-examples/standard_password_true-unreach-call_ground.i 2 10     12 160    - - - - 0 900    6100 0 960     4700  
array-examples/standard_reverse_true-unreach-call_ground.i 2 10     12 140    - - - - 0 900    4900 0 960     1700  
array-examples/standard_running_true-unreach-call.i 2 11     12 130    - - - - 0 900    5600 0 960     750  
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 1.2   170 17    - - - - 0 900    800 2 9.4   320  
array-examples/standard_seq_init_true-unreach-call_ground.i 2 9.1   11 120    - - - - 0 900    2400 0 960     2200  
array-examples/standard_strcmp_true-unreach-call_ground.i 2 11     12 170    - - - - 0 900    5100 0 960     4600  
array-examples/standard_strcpy_original_true-unreach-call.i 0 890     130 12000    - - - - 0 .53 43 0 .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i 0 890     120 11000    - - - - 0 .41 43 0 .024 4.9
array-examples/standard_two_index_01_true-unreach-call.i 2 300     50 2700    - - - - 0 900    4100 0 960     2700  
array-examples/standard_two_index_02_true-unreach-call.i 0 900     120 11000    - - - - 0 .62 43 0 .018 4.9
array-examples/standard_two_index_03_true-unreach-call.i 2 290     49 2700    - - - - 0 900    5000 0 960     3200  
array-examples/standard_two_index_04_true-unreach-call.i 0 900     130 11000    - - - - 0 .57 44 0 .023 4.9
array-examples/standard_two_index_05_true-unreach-call.i 0 890     120 11000    - - - - 0 .57 43 0 .024 4.8
array-examples/standard_two_index_06_true-unreach-call.i 2 300     49 3000    - - - - 0 900    3700 0 960     3000  
array-examples/standard_two_index_07_true-unreach-call.i 0 900     130 11000    - - - - 0 .41 44 0 .020 4.9
array-examples/standard_two_index_08_true-unreach-call.i 0 900     130 11000    - - - - 0 .56 43 0 .022 4.8
array-examples/standard_two_index_09_true-unreach-call.i 0 890     120 14000    - - - - 0 .66 43 0 .048 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 2 .32  11 4.0  - - - - 0 760    7000 0 960     4600  
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 9.8   13 140    - - - - 0 900    3900 0 960     2000  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 1 3.2   30 45    0 92    610 -32 11     460   0 3.8  210 1 .58   18    - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 1 3.2   11 50    0 92    920 0 97     4800   0 3.3  180 1 .66   18    - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 900     4000 6100    0 .44 43 0 .018 4.8 0 .87 50 0 .0016 .28 - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 32     15000 390    0 .70 41 0 .020 4.9 0 1.1  49 0 .0016 .28 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 900     3200 9300    0 .59 43 0 .020 4.9 0 1.1  49 0 .0015 .27 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 57     15000 720    0 .68 41 0 .018 4.8 0 .88 47 0 .0016 .29 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 900     3700 9800    - - - - 0 .55 43 0 .023 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 3.3   11 38    - - - - 0 .52 44 0 .025 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 17     13 220    - - - - 0 900    3800 0 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 .35  12 3.7  - - - - 0 .65 43 0 .024 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 2 11     50 140    - - - - 0 910    6100 2 15     480  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900     3500 8700    - - - - 0 .55 43 0 .022 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 3.2   11 40    - - - - 0 .54 44 0 .026 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 900     120 11000    - - - - 0 .57 45 0 .025 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 2 9.1   30 130    - - - - 0 900    3800 0 960     6000  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900     3200 9800    - - - - 0 .55 44 0 .023 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 2 .50  12 5.6  - - - - 0 910    5500 0 960     4700  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 0 .57  13 7.6  0 6.4  360 -32 5.4   230   0 3.6  210 -32 .75   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 .68  17 8.9  1 9.0  380 -32 4.9   230   0 3.9  210 1 .71   18    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 1.2   28 16    1 15    460 -32 5.2   240   0 4.3  210 1 .77   18    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 1.7   30 23    0 92    950 -32 5.7   250   0 3.6  210 1 .72   19    - -
reducercommutativity/rangesum60_false-unreach-call.i 1 2.2   37 27    0 93    1600 -32 5.6   280   0 3.8  260 1 .67   19    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i -32 4.4   33 53    0 92    1800 1 13     500   0 .71 51 0 .072  9.0  - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 .38  11 4.6  - - - - 0 900    1300 0 960     5100  
reducercommutativity/avg10_true-unreach-call_true-termination.i 0 900     110 11000    - - - - 0 .54 43 0 .020 4.8
reducercommutativity/avg20_true-unreach-call.i 2 110     42 1400    - - - - 0 900    4900 0 960     1800  
reducercommutativity/avg40_true-unreach-call.i 0 900     140 12000    - - - - 0 .58 44 0 .024 4.9
reducercommutativity/avg60_true-unreach-call.i 0 900     140 11000    - - - - 0 .40 43 0 .020 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i 2 .51  12 6.4  - - - - 0 900    2900 0 960     590  
reducercommutativity/max05_true-unreach-call_true-termination.i 2 14     15 200    - - - - 2 110    920 0 960     3700  
reducercommutativity/max10_true-unreach-call_true-termination.i 0 900     110 10000    - - - - 0 .53 43 0 .019 4.9
reducercommutativity/max20_true-unreach-call.i 0 900     180 11000    - - - - 0 .54 44 0 .018 4.9
reducercommutativity/max40_true-unreach-call.i 0 900     210 12000    - - - - 0 .53 44 0 .026 5.0
reducercommutativity/max60_true-unreach-call.i 0 900     240 11000    - - - - 0 .68 43 0 .025 4.9
reducercommutativity/max_true-unreach-call_true-termination.i 2 .51  12 5.5  - - - - 0 900    3500 0 960     900  
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 3.5   12 52    - - - - 0 900    1500 0 960     1800  
reducercommutativity/sep10_true-unreach-call.i 2 150     35 1600    - - - - 0 900    1800 0 930     7000  
reducercommutativity/sep20_true-unreach-call.i 0 900     3500 8400    - - - - 0 .71 43 0 .022 4.8
reducercommutativity/sep40_true-unreach-call.i 0 900     3300 6200    - - - - 0 .59 43 0 .023 4.9
reducercommutativity/sep60_true-unreach-call.i 0 900     3400 6800    - - - - 0 .58 41 0 .020 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 2 .50  12 6.1  - - - - 0 900    4200 0 960     3000  
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 .42  11 4.4  - - - - 0 900    960 2 350     3400  
reducercommutativity/sum10_true-unreach-call_true-termination.i 0 900     56 12000    - - - - 0 .54 42 0 .026 4.9
reducercommutativity/sum20_true-unreach-call.i 2 .57  12 7.5  - - - - 0 900    4600 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i 2 .70  12 9.4  - - - - 0 900    2500 0 960     4100  
reducercommutativity/sum60_true-unreach-call.i 2 .93  12 12    - - - - 0 900    3000 0 960     3100  
reducercommutativity/sum_true-unreach-call_true-termination.i 2 .49  12 5.8  - - - - 0 900    3400 0 960     4700  
array-tiling/mlceu_false-unreach-call.i -32 .45  12 4.9  0 92    1400 0 97     980   0 1.1  51 0 .088  9.0  - -
array-tiling/skippedu_false-unreach-call.i 0 .055 11 .27 0 .72 43 0 .020 4.9 0 .86 50 0 .0015 .30 - -
array-tiling/mbpr2_true-unreach-call.i 0 .068 11 .23 - - - - 0 .53 41 0 .019 4.9
array-tiling/mbpr3_true-unreach-call.i 0 .035 11 .41 - - - - 0 .60 43 0 .025 4.9
array-tiling/mbpr4_true-unreach-call.i 0 .035 11 .31 - - - - 0 .57 44 0 .025 4.8
array-tiling/mbpr5_true-unreach-call.i 0 .058 12 .27 - - - - 0 .57 44 0 .023 4.8
array-tiling/nr2_true-unreach-call.i 0 .061 11 .19 - - - - 0 .59 43 0 .024 4.8
array-tiling/nr3_true-unreach-call.i 0 .062 11 .26 - - - - 0 .54 43 0 .018 4.8
array-tiling/nr4_true-unreach-call.i 0 .041 11 .37 - - - - 0 .40 43 0 .018 4.8
array-tiling/nr5_true-unreach-call.i 0 .062 11 .25 - - - - 0 .55 45 0 .047 4.8
array-tiling/pnr2_true-unreach-call.i 0 .039 11 .29 - - - - 0 .53 41 0 .023 4.9
array-tiling/pnr3_true-unreach-call.i 0 .062 11 .27 - - - - 0 .53 41 0 .021 4.8
array-tiling/pnr4_true-unreach-call.i 0 .061 11 .24 - - - - 0 .62 43 0 .021 4.9
array-tiling/pnr5_true-unreach-call.i 0 .072 11 .25 - - - - 0 .54 41 0 .018 4.8
array-tiling/poly1_true-unreach-call.i 2 .43  12 4.7  - - - - 0 900    4800 0 960     960  
array-tiling/poly2_true-unreach-call.i 0 .071 11 .31 - - - - 0 .55 43 0 .019 4.9
array-tiling/pr2_true-unreach-call.i 0 .040 11 .33 - - - - 0 .55 43 0 .019 4.8
array-tiling/pr3_true-unreach-call.i 0 .036 11 .35 - - - - 0 .71 43 0 .026 4.9
array-tiling/pr4_true-unreach-call.i 0 .063 11 .27 - - - - 0 .57 43 0 .024 5.0
array-tiling/pr5_true-unreach-call.i 0 .059 11 .26 - - - - 0 .56 43 0 .019 4.9
array-tiling/revcpyswp2_true-unreach-call.i 2 .51  12 5.7  - - - - 0 900    2000 0 960     2000  
array-tiling/rew_true-unreach-call.i 2 .46  12 4.7  - - - - 0 900    2800 0 960     1700  
array-tiling/rewnif_true-unreach-call.i 2 .47  12 4.6  - - - - 0 900    2600 0 960     1100  
array-tiling/rewnifrev2_true-unreach-call.i 2 .81  12 10    - - - - 0 900    1600 0 960     3000  
array-tiling/rewnifrev_true-unreach-call.i 2 .88  12 12    - - - - 0 900    2100 0 960     1900  
array-tiling/rewrev_true-unreach-call.i 2 .84  12 11    - - - - 0 900    2300 0 960     2100  
array-tiling/skipped_true-unreach-call.i 0 .039 11 .27 - - - - 0 .59 46 0 .026 5.0
array-tiling/tcpy_true-unreach-call.i 0 .064 11 .30 - - - - 0 .57 44 0 .022 4.8
array-programs/copysome1_false-unreach-call.i 0 900     140 11000    0 .73 44 0 .018 4.9 0 .93 49 0 .0016 .29 - -
array-programs/copysome2_false-unreach-call.i 0 900     150 12000    0 .73 44 0 .022 5.0 0 .86 50 0 .0014 .29 - -
array-programs/copysome1_true-unreach-call.i 0 900     140 11000    - - - - 0 .54 41 0 .019 4.9
array-programs/copysome2_true-unreach-call.i 0 890     140 11000    - - - - 0 .55 43 0 .019 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 34 52000    260000 650000   44 2 700 12000 44 -191 340 8800 44 0 61 3300 44 -26 5.1  170 123 4 54000 240000 123 10 54000 200000
    correct results 68 130 1700    1300 19000   2 2 24 840 1 1 13 500 0 6 6 4.1  110 2 4 110 1200 5 10 390 4700
        correct true 62 124 1700    1100 19000   0 0 0 0 2 4 110 1200 5 10 390 4700
        correct false 6 6 12    150 170   2 2 24 840 1 1 13 500 0 6 6 4.1  110 0 0
    correct-unconfimed results 1 0 .57 13 7.6 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 .57 13 7.6 0 0 0 0 0 0
    incorrect results 3 -96 11    59 140   0 6 -192 37 1700 0 1 -32 .75 18 0 0
        incorrect true 3 -96 11    59 140   0 6 -192 37 1700 0 1 -32 .75 18 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 34 2 -191 0 -26 4 10
Run set map2check.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Arrays