Tool ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 0 900   750   14000 5300 2.3 0   .48 .31 10   39 5.8 3.1 97 290
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 900   730   12000 2200 2.3 0   .54 .35 10   44 5.4 2.9 79 290
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 900   730   14000 2100 2.3 0   .57 .37 7.8 41 6.2 3.3 100 300
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 900   710   13000 2400 2.3 0   .51 .32 7.5 39 5.6 3.0 130 300
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 900   720   12000 2600 2.3 0   .55 .36 13   41 5.4 2.9 110 290
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 900   750   13000 5400 2.7 0   .48 .31 6.1 41 6.5 3.4 120 320
array-examples/standard_copy1_false-unreach-call_ground.i 0 900   720   13000 1800 2.3 0   .50 .31 9.2 40 6.0 3.2 110 310
array-examples/standard_copy2_false-unreach-call_ground.i 0 900   750   12000 2400 2.3 0   .52 .35 3.9 41 6.2 3.3 98 300
array-examples/standard_copy3_false-unreach-call_ground.i 0 900   760   14000 3500 2.3 0   .54 .35 11   42 6.2 3.3 120 310
array-examples/standard_copy4_false-unreach-call_ground.i 0 900   770   13000 5000 2.3 0   .56 .37 11   41 6.4 3.4 110 300
array-examples/standard_copy5_false-unreach-call_ground.i 0 900   780   13000 5100 2.3 0   .50 .34 6.4 39 5.6 3.0 69 290
array-examples/standard_copy6_false-unreach-call_ground.i 0 900   780   13000 5300 2.3 0   .68 .45 8.3 44 6.3 3.3 110 300
array-examples/standard_copy7_false-unreach-call_ground.i 0 900   780   14000 5200 2.3 0   .52 .34 6.4 42 6.0 3.2 120 300
array-examples/standard_copy8_false-unreach-call_ground.i 0 900   790   14000 5300 2.3 0   .55 .35 14   42 5.8 3.1 110 300
array-examples/standard_copy9_false-unreach-call_ground.i 0 900   790   12000 5300 2.3 0   .50 .31 11   40 6.3 3.3 130 300
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 900   770   13000 3300 2.3 0   .48 .31 9.5 39 5.6 3.0 110 300
array-examples/standard_init1_false-unreach-call_ground.i 0 900   710   12000 1700 2.3 0   .56 .36 8.6 42 6.3 3.3 130 300
array-examples/standard_init2_false-unreach-call_ground.i 0 900   730   11000 2300 2.3 0   .52 .33 11   40 5.8 3.1 71 300
array-examples/standard_init3_false-unreach-call_ground.i 0 900   750   13000 2500 2.3 0   .50 .32 6.1 40 6.1 3.3 140 300
array-examples/standard_init4_false-unreach-call_ground.i 0 900   760   14000 3200 2.3 0   .49 .32 12   39 6.0 3.2 110 300
array-examples/standard_init5_false-unreach-call_ground.i 0 900   770   13000 3800 2.3 0   .56 .36 6.3 40 6.4 3.4 130 300
array-examples/standard_init6_false-unreach-call_ground.i 0 900   770   13000 5000 2.3 0   .56 .36 10   44 5.8 3.1 120 310
array-examples/standard_init7_false-unreach-call_ground.i 0 900   780   14000 5000 2.3 0   .57 .36 6.2 40 5.8 3.1 110 290
array-examples/standard_init8_false-unreach-call_ground.i 0 900   770   13000 5300 2.3 0   .46 .31 5.7 40 5.9 3.1 130 310
array-examples/standard_init9_false-unreach-call_ground.i 0 900   780   15000 5200 2.3 0   .59 .38 9.6 39 5.8 3.1 110 300
array-examples/standard_minInArray_false-unreach-call_ground.i 0 900   740   14000 1900 2.3 0   .53 .35 9.5 39 5.6 2.9 61 300
array-examples/standard_partition_false-unreach-call_ground.i 0 900   760   12000 3100 2.3 0   .52 .35 12   40 6.2 3.3 110 300
array-examples/standard_running_false-unreach-call.i 0 900   760   13000 2900 2.3 0   .50 .33 8.1 40 6.0 3.2 120 300
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 7.0 2.2 54 350 2.6 0   4.6  2.5  94   280 9.1 4.9 140 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 900   760   12000 5400 2.3 0   .60 .38 8.9 40 6.7 3.5 110 310
array-examples/relax_true-unreach-call.i 0 900   840   11000 730 2.3 0   .65 .42 9.4 43 6.1 3.2 110 300
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 900   750   12000 2000 2.3 0   .51 .32 12   40 5.3 2.8 79 280
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900   820   12000 1500 2.3 0   .58 .36 9.7 41 5.9 3.1 130 290
array-examples/sanfoundry_24_true-unreach-call.i 2 6.7 2.2 52 350 2.5 0   3.8  2.1  79   280 9.5 5.1 170 350
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 900   730   15000 2000 2.4 0   .51 .33 13   40 5.4 2.9 74 300
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 7.3 2.0 54 350 2.5 0   3.8  2.1  70   270 7.2 3.8 110 310
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 900   730   12000 2300 2.3 0   .55 .35 10   39 6.4 3.4 110 300
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 900   720   13000 2700 2.3 0   .65 .41 9.8 41 6.8 3.6 71 290
array-examples/standard_compareModified_true-unreach-call_ground.i 0 900   730   12000 2100 2.3 0   .64 .41 6.8 39 5.8 3.1 95 300
array-examples/standard_compare_true-unreach-call_ground.i 0 900   720   13000 2000 2.3 0   .62 .39 6.8 40 5.3 2.9 98 290
array-examples/standard_copy1_true-unreach-call_ground.i 0 900   720   13000 1900 2.4 0   .59 .38 11   43 6.1 3.2 120 300
array-examples/standard_copy2_true-unreach-call_ground.i 0 900   750   13000 2800 2.3 0   .51 .32 11   39 5.5 2.9 120 290
array-examples/standard_copy3_true-unreach-call_ground.i 0 900   760   13000 3500 2.3 0   .47 .31 8.1 39 6.3 3.4 74 290
array-examples/standard_copy4_true-unreach-call_ground.i 0 900   770   12000 4900 2.3 0   .56 .35 9.9 45 5.8 3.1 86 300
array-examples/standard_copy5_true-unreach-call_ground.i 0 900   780   15000 5100 2.3 0   .64 .41 8.5 41 5.9 3.2 110 300
array-examples/standard_copy6_true-unreach-call_ground.i 0 900   780   13000 5300 2.3 0   .54 .35 10   40 6.2 3.3 110 310
array-examples/standard_copy7_true-unreach-call_ground.i 0 900   780   14000 5200 2.3 0   .50 .33 11   40 6.1 3.2 130 300
array-examples/standard_copy8_true-unreach-call_ground.i 0 900   790   13000 5200 2.3 0   .50 .32 13   39 5.7 3.0 97 300
array-examples/standard_copy9_true-unreach-call_ground.i 0 900   790   14000 5300 2.3 0   .67 .43 11   43 6.8 3.5 130 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 900   760   13000 3400 2.3 0   .71 .44 8.5 40 5.8 3.1 93 300
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 900   770   13000 4100 2.3 0   .47 .31 11   39 5.9 3.2 120 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 900   760   12000 3100 2.3 0   .50 .32 11   39 5.7 3.0 95 300
array-examples/standard_copyInit_true-unreach-call_ground.i 0 900   750   12000 2300 2.3 0   .52 .34 14   42 5.6 3.0 100 300
array-examples/standard_find_true-unreach-call_ground.i 0 900   720   11000 2100 2.3 0   .65 .40 9.2 41 5.1 2.8 88 290
array-examples/standard_init1_true-unreach-call_ground.i 0 900   710   13000 1700 2.3 0   .61 .39 8.1 39 6.4 3.4 72 300
array-examples/standard_init2_true-unreach-call_ground.i 0 900   740   12000 2000 2.3 0   .51 .33 12   40 5.3 2.8 66 300
array-examples/standard_init3_true-unreach-call_ground.i 0 900   750   13000 2700 2.3 0   .53 .33 13   40 5.9 3.1 85 300
array-examples/standard_init4_true-unreach-call_ground.i 0 900   760   14000 3600 2.5 0   .61 .38 8.1 39 5.8 3.1 120 300
array-examples/standard_init5_true-unreach-call_ground.i 0 900   770   11000 3800 2.3 0   .62 .39 6.8 39 5.8 3.1 120 290
array-examples/standard_init6_true-unreach-call_ground.i 0 900   770   12000 5100 2.3 0   .67 .43 10   44 5.4 2.9 110 280
array-examples/standard_init7_true-unreach-call_ground.i 0 900   770   13000 5200 2.3 0   .50 .32 12   39 6.1 3.3 120 300
array-examples/standard_init8_true-unreach-call_ground.i 0 900   780   14000 5300 2.3 0   .64 .39 7.4 39 5.4 2.9 110 290
array-examples/standard_init9_true-unreach-call_ground.i 0 900   780   14000 5300 2.3 0   .56 .37 12   44 5.9 3.1 110 300
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 900   730   14000 2000 2.3 0   .64 .41 7.7 42 5.6 3.0 75 290
array-examples/standard_minInArray_true-unreach-call_ground.i 0 900   740   13000 1900 2.3 0   .49 .31 11   39 5.9 3.1 110 300
array-examples/standard_palindrome_true-unreach-call_ground.i 0 900   720   12000 2000 2.3 0   .49 .33 12   39 6.2 3.3 130 300
array-examples/standard_partial_init_true-unreach-call_ground.i 0 900   730   12000 2200 2.3 0   .59 .38 9.7 40 5.5 2.9 96 290
array-examples/standard_partition_original_true-unreach-call_ground.i 0 900   730   11000 2200 2.3 0   .72 .45 7.4 43 6.0 3.1 100 300
array-examples/standard_partition_true-unreach-call_ground.i 0 900   770   14000 2800 2.3 0   .57 .36 6.2 42 7.0 3.6 110 310
array-examples/standard_password_true-unreach-call_ground.i 0 900   720   12000 2300 2.3 0   .62 .39 8.4 39 6.0 3.2 110 300
array-examples/standard_reverse_true-unreach-call_ground.i 0 900   720   12000 2000 2.3 0   .65 .43 8.4 40 6.1 3.2 110 310
array-examples/standard_running_true-unreach-call.i 0 900   770   12000 3100 2.3 0   .60 .39 8.6 42 6.3 3.3 92 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 9.6 3.0 71 480 2.5 0   4.4  2.4  47   270 8.1 4.3 160 320
array-examples/standard_seq_init_true-unreach-call_ground.i 0 900   710   14000 1800 2.3 0   .64 .41 7.4 40 6.2 3.3 110 300
array-examples/standard_strcmp_true-unreach-call_ground.i 0 900   720   12000 4300 2.3 0   .65 .41 7.7 40 5.2 2.8 120 290
array-examples/standard_strcpy_original_true-unreach-call.i 0 900   710   12000 1900 2.3 0   .62 .39 9.1 41 6.8 3.6 110 320
array-examples/standard_strcpy_true-unreach-call_ground.i 0 900   710   14000 2000 2.3 0   .62 .40 8.3 39 5.6 3.0 85 300
array-examples/standard_two_index_01_true-unreach-call.i 0 900   740   11000 1500 2.3 0   .67 .42 8.6 40 5.6 3.0 89 290
array-examples/standard_two_index_02_true-unreach-call.i 0 900   740   13000 1500 2.3 0   .60 .38 9.7 41 6.0 3.2 67 300
array-examples/standard_two_index_03_true-unreach-call.i 0 900   740   13000 1500 2.3 0   .68 .43 8.5 40 5.7 3.1 110 290
array-examples/standard_two_index_04_true-unreach-call.i 0 900   740   11000 1600 2.3 0   .64 .41 7.1 39 7.2 3.8 130 320
array-examples/standard_two_index_05_true-unreach-call.i 0 900   740   11000 1500 2.3 0   .66 .42 8.3 40 6.8 3.7 110 330
array-examples/standard_two_index_06_true-unreach-call.i 0 900   740   13000 1500 2.3 0   .52 .33 12   41 7.4 3.9 110 300
array-examples/standard_two_index_07_true-unreach-call.i 0 900   740   12000 1500 2.3 0   .61 .39 7.9 45 5.8 3.0 100 300
array-examples/standard_two_index_08_true-unreach-call.i 0 900   730   12000 1600 2.3 0   .68 .43 7.9 41 7.3 3.8 80 300
array-examples/standard_two_index_09_true-unreach-call.i 0 900   740   12000 1500 2.3 0   .58 .37 9.4 39 5.7 3.0 92 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 900   750   14000 2900 2.3 0   .63 .41 8.4 39 5.9 3.1 100 300
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 900   710   14000 1600 2.3 0   .66 .42 8.5 40 6.1 3.2 130 300
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 0 900   740   14000 1600 2.3 0   .56 .34 8.1 42 5.8 3.1 100 300
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 900   850   8900 5000 2.3 0   .50 .33 9.2 39 5.8 3.1 110 290
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 0 900   770   14000 3400 2.3 0   .47 .30 5.7 39 5.2 2.8 91 280
array-industry-pattern/array_range_init_false-unreach-call.i 0 900   850   9600 4900 2.3 0   .52 .33 13   39 6.3 3.3 130 300
array-industry-pattern/array_single_elem_init_false-unreach-call.i 0 900   770   11000 3400 2.3 0   .49 .31 12   39 5.6 3.0 110 290
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   760   12000 4800 2.3 0   .53 .35 13   40 5.7 3.1 110 300
array-industry-pattern/array_monotonic_true-unreach-call.i 0 900   760   14000 1700 2.3 0   .59 .38 8.7 40 5.3 2.8 69 300
array-industry-pattern/array_mul_init_true-unreach-call.i 0 900   860   9800 3500 2.3 0   .59 .38 8.7 40 5.7 3.0 90 290
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 900   860   8800 5300 2.3 0   .50 .31 11   40 6.1 3.2 110 300
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900   880   7600 5400 2.3 0   .52 .32 12   40 5.7 3.1 98 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 900   750   12000 3100 2.3 0   .62 .39 11   41 6.1 3.3 130 290
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900   880   7600 5400 2.3 0   .58 .37 9.6 40 5.5 3.0 86 300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900   880   7300 5200 2.5 0   .59 .38 8.8 39 5.5 3.0 77 290
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 8.2 2.7 60 310 2.6 0   .49 .31 10   39 5.9 3.2 120 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 900   880   9500 5500 2.3 0   .50 .33 11   41 5.9 3.2 110 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900   880   7800 5400 2.3 0   .53 .34 9.8 40 6.6 3.5 84 290
array-industry-pattern/array_shadowinit_true-unreach-call.i 0 900   740   13000 1600 2.3 0   .52 .33 11   41 6.1 3.2 120 300
reducercommutativity/rangesum05_false-unreach-call.i 1 19   11   190 570 2.6 0   92    87    1200   760 17   10   240 430
reducercommutativity/rangesum10_false-unreach-call.i 1 30   20   290 530 2.6 0   7.5  4.3  76   390 15   8.3 160 530
reducercommutativity/rangesum20_false-unreach-call.i 1 46   32   530 610 2.6 0   91    88    980   760 85   54   730 7000
reducercommutativity/rangesum40_false-unreach-call.i 1 60   37   660 1500 2.7 0   15    9.2  180   650 89   55   630 7000
reducercommutativity/rangesum60_false-unreach-call.i 0 64   40   640 2300 2.7 0   .51 .32 11   40 5.9 3.1 100 300
reducercommutativity/rangesum_false-unreach-call.i 1 20   8.7 190 680 2.6 0   7.4  4.8  71   390 11   5.8 140 380
reducercommutativity/avg05_true-unreach-call.i 0 900   870   13000 1100 2.3 0   .60 .37 8.7 40 6.1 3.2 60 290
reducercommutativity/avg10_true-unreach-call.i 0 900   840   11000 4400 2.3 0   .66 .43 7.4 41 5.9 3.1 82 300
reducercommutativity/avg20_true-unreach-call.i 0 900   800   13000 4700 2.3 0   .52 .33 8.6 41 7.2 3.8 120 310
reducercommutativity/avg40_true-unreach-call.i 0 230   160   2400 4600 2.5 0   .68 .43 8.7 40 5.9 3.2 110 300
reducercommutativity/avg60_true-unreach-call.i 0 440   350   5700 5300 2.5 0   .58 .39 7.9 40 6.2 3.3 110 300
reducercommutativity/avg_true-unreach-call.i 0 900   850   13000 780 2.3 0   .58 .38 8.2 39 6.1 3.2 110 290
reducercommutativity/max05_true-unreach-call_true-termination.i 0 900   870   12000 1400 2.3 0   .59 .38 7.7 40 6.2 3.3 110 290
reducercommutativity/max10_true-unreach-call_true-termination.i 0 900   850   11000 2400 2.3 0   .60 .38 9.5 41 5.8 3.1 68 300
reducercommutativity/max20_true-unreach-call.i 0 900   810   12000 4600 2.3 0   .73 .47 10   40 7.0 3.7 100 320
reducercommutativity/max40_true-unreach-call.i 0 900   790   11000 4700 2.3 0   .68 .43 7.9 41 5.9 3.2 120 290
reducercommutativity/max60_true-unreach-call.i 0 900   750   13000 5100 2.3 0   .61 .39 7.5 40 6.7 3.5 120 300
reducercommutativity/max_true-unreach-call.i 0 900   860   9900 1800 2.3 0   .48 .31 11   40 5.6 3.0 100 290
reducercommutativity/sep05_true-unreach-call.i 0 900   800   11000 4900 2.3 0   .54 .35 11   41 5.6 3.0 110 300
reducercommutativity/sep10_true-unreach-call.i 0 900   700   9500 7400 2.3 0   .54 .34 14   41 5.8 3.1 69 300
reducercommutativity/sep20_true-unreach-call.i 0 900   810   9800 4700 2.3 0   .50 .33 11   40 5.9 3.1 110 300
reducercommutativity/sep40_true-unreach-call.i 0 900   800   11000 4800 2.3 0   .52 .34 9.3 40 5.7 3.0 66 300
reducercommutativity/sep60_true-unreach-call.i 0 900   760   13000 5300 2.3 0   .55 .35 9.7 40 5.6 3.0 100 300
reducercommutativity/sep_true-unreach-call.i 0 900   650   8500 7900 2.3 0   .49 .32 12   40 6.3 3.3 130 300
reducercommutativity/sum05_true-unreach-call_true-termination.i 0 900   880   11000 1100 2.3 0   .54 .35 11   40 6.5 3.4 120 320
reducercommutativity/sum10_true-unreach-call.i 0 900   840   13000 5100 2.3 0   .64 .41 7.0 40 6.0 3.2 120 300
reducercommutativity/sum20_true-unreach-call.i 0 900   800   6800 5000 2.3 0   .50 .33 10   40 5.8 3.1 85 300
reducercommutativity/sum40_true-unreach-call.i 0 900   760   12000 4700 2.3 0   .50 .33 12   41 6.1 3.2 110 290
reducercommutativity/sum60_true-unreach-call.i 0 900   730   11000 6300 2.3 0   .53 .35 11   39 6.0 3.2 100 300
reducercommutativity/sum_true-unreach-call.i 0 900   850   9700 4700 2.3 0   .63 .41 9.9 40 6.4 3.4 99 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 135 13 110000 95000   1500000 440000 320 0   135 230 210 2800 4400   135 420 240 5700 26000   135 70 43   1200 4800   135 580 310 9900 29000  
    correct results 9 13 210 120   2100 5400 23 0   3 210 190 2500 3000   3 220 130 1900 15000   1 17 9.2 290 1100   4 34 18 580 1300  
        correct true 4 8 31 9.3 230 1500 10 0   1 0 0 0 0   0 0 0 0 0   1 17 9.2 290 1100   4 34 18 580 1300  
        correct false 5 5 180 110   1900 3900 13 0   2 210 190 2500 3000   3 220 130 1900 15000   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (135 tasks, max score: 230) 13
Run set sv-comp17.ReachSafety-Arrays