Tool skink 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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] 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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.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 1 6.0 330 56 0 94    2600 -32 5.0   280   0 2.7  210 1 .70   18    - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 34   690 390 0 .65 41 0 .023 4.9 0 .82 47 0 .0010 .29 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 34   700 390 0 .56 44 0 .019 4.8 0 .67 49 0 .0011 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 110   860 1200 0 .40 41 0 .020 4.9 0 .84 47 0 .0011 .28 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 110   810 1200 0 .40 41 0 .020 4.9 0 .65 49 0 .0041 .26 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 1 5.8 320 53 0 92    2000 -32 3.9   270   0 2.0  210 1 12      18    - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 43   710 460 0 .56 44 0 .018 4.8 0 .83 47 0 .0010 .29 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 5.7 320 52 0 .59 43 0 .020 4.8 0 .84 47 0 .0011 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 5.9 320 50 0 .63 43 0 .018 4.8 0 .66 49 0 .0033 .29 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 6.0 320 54 0 .55 44 0 .022 4.9 0 .85 47 0 .0012 .28 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 5.7 320 50 0 .68 42 0 .023 5.0 0 .86 47 0 .0036 .26 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 6.1 320 52 0 .53 41 0 .018 4.8 0 .85 47 0 .0035 .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 5.5 300 46 0 .71 46 0 .021 4.8 0 .66 49 0 .0012 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 5.8 320 46 0 .64 41 0 .018 4.9 0 .84 47 0 .0039 .29 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 5.5 300 49 0 .54 44 0 .018 4.8 0 .65 49 0 .0011 .28 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 6.1 320 54 0 .40 41 0 .033 4.9 0 .65 49 0 .0036 .28 - -
array-examples/standard_init1_false-unreach-call_ground.i 0 40   720 460 0 .53 44 0 .021 5.0 0 .83 47 0 .0041 .26 - -
array-examples/standard_init2_false-unreach-call_ground.i 0 26   690 270 0 .54 42 0 .018 4.8 0 .86 47 0 .0019 .28 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 22   720 200 0 .40 43 0 .021 4.8 0 .84 47 0 .0014 .29 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 22   690 220 0 .68 46 0 .018 4.8 0 .85 48 0 .0018 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 22   680 190 0 .56 43 0 .018 4.9 0 .81 47 0 .0030 .29 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 24   690 240 0 .66 43 0 .023 4.9 0 .68 49 0 .0011 .26 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 24   690 270 0 .68 41 0 .022 4.9 0 .66 49 0 .0035 .29 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 25   700 240 0 .56 44 0 .020 4.9 0 .66 49 0 .0036 .29 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 26   690 240 0 .67 45 0 .019 5.0 0 .83 47 0 .0011 .26 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 42   710 510 0 .58 43 0 .022 4.9 0 .83 47 0 .0036 .26 - -
array-examples/standard_partition_false-unreach-call_ground.i 0 26   680 240 0 .41 43 0 .018 4.8 0 .85 48 0 .0038 .26 - -
array-examples/standard_running_false-unreach-call.i 0 24   700 240 0 .67 45 0 .021 4.9 0 .84 47 0 .0041 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 4.1 270 36 - - - - 0 900    6100 2 7.1   270  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 31   690 310 - - - - 0 .56 42 0 .020 4.9
array-examples/relax_true-unreach-call.i 0 8.1 410 67 - - - - 0 .59 42 0 .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 31   700 320 - - - - 0 .57 43 0 .021 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 160   720 1700 - - - - 0 .59 46 0 .019 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 4.5 270 44 - - - - 2 6.4  490 2 7.9   260  
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 60   720 640 - - - - 0 .56 43 0 .020 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 4.4 290 41 - - - - 2 4.8  270 2 5.1   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 34   720 410 - - - - 0 .59 42 0 .024 5.0
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 900   1700 8800 - - - - 0 .53 42 0 .019 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i 0 26   680 240 - - - - 0 .56 41 0 .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i 0 45   710 470 - - - - 0 .58 45 0 .020 4.8
array-examples/standard_copy1_true-unreach-call_ground.i 0 5.8 320 48 - - - - 0 .56 44 0 .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i 0 5.8 320 56 - - - - 0 .58 42 0 .019 4.8
array-examples/standard_copy3_true-unreach-call_ground.i 0 5.6 320 53 - - - - 0 .55 43 0 .019 4.9
array-examples/standard_copy4_true-unreach-call_ground.i 0 5.8 320 47 - - - - 0 .54 41 0 .019 4.8
array-examples/standard_copy5_true-unreach-call_ground.i 0 5.6 320 53 - - - - 0 .69 41 0 .020 4.8
array-examples/standard_copy6_true-unreach-call_ground.i 0 6.4 400 50 - - - - 0 .58 41 0 .019 4.8
array-examples/standard_copy7_true-unreach-call_ground.i 0 5.7 320 51 - - - - 0 .54 43 0 .025 5.0
array-examples/standard_copy8_true-unreach-call_ground.i 0 5.3 310 45 - - - - 0 .70 42 0 .018 4.9
array-examples/standard_copy9_true-unreach-call_ground.i 0 5.7 320 52 - - - - 0 .53 44 0 .023 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 5.8 310 53 - - - - 0 .56 44 0 .024 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 6.0 320 58 - - - - 0 .55 42 0 .018 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 5.9 310 56 - - - - 0 .71 43 0 .022 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i 0 5.5 310 51 - - - - 0 .56 44 0 .019 4.8
array-examples/standard_find_true-unreach-call_ground.i 0 24   710 250 - - - - 0 .58 46 0 .021 4.9
array-examples/standard_init1_true-unreach-call_ground.i 0 39   720 400 - - - - 0 .54 42 0 .019 4.8
array-examples/standard_init2_true-unreach-call_ground.i 0 26   690 250 - - - - 0 .56 43 0 .022 4.9
array-examples/standard_init3_true-unreach-call_ground.i 0 21   710 190 - - - - 0 .54 44 0 .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i 0 21   670 200 - - - - 0 .54 43 0 .020 4.9
array-examples/standard_init5_true-unreach-call_ground.i 0 23   680 230 - - - - 0 .54 42 0 .018 4.8
array-examples/standard_init6_true-unreach-call_ground.i 0 23   680 230 - - - - 0 .44 43 0 .019 4.9
array-examples/standard_init7_true-unreach-call_ground.i 0 25   700 250 - - - - 0 .54 43 0 .020 4.9
array-examples/standard_init8_true-unreach-call_ground.i 0 24   680 230 - - - - 0 .55 43 0 .025 5.0
array-examples/standard_init9_true-unreach-call_ground.i 0 25   690 280 - - - - 0 .54 42 0 .027 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 41   740 410 - - - - 0 .54 42 0 .019 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i 0 42   730 440 - - - - 0 .73 42 0 .019 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i 0 45   710 530 - - - - 0 .50 43 0 .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i 0 34   720 410 - - - - 0 .68 43 0 .019 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i 0 33   690 300 - - - - 0 .63 42 0 .035 4.9
array-examples/standard_partition_true-unreach-call_ground.i 0 69   710 830 - - - - 0 .46 44 0 .019 4.8
array-examples/standard_password_true-unreach-call_ground.i 0 46   700 520 - - - - 0 .52 44 0 .020 4.8
array-examples/standard_reverse_true-unreach-call_ground.i 0 46   730 430 - - - - 0 .43 43 0 .018 4.8
array-examples/standard_running_true-unreach-call.i 0 29   710 290 - - - - 0 .65 42 0 .019 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 25   700 240 - - - - 0 900    1000 2 11     330  
array-examples/standard_seq_init_true-unreach-call_ground.i 0 40   700 450 - - - - 0 .50 43 0 .022 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i 0 240   710 3300 - - - - 0 .55 43 0 .019 4.9
array-examples/standard_strcpy_original_true-unreach-call.i 0 30   710 300 - - - - 0 .68 42 0 .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i 0 26   690 230 - - - - 0 .55 42 0 .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i 0 5.6 310 47 - - - - 0 .61 43 0 .018 4.8
array-examples/standard_two_index_02_true-unreach-call.i 0 32   720 310 - - - - 0 .57 44 0 .019 4.9
array-examples/standard_two_index_03_true-unreach-call.i 0 33   720 310 - - - - 0 .41 45 0 .017 4.9
array-examples/standard_two_index_04_true-unreach-call.i 0 31   700 330 - - - - 0 .63 41 0 .018 5.0
array-examples/standard_two_index_05_true-unreach-call.i 0 33   730 340 - - - - 0 .70 42 0 .021 4.9
array-examples/standard_two_index_06_true-unreach-call.i 0 32   780 320 - - - - 0 .60 41 0 .018 4.9
array-examples/standard_two_index_07_true-unreach-call.i 0 34   740 400 - - - - 0 .53 44 0 .019 4.8
array-examples/standard_two_index_08_true-unreach-call.i 0 31   700 330 - - - - 0 .50 44 0 .022 5.0
array-examples/standard_two_index_09_true-unreach-call.i 0 32   740 350 - - - - 0 .59 41 0 .021 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 100   710 1400 - - - - 0 .56 44 0 .022 5.0
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 49   720 510 - - - - 0 .54 43 0 .021 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 25   690 280 0 .57 44 0 .024 4.9 0 .85 48 0 .0032 .30 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 5.0 290 42 0 .70 45 0 .022 4.9 0 .84 47 0 .0011 .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 150   730 1700 0 .55 43 0 .018 4.9 0 .84 47 0 .0011 .28 - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 28   680 320 0 .41 41 0 .034 4.8 0 .84 47 0 .0011 .26 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 41   710 420 0 .66 42 0 .018 4.8 0 .85 47 0 .0011 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 54   700 590 0 .56 44 0 .023 4.8 0 .67 49 0 .0011 .26 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 350   700 3900 - - - - 0 .58 41 0 .023 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 28   700 300 - - - - 0 .53 42 0 .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 5.4 330 42 - - - - 0 .67 41 0 .022 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 5.3 300 49 - - - - 0 .61 43 0 .025 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 5.7 310 51 - - - - 0 .44 43 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 5.5 310 49 - - - - 0 .55 42 0 .020 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 5.9 330 48 - - - - 0 .41 45 0 .020 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 5.1 300 48 - - - - 0 .66 41 0 .018 5.0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 5.6 320 57 - - - - 0 .61 41 0 .020 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 5.9 350 55 - - - - 0 .61 41 0 .020 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 140   710 1600 - - - - 0 .56 42 0 .020 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 6.0 390 53 1 6.1  360 -32 4.9   230   0 2.1  210 1 .57   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 6.5 410 56 0 91    610 -32 3.6   240   0 2.0  210 1 .58   18    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 7.0 430 68 0 91    630 -32 3.5   230   0 2.0  210 1 .61   18    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 21   620 200 0 91    800 -32 3.6   230   0 2.0  190 1 .57   18    - -
reducercommutativity/rangesum60_false-unreach-call.i 0 67   950 560 0 .55 44 0 .019 4.9 0 .69 49 0 .0032 .29 - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 8.6 440 72 0 .57 42 0 .022 4.9 0 .90 47 0 .0010 .26 - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 16   840 140 - - - - 0 900    1500 0 960     4900  
reducercommutativity/avg10_true-unreach-call_true-termination.i 2 17   690 170 - - - - 0 900    3500 0 960     6800  
reducercommutativity/avg20_true-unreach-call.i 2 20   660 180 - - - - 0 900    5000 0 960     1700  
reducercommutativity/avg40_true-unreach-call.i 2 23   900 240 - - - - 0 900    3700 0 960     4200  
reducercommutativity/avg60_true-unreach-call.i 0 60   840 540 - - - - 0 .58 41 0 .019 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i 0 26   710 230 - - - - 0 .55 43 0 .019 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i 2 17   450 200 - - - - 2 99    930 0 960     1400  
reducercommutativity/max10_true-unreach-call_true-termination.i 2 18   450 200 - - - - 0 900    2800 0 960     3200  
reducercommutativity/max20_true-unreach-call.i 2 22   560 230 - - - - 0 900    4300 0 960     4500  
reducercommutativity/max40_true-unreach-call.i 0 47   740 520 - - - - 0 .45 43 0 .019 4.8
reducercommutativity/max60_true-unreach-call.i 0 24   690 240 - - - - 0 .56 43 0 .020 4.9
reducercommutativity/max_true-unreach-call_true-termination.i 0 22   680 200 - - - - 0 .48 44 0 .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 6.7 350 63 - - - - 2 870    1600 0 960     1800  
reducercommutativity/sep10_true-unreach-call.i 2 9.8 420 84 - - - - 0 900    1800 0 960     6500  
reducercommutativity/sep20_true-unreach-call.i 0 37   800 410 - - - - 0 .57 43 0 .025 4.9
reducercommutativity/sep40_true-unreach-call.i 0 41   920 410 - - - - 0 .77 43 0 .018 4.9
reducercommutativity/sep60_true-unreach-call.i 0 21   690 190 - - - - 0 .55 43 0 .019 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 0 19   680 190 - - - - 0 .54 41 0 .027 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 16   650 180 - - - - 0 900    850 2 350     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i 2 17   420 170 - - - - 0 900    2200 0 960     5400  
reducercommutativity/sum20_true-unreach-call.i 2 17   450 210 - - - - 0 900    4600 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i 2 21   670 190 - - - - 0 900    2500 0 960     4400  
reducercommutativity/sum60_true-unreach-call.i 0 25   720 240 - - - - 0 .60 43 0 .019 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i 0 22   690 220 - - - - 0 .53 43 0 .018 4.8
array-tiling/mlceu_false-unreach-call.i 0 170   730 1900 0 .68 46 0 .018 4.8 0 .67 49 0 .0019 .30 - -
array-tiling/skippedu_false-unreach-call.i 0 200   720 2200 0 .57 44 0 .019 4.8 0 .68 49 0 .0026 .26 - -
array-tiling/mbpr2_true-unreach-call.i 0 57   730 640 - - - - 0 .54 43 0 .024 4.9
array-tiling/mbpr3_true-unreach-call.i 0 41   740 380 - - - - 0 .64 41 0 .019 4.9
array-tiling/mbpr4_true-unreach-call.i 0 34   850 350 - - - - 0 .66 44 0 .018 5.0
array-tiling/mbpr5_true-unreach-call.i 0 42   750 450 - - - - 0 .56 43 0 .022 4.9
array-tiling/nr2_true-unreach-call.i 0 140   730 1700 - - - - 0 .59 41 0 .020 4.9
array-tiling/nr3_true-unreach-call.i 0 160   840 1900 - - - - 0 .70 41 0 .024 4.9
array-tiling/nr4_true-unreach-call.i 0 170   750 1700 - - - - 0 .69 42 0 .019 4.9
array-tiling/nr5_true-unreach-call.i 0 180   760 2000 - - - - 0 .55 42 0 .020 4.8
array-tiling/pnr2_true-unreach-call.i 0 26   720 250 - - - - 0 .44 43 0 .020 4.9
array-tiling/pnr3_true-unreach-call.i 0 28   720 280 - - - - 0 .62 42 0 .021 5.0
array-tiling/pnr4_true-unreach-call.i 0 28   720 290 - - - - 0 .65 41 0 .021 4.9
array-tiling/pnr5_true-unreach-call.i 0 30   740 290 - - - - 0 .59 41 0 .019 4.8
array-tiling/poly1_true-unreach-call.i 2 120   1400 1100 - - - - 0 900    5200 0 960     930  
array-tiling/poly2_true-unreach-call.i 0 220   1400 2400 - - - - 0 .63 44 0 .019 4.9
array-tiling/pr2_true-unreach-call.i 2 4.3 270 43 - - - - 0 900    2300 0 960     910  
array-tiling/pr3_true-unreach-call.i 2 4.6 360 37 - - - - 0 900    2100 0 960     920  
array-tiling/pr4_true-unreach-call.i 2 4.4 270 43 - - - - 0 900    2100 0 960     740  
array-tiling/pr5_true-unreach-call.i 2 4.3 270 39 - - - - 0 900    1900 0 960     1200  
array-tiling/revcpyswp2_true-unreach-call.i 0 41   750 410 - - - - 0 .55 44 0 .025 4.8
array-tiling/rew_true-unreach-call.i 0 6.8 340 55 - - - - 0 .45 43 0 .023 5.0
array-tiling/rewnif_true-unreach-call.i 0 6.8 350 52 - - - - 0 .56 41 0 .024 4.8
array-tiling/rewnifrev2_true-unreach-call.i 0 160   720 2000 - - - - 0 .49 43 0 .020 4.9
array-tiling/rewnifrev_true-unreach-call.i 0 91   750 960 - - - - 0 .56 44 0 .021 5.0
array-tiling/rewrev_true-unreach-call.i 2 32   720 390 - - - - 0 900    2300 0 960     2500  
array-tiling/skipped_true-unreach-call.i 0 190   720 2500 - - - - 0 .46 43 0 .024 4.8
array-tiling/tcpy_true-unreach-call.i 0 170   760 2200 - - - - 0 .68 43 0 .019 4.9
array-programs/copysome1_false-unreach-call.i 0 31   690 300 0 .62 43 0 .047 4.8 0 .66 49 0 .0011 .26 - -
array-programs/copysome2_false-unreach-call.i 0 6.5 330 56 0 .71 42 0 .018 4.9 0 .66 50 0 .0013 .30 - -
array-programs/copysome1_true-unreach-call.i 0 31   690 350 - - - - 0 .68 43 0 .020 4.9
array-programs/copysome2_true-unreach-call.i 0 6.4 320 55 - - - - 0 .57 42 0 .022 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 52 7500 100000 81000 44 1 490   8600 44 -192 25 1700 44 0 42 3100 44 6 16 120 123 8 18000 63000 123 10 18000 62000
    correct results 29 52 480 15000 4700 1 1 6.1 360 0 0 6 6 15 110 4 8 980 3300 5 10 380 4600
        correct true 23 46 430 12000 4300 0 0 0 0 4 8 980 3300 5 10 380 4600
        correct false 6 6 52 2500 490 1 1 6.1 360 0 0 6 6 15 110 0 0
    incorrect results 0 0 6 -192 24 1500 0 0 0 0
        incorrect true 0 0 6 -192 24 1500 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 52 1 -192 0 6 8 10
Run set skink.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Arrays