Tool ULTIMATE Kojak 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-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.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   740   12000 5200 2.9 11    .67 .43 9.1 44 5.7 3.1 120 300
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 900   730   12000 4400 2.3 0    .57 .37 9.2 40 6.0 3.2 110 300
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 900   720   13000 3900 2.3 0    .58 .37 9.3 41 5.3 2.9 100 280
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 900   730   14000 3400 2.3 0    .53 .34 11   40 5.1 2.8 100 290
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 900   730   12000 2600 2.3 0    .51 .34 8.8 40 5.9 3.2 110 300
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 900   750   13000 2300 2.3 0    .54 .35 13   40 6.3 3.3 120 300
array-examples/standard_copy1_false-unreach-call_ground.i 0 900   730   14000 3500 2.3 0    .52 .33 9.4 40 5.9 3.2 120 300
array-examples/standard_copy2_false-unreach-call_ground.i 0 900   730   13000 3400 2.3 0    .53 .33 13   41 5.7 3.0 120 290
array-examples/standard_copy3_false-unreach-call_ground.i 0 900   730   12000 3600 2.3 0    .51 .34 7.1 40 6.5 3.4 130 310
array-examples/standard_copy4_false-unreach-call_ground.i 0 900   720   12000 4300 2.3 0    .49 .31 10   39 6.6 3.5 100 310
array-examples/standard_copy5_false-unreach-call_ground.i 0 900   730   13000 3800 2.3 0    .61 .38 9.7 39 5.8 3.1 110 300
array-examples/standard_copy6_false-unreach-call_ground.i 0 900   730   13000 4800 2.3 0    .52 .33 8.9 40 5.9 3.1 100 300
array-examples/standard_copy7_false-unreach-call_ground.i 0 900   720   15000 2900 2.3 0    .47 .31 10   40 6.3 3.3 140 300
array-examples/standard_copy8_false-unreach-call_ground.i 0 900   730   12000 2400 2.3 0    .53 .34 14   40 6.0 3.2 120 300
array-examples/standard_copy9_false-unreach-call_ground.i 0 900   730   13000 3600 2.3 0    .50 .33 12   39 6.1 3.2 91 300
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 900   730   12000 2500 2.3 0    .55 .34 10   43 5.6 3.0 110 300
array-examples/standard_init1_false-unreach-call_ground.i 0 900   730   13000 2500 2.3 0    .52 .33 13   41 5.7 3.1 99 300
array-examples/standard_init2_false-unreach-call_ground.i 0 900   730   15000 3900 2.3 0    .51 .34 11   39 6.0 3.2 120 300
array-examples/standard_init3_false-unreach-call_ground.i 0 900   730   12000 4100 2.3 0    .50 .32 6.9 41 6.3 3.3 120 310
array-examples/standard_init4_false-unreach-call_ground.i 0 900   730   12000 3700 2.3 0    .63 .40 7.2 39 6.0 3.2 110 300
array-examples/standard_init5_false-unreach-call_ground.i 0 900   730   12000 3100 2.3 0    .68 .43 8.4 40 6.0 3.2 130 300
array-examples/standard_init6_false-unreach-call_ground.i 0 900   720   14000 3100 2.3 0    .51 .33 11   42 5.9 3.2 130 290
array-examples/standard_init7_false-unreach-call_ground.i 0 900   730   12000 4200 2.3 0    .49 .33 12   40 5.2 2.8 89 290
array-examples/standard_init8_false-unreach-call_ground.i 0 900   720   13000 4500 2.3 0    .52 .35 8.8 40 6.3 3.3 120 310
array-examples/standard_init9_false-unreach-call_ground.i 0 900   730   15000 4000 2.3 0    .51 .32 10   40 6.2 3.3 130 300
array-examples/standard_minInArray_false-unreach-call_ground.i 0 900   730   14000 2800 2.3 0    .52 .33 7.5 41 6.0 3.2 120 300
array-examples/standard_partition_false-unreach-call_ground.i 0 900   720   12000 3800 2.3 0    .53 .34 10   41 5.8 3.1 110 300
array-examples/standard_running_false-unreach-call.i 0 900   720   14000 3100 2.3 0    .50 .32 9.2 39 5.7 3.0 110 290
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 900   760   12000 2200 2.3 0    .49 .32 11   39 6.6 3.5 110 310
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 900   740   13000 5200 2.3 0    .52 .33 12   40 7.1 3.8 80 300
array-examples/relax_true-unreach-call.i 0 900   890   11000 540 2.3 0    .51 .33 10   39 6.1 3.2 110 310
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 900   730   14000 3900 2.3 0    .52 .34 12   42 5.6 3.0 110 290
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900   750   11000 1300 2.3 0    .65 .42 8.2 40 5.9 3.1 120 300
array-examples/sanfoundry_24_true-unreach-call.i 2 6.7 2.1 55 320 2.5 0    5.0  2.8  56   270 9.5 5.3 190 350
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 900   730   14000 3200 2.3 0    .54 .35 10   40 6.2 3.3 120 300
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 5.9 1.8 47 320 2.5 0    3.5  1.9  66   270 7.4 3.9 160 310
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 900   720   13000 3000 2.3 0    .50 .33 9.7 39 5.8 3.1 120 300
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 900   730   14000 3800 2.3 0    .54 .35 10   40 6.2 3.3 120 300
array-examples/standard_compareModified_true-unreach-call_ground.i 0 900   730   12000 4900 2.3 0    .69 .44 7.8 41 5.5 3.0 88 300
array-examples/standard_compare_true-unreach-call_ground.i 0 900   720   13000 2500 2.3 0    .66 .41 8.8 39 6.5 3.4 110 310
array-examples/standard_copy1_true-unreach-call_ground.i 0 900   720   14000 3500 2.3 0    .55 .35 8.3 40 6.0 3.2 120 300
array-examples/standard_copy2_true-unreach-call_ground.i 0 900   730   15000 3700 2.3 0    .65 .42 6.5 39 5.5 2.9 98 290
array-examples/standard_copy3_true-unreach-call_ground.i 0 900   730   11000 4000 2.3 0    .53 .34 10   40 5.9 3.1 100 300
array-examples/standard_copy4_true-unreach-call_ground.i 0 900   730   12000 4500 2.3 0    .49 .33 11   39 6.8 3.5 130 320
array-examples/standard_copy5_true-unreach-call_ground.i 0 900   730   13000 3000 2.3 0    .54 .34 9.2 39 5.6 3.0 94 290
array-examples/standard_copy6_true-unreach-call_ground.i 0 900   720   13000 3600 2.3 0    .59 .38 11   40 6.3 3.3 100 300
array-examples/standard_copy7_true-unreach-call_ground.i 0 900   730   12000 3900 2.3 0    .64 .41 8.3 41 5.7 3.1 85 300
array-examples/standard_copy8_true-unreach-call_ground.i 0 900   730   14000 3800 2.3 0    .62 .40 6.9 40 6.8 3.5 110 310
array-examples/standard_copy9_true-unreach-call_ground.i 0 900   720   12000 3400 2.3 0    .62 .38 8.4 39 6.1 3.2 120 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 900   720   12000 3300 2.3 0    .55 .36 10   40 6.3 3.3 140 310
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 900   720   14000 3800 2.3 0    .51 .32 12   39 5.9 3.2 120 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 900   730   13000 2600 2.3 0    .54 .35 11   41 6.2 3.3 89 310
array-examples/standard_copyInit_true-unreach-call_ground.i 0 900   730   14000 2700 2.3 0    .66 .42 7.8 42 5.6 3.0 62 300
array-examples/standard_find_true-unreach-call_ground.i 0 900   720   11000 3800 2.3 0    .53 .34 11   40 5.8 3.0 77 290
array-examples/standard_init1_true-unreach-call_ground.i 0 900   720   13000 3400 2.3 0    .54 .34 12   41 5.6 3.0 96 300
array-examples/standard_init2_true-unreach-call_ground.i 0 900   730   13000 4000 2.3 0    .56 .36 7.8 40 6.4 3.4 69 310
array-examples/standard_init3_true-unreach-call_ground.i 0 900   730   13000 3100 2.3 0    .48 .32 11   40 6.1 3.2 110 310
array-examples/standard_init4_true-unreach-call_ground.i 0 900   730   15000 4900 2.3 0    .66 .41 10   45 5.9 3.1 110 300
array-examples/standard_init5_true-unreach-call_ground.i 0 900   730   14000 3400 2.3 0    .65 .43 9.2 41 6.3 3.4 120 310
array-examples/standard_init6_true-unreach-call_ground.i 0 900   730   12000 3200 2.3 0    .50 .34 12   44 6.1 3.2 98 310
array-examples/standard_init7_true-unreach-call_ground.i 0 900   730   14000 3700 2.3 0    .59 .36 7.0 40 6.1 3.2 110 310
array-examples/standard_init8_true-unreach-call_ground.i 0 900   730   13000 3300 2.3 0    .67 .42 9.4 43 6.3 3.3 110 320
array-examples/standard_init9_true-unreach-call_ground.i 0 900   720   13000 3700 2.3 0    .57 .35 11   40 5.9 3.1 110 290
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 900   720   14000 3200 2.3 0    .52 .34 10   42 5.7 3.0 93 290
array-examples/standard_minInArray_true-unreach-call_ground.i 0 900   720   13000 3800 2.3 0    .50 .32 12   39 6.0 3.2 100 300
array-examples/standard_palindrome_true-unreach-call_ground.i 0 900   730   12000 3000 2.3 0    .64 .40 8.9 40 4.9 2.7 48 280
array-examples/standard_partial_init_true-unreach-call_ground.i 0 900   720   14000 4400 2.3 0    .65 .41 8.8 40 5.7 3.1 110 290
array-examples/standard_partition_original_true-unreach-call_ground.i 0 900   730   13000 4100 2.3 0    .70 .45 6.4 40 6.1 3.3 100 310
array-examples/standard_partition_true-unreach-call_ground.i 0 900   720   13000 2500 2.3 0    .82 .51 6.5 40 5.9 3.1 110 290
array-examples/standard_password_true-unreach-call_ground.i 0 900   720   13000 2100 2.3 0    .56 .36 8.2 39 5.9 3.1 89 300
array-examples/standard_reverse_true-unreach-call_ground.i 0 900   730   13000 3600 2.3 0    .50 .32 10   39 5.6 3.0 110 300
array-examples/standard_running_true-unreach-call.i 0 900   720   13000 2800 2.3 0    .61 .39 10   43 6.1 3.3 82 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 6.6 2.1 56 320 2.5 0    3.9  2.2  75   270 9.0 4.8 96 320
array-examples/standard_seq_init_true-unreach-call_ground.i 0 900   720   11000 2400 2.3 0    .62 .41 8.4 39 6.2 3.3 110 310
array-examples/standard_strcmp_true-unreach-call_ground.i 0 900   730   12000 5200 2.3 0    .51 .32 12   40 6.9 3.6 100 320
array-examples/standard_strcpy_original_true-unreach-call.i 0 900   730   13000 4700 2.3 0    .56 .36 9.0 40 6.7 3.5 130 320
array-examples/standard_strcpy_true-unreach-call_ground.i 0 900   720   15000 3200 2.3 0    .49 .32 8.4 40 6.0 3.2 110 300
array-examples/standard_two_index_01_true-unreach-call.i 0 900   720   12000 2800 2.3 0    .57 .36 9.8 40 6.3 3.3 120 310
array-examples/standard_two_index_02_true-unreach-call.i 0 900   730   12000 4200 2.3 0    .62 .40 6.8 40 5.5 2.9 99 290
array-examples/standard_two_index_03_true-unreach-call.i 0 900   720   12000 2700 2.3 0    .48 .31 10   40 5.9 3.1 110 310
array-examples/standard_two_index_04_true-unreach-call.i 0 900   720   13000 3800 2.3 0    .49 .31 12   39 6.0 3.2 110 300
array-examples/standard_two_index_05_true-unreach-call.i 0 900   720   14000 3300 2.3 0    .59 .38 10   42 5.8 3.1 120 290
array-examples/standard_two_index_06_true-unreach-call.i 0 900   730   13000 3800 2.3 0    .49 .31 10   40 5.6 3.0 110 290
array-examples/standard_two_index_07_true-unreach-call.i 0 900   730   13000 4300 2.3 0    .57 .36 10   39 5.2 2.8 67 290
array-examples/standard_two_index_08_true-unreach-call.i 0 900   730   12000 3900 2.3 0    .60 .37 7.7 39 5.6 3.0 110 290
array-examples/standard_two_index_09_true-unreach-call.i 0 900   720   14000 3100 2.3 0    .51 .33 12   40 5.9 3.1 130 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 900   840   13000 850 2.3 0    .66 .42 7.9 40 6.1 3.2 74 310
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 900   730   12000 4400 2.3 0    .52 .33 10   40 6.8 3.6 140 320
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 0 900   730   13000 3300 2.3 0    .51 .33 12   40 6.0 3.2 120 300
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 900   860   10000 5200 2.3 0    .53 .34 4.2 40 5.8 3.1 100 300
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 0 900   720   13000 3700 2.3 0    .65 .41 8.7 40 6.6 3.4 110 310
array-industry-pattern/array_range_init_false-unreach-call.i 0 900   850   9700 4900 2.3 0    .49 .33 11   42 5.9 3.2 120 310
array-industry-pattern/array_single_elem_init_false-unreach-call.i 0 900   730   15000 5200 2.3 0    .50 .33 8.7 41 5.7 3.0 100 290
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   760   13000 5300 2.3 0    .53 .34 11   41 6.7 3.5 96 300
array-industry-pattern/array_monotonic_true-unreach-call.i 0 900   720   13000 2700 2.3 0    .61 .40 7.8 40 5.5 2.9 120 300
array-industry-pattern/array_mul_init_true-unreach-call.i 0 900   720   15000 3600 2.3 0    .51 .33 8.5 40 5.5 2.9 85 290
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 900   860   9000 5200 2.3 0    .66 .42 7.7 41 6.0 3.2 130 300
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900   870   8600 5500 2.3 0    .66 .43 8.1 40 5.7 3.1 120 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 900   740   13000 3800 2.3 0    .65 .40 8.8 40 5.9 3.1 120 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900   870   7100 5400 2.3 0    .51 .33 12   41 5.9 3.1 130 300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900   870   8000 5200 2.3 0    .59 .37 9.2 40 6.0 3.2 100 290
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 8.0 2.6 66 300 2.6 0    .50 .32 11   39 5.7 3.0 96 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 900   880   8300 5500 2.3 0    .56 .36 11   43 6.2 3.3 120 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900   870   9800 5500 2.3 0    .56 .36 10   41 5.7 3.0 86 300
array-industry-pattern/array_shadowinit_true-unreach-call.i 0 900   830   12000 920 2.3 0    .53 .33 11   40 5.7 3.0 89 290
reducercommutativity/rangesum05_false-unreach-call.i 1 9.4 2.8 74 490 2.6 0    91    89    860   540 17   10   240 420
reducercommutativity/rangesum10_false-unreach-call.i 1 13   3.8 110 490 2.6 0    6.6  4.0  140   390 15   8.3 210 540
reducercommutativity/rangesum20_false-unreach-call.i 1 26   8.1 240 670 2.6 0    91    88    940   670 77   49   700 7000
reducercommutativity/rangesum40_false-unreach-call.i 0 900   800   9100 1500 2.5 0    .54 .36 12   39 6.4 3.4 120 300
reducercommutativity/rangesum60_false-unreach-call.i 0 900   800   8700 2400 2.5 0    .51 .33 11   40 6.3 3.3 120 300
reducercommutativity/rangesum_false-unreach-call.i 0 900   590   11000 1200 2.3 0    .50 .32 9.8 39 6.3 3.3 110 300
reducercommutativity/avg05_true-unreach-call.i 0 900   830   6300 5600 2.9 0    .66 .42 8.4 41 5.3 2.9 99 290
reducercommutativity/avg10_true-unreach-call.i 0 900   860   11000 1300 2.7 0    5.5  3.0  48   270 310   270   4000 1600
reducercommutativity/avg20_true-unreach-call.i 0 900   840   13000 1900 2.3 0    .63 .41 7.8 40 6.2 3.3 95 310
reducercommutativity/avg40_true-unreach-call.i 0 900   780   11000 4000 2.3 .15 .51 .33 11   43 6.7 3.5 95 310
reducercommutativity/avg60_true-unreach-call.i 0 750   660   10000 4700 2.5 0    .64 .40 9.8 42 5.8 3.1 100 290
reducercommutativity/avg_true-unreach-call.i 0 900   890   12000 580 2.3 0    .64 .40 8.4 40 5.9 3.1 110 300
reducercommutativity/max05_true-unreach-call_true-termination.i 0 900   790   14000 2200 2.3 0    .66 .42 6.6 40 6.2 3.3 100 310
reducercommutativity/max10_true-unreach-call_true-termination.i 0 900   850   11000 3300 2.3 0    .61 .39 8.6 40 5.1 2.8 76 290
reducercommutativity/max20_true-unreach-call.i 0 900   830   7100 4600 2.3 0    .65 .42 9.0 41 7.3 3.9 100 300
reducercommutativity/max40_true-unreach-call.i 0 900   750   8700 6000 2.3 0    .60 .38 10   42 6.2 3.3 110 300
reducercommutativity/max60_true-unreach-call.i 0 900   740   10000 6100 2.3 0    .61 .38 9.9 39 6.1 3.2 130 300
reducercommutativity/max_true-unreach-call.i 0 900   810   13000 1900 2.3 0    .57 .36 13   43 5.9 3.1 120 300
reducercommutativity/sep05_true-unreach-call.i 2 290   250   3900 1900 2.7 0    4.5  2.5  81   270 200   140   2000 3300
reducercommutativity/sep10_true-unreach-call.i 0 900   810   12000 2500 2.3 0    .58 .38 9.2 40 6.1 3.2 100 300
reducercommutativity/sep20_true-unreach-call.i 0 910   490   7700 13000 2.3 0    .51 .33 13   40 6.0 3.2 120 300
reducercommutativity/sep40_true-unreach-call.i 0 900   420   8000 13000 2.3 0    .57 .36 12   43 5.7 3.0 96 290
reducercommutativity/sep60_true-unreach-call.i 0 900   490   9600 12000 2.3 0    .58 .38 8.6 40 5.2 2.8 53 290
reducercommutativity/sep_true-unreach-call.i 0 900   810   11000 1700 2.3 0    .67 .43 8.2 41 5.9 3.1 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 24   12   240 720 2.6 0    3.7  2.1  69   270 32   20   390 700
reducercommutativity/sum10_true-unreach-call.i 2 88   63   950 1200 2.6 .21 4.3  2.4  67   270 100   64   1900 1100
reducercommutativity/sum20_true-unreach-call.i 2 790   740   9800 2600 2.8 0    4.1  2.3  75   270 960   910   9200 5200
reducercommutativity/sum40_true-unreach-call.i 0 900   740   11000 4700 2.3 0    .49 .31 10   40 5.5 2.9 120 290
reducercommutativity/sum60_true-unreach-call.i 0 900   730   13000 4900 2.3 0    .56 .36 8.9 39 6.1 3.2 120 300
reducercommutativity/sum_true-unreach-call.i 0 900   840   11000 990 2.3 0    .64 .42 7.9 41 6.1 3.2 120 310
../../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 17 110000 93000 1500000 470000 320   11    135 210 190 2300 3100   135 330 190 5300 19000   135 85 51 1400 5700   135 2200 1700 27000 39000  
    correct results 10 17 1300 1100 15000 9100 26   .21 1 190 180 1900 1600   2 110 68 1100 8000   1 29 16 490 1900   6 1300 1100 14000 11000  
        correct true 7 14 1200 1100 15000 7500 18   .21 1 0 0 0 0   0 0 0 0 0   1 29 16 490 1900   6 1300 1100 14000 11000  
        correct false 3 3 49 15 420 1600 7.8 0    0 190 180 1900 1600   2 110 68 1100 8000   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) 17
Run set sv-comp17.ReachSafety-Arrays