Tool CPAchecker 1.6.1-svn 23987
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; 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-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.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 2.6 1.1 21 280 0     0      .50 .33 5.0 40 5.7 3.0 110 290
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 2.5 1.1 24 280 0     0      .51 .34 12   41 6.0 3.2 110 300
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 2.4 1.0 21 270 0     0      .53 .34 9.6 42 5.6 3.0 99 300
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 2.4 1.0 20 260 0     0      .49 .31 11   40 6.4 3.4 95 300
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 2.5 1.0 22 280 0     0      .46 .31 7.6 40 5.9 3.2 110 300
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 2.5 1.0 23 280 0     0      .48 .32 11   39 7.1 3.7 100 320
array-examples/standard_copy1_false-unreach-call_ground.i 0 2.3 1.0 20 270 0     0      .46 .31 7.1 39 6.2 3.3 110 300
array-examples/standard_copy2_false-unreach-call_ground.i 0 2.3 1.0 22 270 0     0      .51 .32 11   39 6.1 3.2 97 290
array-examples/standard_copy3_false-unreach-call_ground.i 0 2.5 1.1 22 270 0     0      .50 .33 12   39 5.7 3.0 110 280
array-examples/standard_copy4_false-unreach-call_ground.i 0 2.4 1.0 23 260 0     0      .52 .33 13   39 6.3 3.3 120 310
array-examples/standard_copy5_false-unreach-call_ground.i 0 2.5 1.1 22 260 0     0      .55 .37 4.2 44 6.6 3.5 73 300
array-examples/standard_copy6_false-unreach-call_ground.i 0 2.4 1.0 21 260 0     0      .48 .31 9.4 39 5.7 3.1 100 300
array-examples/standard_copy7_false-unreach-call_ground.i 0 2.4 1.0 22 270 0     0      .52 .34 12   39 6.3 3.3 110 300
array-examples/standard_copy8_false-unreach-call_ground.i 0 2.4 1.0 21 270 0     0      .55 .35 9.1 39 5.8 3.1 90 300
array-examples/standard_copy9_false-unreach-call_ground.i 0 2.5 1.1 23 270 0     0      .50 .34 3.8 40 6.0 3.2 96 300
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 2.5 1.0 23 280 0     0      .47 .30 9.8 39 6.1 3.2 100 300
array-examples/standard_init1_false-unreach-call_ground.i 0 2.6 1.1 26 280 0     0      .52 .33 10   43 5.6 2.9 88 300
array-examples/standard_init2_false-unreach-call_ground.i 0 2.6 1.0 26 280 0     0      .49 .32 12   39 7.3 3.8 130 320
array-examples/standard_init3_false-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .50 .31 11   40 5.6 3.0 99 290
array-examples/standard_init4_false-unreach-call_ground.i 0 2.4 1.0 21 260 0     0      .50 .31 13   40 5.8 3.1 97 300
array-examples/standard_init5_false-unreach-call_ground.i 0 2.4 1.1 21 260 0     0      .48 .32 12   39 6.7 3.4 120 300
array-examples/standard_init6_false-unreach-call_ground.i 0 2.6 1.0 23 280 0     0      .50 .32 7.9 39 5.9 3.1 120 300
array-examples/standard_init7_false-unreach-call_ground.i 0 2.6 1.1 20 270 0     0      .50 .31 12   39 6.2 3.3 130 300
array-examples/standard_init8_false-unreach-call_ground.i 0 2.6 1.0 25 270 0     0      .50 .32 9.4 40 6.9 3.6 140 320
array-examples/standard_init9_false-unreach-call_ground.i 0 2.5 1.0 21 270 0     0      .51 .32 13   40 5.7 3.1 130 290
array-examples/standard_minInArray_false-unreach-call_ground.i 0 2.5 1.0 20 280 0     0      .55 .36 9.4 41 5.9 3.1 120 290
array-examples/standard_partition_false-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .50 .32 12   39 6.0 3.2 100 300
array-examples/standard_running_false-unreach-call.i 0 2.6 1.0 21 280 0     .0041 .50 .33 13   41 5.3 2.9 110 300
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 2.7 1.2 22 280 0     5.7    .64 .41 8.9 41 5.3 2.9 100 290
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 2.5 1.1 23 280 0     0      .62 .41 8.5 40 6.1 3.2 120 300
array-examples/relax_true-unreach-call.i 0 7.6 2.4 57 410 .053 0      .53 .35 10   39 6.0 3.2 130 300
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 2.4 1.0 24 270 0     0      .63 .40 7.9 39 6.3 3.3 110 290
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900   820   8800 4200 0     0      .76 .48 9.0 44 6.2 3.3 84 290
array-examples/sanfoundry_24_true-unreach-call.i 0 2.7 1.0 24 270 0     0      .67 .44 8.1 42 6.2 3.3 130 290
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 2.5 1.0 20 280 0     0      .66 .40 7.2 39 6.3 3.3 110 310
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 2.7 1.2 25 280 0     0      3.6  2.0  87   270 8.0 4.2 120 330
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .52 .34 11   40 6.1 3.2 120 310
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 2.6 1.0 21 280 0     0      .53 .34 12   41 6.1 3.2 110 300
array-examples/standard_compareModified_true-unreach-call_ground.i 0 2.6 1.1 24 280 0     0      .60 .39 9.8 39 5.6 3.0 95 290
array-examples/standard_compare_true-unreach-call_ground.i 0 2.6 1.1 22 290 0     5.6    .53 .33 5.4 39 6.3 3.3 120 290
array-examples/standard_copy1_true-unreach-call_ground.i 0 2.4 1.0 20 270 0     0      .71 .45 7.9 40 5.8 3.1 98 290
array-examples/standard_copy2_true-unreach-call_ground.i 0 2.3 1.0 23 260 0     0      .57 .37 9.1 42 7.0 3.7 72 300
array-examples/standard_copy3_true-unreach-call_ground.i 0 2.5 1.0 21 270 0     0      .61 .39 9.8 42 5.7 3.0 110 300
array-examples/standard_copy4_true-unreach-call_ground.i 0 2.4 1.0 23 270 0     0      .62 .40 7.8 39 5.8 3.0 110 290
array-examples/standard_copy5_true-unreach-call_ground.i 0 2.5 1.1 22 270 0     0      .53 .35 12   41 6.3 3.3 130 310
array-examples/standard_copy6_true-unreach-call_ground.i 0 2.6 1.1 22 260 0     0      .61 .39 9.0 41 6.1 3.3 130 300
array-examples/standard_copy7_true-unreach-call_ground.i 0 2.4 1.0 21 260 0     0      .51 .33 11   41 6.7 3.5 110 300
array-examples/standard_copy8_true-unreach-call_ground.i 0 2.5 1.0 23 260 0     0      .52 .34 11   40 7.0 3.7 140 310
array-examples/standard_copy9_true-unreach-call_ground.i 0 2.4 1.1 25 270 0     0      .62 .39 7.8 39 5.9 3.1 100 290
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 2.5 1.0 23 280 0     0      .69 .43 8.5 44 5.5 2.9 100 290
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 2.5 1.0 22 280 0     0      .47 .30 11   39 5.7 3.0 100 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 2.5 1.0 22 280 0     0      .60 .37 8.5 39 6.6 3.4 130 310
array-examples/standard_copyInit_true-unreach-call_ground.i 0 2.7 1.0 21 280 0     0      .65 .40 8.8 39 7.2 3.8 88 310
array-examples/standard_find_true-unreach-call_ground.i 0 2.6 1.0 24 280 0     0      .60 .40 8.5 39 5.8 3.1 100 300
array-examples/standard_init1_true-unreach-call_ground.i 0 2.5 1.0 24 280 0     0      .69 .43 7.3 40 7.1 3.7 69 290
array-examples/standard_init2_true-unreach-call_ground.i 0 2.6 1.1 22 280 0     0      .64 .41 7.9 40 5.9 3.1 110 290
array-examples/standard_init3_true-unreach-call_ground.i 0 2.4 1.0 22 260 0     0      .54 .35 8.1 40 5.9 3.1 130 300
array-examples/standard_init4_true-unreach-call_ground.i 0 2.5 1.0 20 270 0     0      .62 .41 7.9 40 5.6 3.0 88 300
array-examples/standard_init5_true-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .64 .40 8.7 40 7.4 3.9 94 300
array-examples/standard_init6_true-unreach-call_ground.i 0 2.5 1.1 20 260 0     0      .68 .44 7.6 39 6.9 3.7 86 290
array-examples/standard_init7_true-unreach-call_ground.i 0 2.4 1.0 21 260 0     0      .48 .32 12   40 6.6 3.5 130 320
array-examples/standard_init8_true-unreach-call_ground.i 0 2.5 1.0 22 280 0     0      .63 .40 8.4 40 6.8 3.6 130 310
array-examples/standard_init9_true-unreach-call_ground.i 0 2.8 1.1 22 280 0     0      .66 .42 7.6 42 7.0 3.7 110 310
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .54 .34 11   41 7.5 4.0 62 300
array-examples/standard_minInArray_true-unreach-call_ground.i 0 2.5 1.0 19 280 0     0      .69 .45 7.7 40 6.0 3.1 110 300
array-examples/standard_palindrome_true-unreach-call_ground.i 0 2.5 1.0 23 270 0     0      .68 .43 7.9 40 6.9 3.6 130 300
array-examples/standard_partial_init_true-unreach-call_ground.i 0 2.4 1.1 21 270 0     0      .70 .45 7.9 41 6.5 3.4 130 300
array-examples/standard_partition_original_true-unreach-call_ground.i 0 2.6 1.0 21 280 0     0      .50 .32 13   39 6.0 3.2 120 300
array-examples/standard_partition_true-unreach-call_ground.i 0 2.5 1.0 21 280 0     0      .50 .32 9.2 41 6.2 3.3 130 300
array-examples/standard_password_true-unreach-call_ground.i 0 2.6 1.1 23 280 0     0      .63 .39 11   43 5.9 3.1 110 290
array-examples/standard_reverse_true-unreach-call_ground.i 0 2.4 1.0 23 260 0     0      .55 .36 8.1 40 5.4 2.9 93 290
array-examples/standard_running_true-unreach-call.i 0 2.6 1.0 20 280 0     0      .57 .37 14   44 5.8 3.1 110 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 2.4 1.0 23 260 0     0      .64 .41 7.4 40 6.7 3.5 130 320
array-examples/standard_seq_init_true-unreach-call_ground.i 0 2.5 1.0 22 280 0     0      .61 .39 11   43 6.6 3.5 120 310
array-examples/standard_strcmp_true-unreach-call_ground.i 0 2.6 1.1 24 280 0     0      .60 .38 8.5 40 5.8 3.1 120 290
array-examples/standard_strcpy_original_true-unreach-call.i 0 2.4 1.0 21 260 0     0      .51 .33 11   42 6.8 3.6 130 310
array-examples/standard_strcpy_true-unreach-call_ground.i 0 2.4 1.1 24 260 0     0      .64 .40 7.3 41 6.8 3.6 110 290
array-examples/standard_two_index_01_true-unreach-call.i 0 2.4 1.0 20 280 0     0      .63 .40 9.4 42 7.1 3.8 77 300
array-examples/standard_two_index_02_true-unreach-call.i 0 2.4 1.0 22 260 0     0      .54 .33 11   39 6.2 3.3 92 300
array-examples/standard_two_index_03_true-unreach-call.i 0 2.3 1.0 21 270 0     0      .63 .40 7.8 39 5.5 2.9 81 300
array-examples/standard_two_index_04_true-unreach-call.i 0 2.5 1.0 23 280 0     0      .63 .41 8.8 40 6.3 3.3 120 310
array-examples/standard_two_index_05_true-unreach-call.i 0 2.5 1.0 22 270 0     0      .49 .31 9.9 39 5.3 2.9 110 300
array-examples/standard_two_index_06_true-unreach-call.i 0 2.6 1.0 24 280 0     0      .64 .41 6.6 40 5.8 3.1 100 290
array-examples/standard_two_index_07_true-unreach-call.i 0 2.6 1.0 24 280 0     0      .70 .44 7.5 41 6.8 3.6 88 290
array-examples/standard_two_index_08_true-unreach-call.i 0 2.6 1.0 20 270 0     0      .63 .39 9.5 40 5.7 3.0 86 290
array-examples/standard_two_index_09_true-unreach-call.i 0 2.5 1.0 22 280 0     0      .69 .44 7.5 41 6.2 3.3 110 290
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 2.4 1.0 24 260 0     0      .59 .38 10   41 5.7 3.0 76 300
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 2.5 1.0 20 280 0     0      .68 .43 8.9 40 6.5 3.4 98 290
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 0 2.3 1.0 23 260 0     0      .52 .33 9.6 40 5.7 3.0 110 310
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 900   830   11000 4300 0     0      .48 .30 5.4 39 6.0 3.2 100 300
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 0 2.5 1.1 22 280 0     0      .50 .33 8.0 42 5.7 3.1 95 300
array-industry-pattern/array_range_init_false-unreach-call.i 0 2.6 1.0 24 270 0     0      .56 .35 9.7 44 5.9 3.2 110 300
array-industry-pattern/array_single_elem_init_false-unreach-call.i 0 2.6 1.0 21 280 0     0      .55 .35 12   43 6.2 3.3 130 300
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   730   9700 5700 0     0      .51 .33 7.1 41 5.3 2.9 93 290
array-industry-pattern/array_monotonic_true-unreach-call.i 0 2.4 1.1 21 260 0     0      .60 .39 6.9 40 5.6 3.0 87 300
array-industry-pattern/array_mul_init_true-unreach-call.i 0 2.5 1.0 23 270 0     0      .54 .34 13   42 5.7 3.0 120 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 900   840   9600 4300 0     5.7    .61 .40 8.0 40 6.1 3.2 96 300
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900   820   9200 4300 0     0      .59 .38 9.1 40 7.0 3.7 86 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 910   190   4300 11000 0     0      .50 .33 12   40 7.0 3.7 86 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900   820   9000 4300 0     0      .55 .36 9.7 39 5.7 3.0 96 290
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900   820   9700 5000 0     0      .53 .34 10   39 6.0 3.1 110 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 900   810   12000 3900 0     .0041 .49 .32 12   40 5.9 3.1 120 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 900   850   10000 4000 0     0      .49 .32 9.8 40 6.0 3.2 130 290
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900   750   8200 6400 0     0      .62 .39 8.4 40 5.7 3.1 120 290
array-industry-pattern/array_shadowinit_true-unreach-call.i 0 910   400   6400 11000 0     0      .58 .37 8.6 39 6.0 3.2 110 290
reducercommutativity/rangesum05_false-unreach-call.i 1 5.3 2.5 54 390 .016 0      5.8  3.5  110   380 26   17   420 540
reducercommutativity/rangesum10_false-unreach-call.i 1 7.2 3.1 58 410 .020 0      7.1  4.2  92   400 49   33   720 1500
reducercommutativity/rangesum20_false-unreach-call.i 1 13   8.3 130 570 .041 0      9.5  5.6  210   460 64   41   870 7000
reducercommutativity/rangesum40_false-unreach-call.i 1 61   25   450 1900 .074 0      13    7.6  210   610 84   50   620 7000
reducercommutativity/rangesum60_false-unreach-call.i 1 110   70   990 4200 .11  0      15    9.4  110   710 83   49   1100 7000
reducercommutativity/rangesum_false-unreach-call.i 1 13   4.2 100 590 .012 .0041 5.2  3.1  48   380 17   9.3 290 450
reducercommutativity/avg05_true-unreach-call.i 0 900   900   9100 1500 .016 0      .51 .31 10   39 5.8 3.1 120 300
reducercommutativity/avg10_true-unreach-call.i 0 900   900   8700 1900 .025 0      .63 .39 8.1 43 5.9 3.1 110 300
reducercommutativity/avg20_true-unreach-call.i 0 900   900   9700 3600 .041 .025  .64 .40 8.3 40 6.0 3.2 90 290
reducercommutativity/avg40_true-unreach-call.i -16 110   73   1000 3100 .074 0      5.6  3.0  110   300 110   59   1200 7000
reducercommutativity/avg60_true-unreach-call.i -16 560   510   7500 4700 .11  .11   6.5  3.4  95   310 140   80   1400 7000
reducercommutativity/avg_true-unreach-call.i 0 900   780   11000 5300 0     0      .54 .34 11   39 7.1 3.7 130 310
reducercommutativity/max05_true-unreach-call_true-termination.i 0 10   3.5 80 470 .020 .0041 .51 .32 14   39 7.1 3.7 120 320
reducercommutativity/max10_true-unreach-call_true-termination.i 0 500   490   6100 1000 .033 0      .60 .37 7.5 39 5.9 3.1 110 300
reducercommutativity/max20_true-unreach-call.i 0 900   890   13000 1200 .057 0      .63 .40 7.2 40 6.0 3.1 100 310
reducercommutativity/max40_true-unreach-call.i -16 220   180   2300 3300 .11  0      7.6  4.1  87   320 110   64   1800 7000
reducercommutativity/max60_true-unreach-call.i -16 780   720   8200 4800 .16  0      6.6  3.5  82   350 110   62   1200 7000
reducercommutativity/max_true-unreach-call.i 0 530   480   5400 3900 .012 0      .73 .44 8.6 44 6.1 3.2 120 300
reducercommutativity/sep05_true-unreach-call.i 0 44   19   380 1400 .020 0      .49 .33 13   40 6.1 3.2 130 300
reducercommutativity/sep10_true-unreach-call.i 0 38   19   350 960 .033 0      .48 .32 12   40 5.9 3.2 120 300
reducercommutativity/sep20_true-unreach-call.i 0 900   860   12000 4100 .061 0      .57 .36 10   40 7.8 4.1 120 340
reducercommutativity/sep40_true-unreach-call.i -16 600   340   4600 7300 .14  2.3    6.0  3.2  140   310 79   48   1100 7000
reducercommutativity/sep60_true-unreach-call.i 0 900   510   7300 8900 0     0      .68 .43 7.9 43 6.1 3.2 110 300
reducercommutativity/sep_true-unreach-call.i 0 900   760   10000 5800 0     .0041 .61 .39 8.9 40 6.0 3.2 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i 0 900   900   9700 1200 .016 .0041 .62 .39 8.5 40 6.5 3.4 110 300
reducercommutativity/sum10_true-unreach-call.i 0 900   900   11000 1700 .025 0      .66 .40 6.4 39 6.0 3.1 130 300
reducercommutativity/sum20_true-unreach-call.i 0 900   900   11000 2600 .041 0      .49 .32 11   39 6.5 3.4 100 290
reducercommutativity/sum40_true-unreach-call.i -16 88   56   870 2900 .074 0      5.3  2.9  78   300 110   59   760 7000
reducercommutativity/sum60_true-unreach-call.i -16 240   190   2400 4600 .11  0      6.7  3.6  75   310 74   43   1300 7000
reducercommutativity/sum_true-unreach-call.i 0 160   140   2200 3600 .012 0      .57 .37 9.8 42 5.8 3.1 100 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 -104 25000   21000   270000 180000 1.5  20      135 72 45 1100 4300   135 530 310 7700 34000   135 100   59   1600 6000   135 1300   710   18000 75000  
    correct results 7 8 210   110   1800 8300 .27 .0041 6 55 33 790 2900   3 320 200 4000 23000   1 3.6 2.0 87 270   1 8.0 4.2 120 330  
        correct true 1 2 2.7 1.2 25 280 0    0      0 0 0 0 0   0 0 0 0 0   1 3.6 2.0 87 270   1 8.0 4.2 120 330  
        correct false 6 6 210   110   1800 8000 .27 .0041 6 55 33 790 2900   3 320 200 4000 23000   0 0   0   0 0   0 0   0   0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 7 -112 2600   2100   27000 31000 .78 2.5    0 0 0 0 0   0 0 0 0 0   7 44   24   660 2200   0 730   410   8700 49000  
        incorrect true 0
        incorrect false 7 -112 2600   2100   27000 31000 .78 2.5    0 0 0 0 0   0 0 0 0 0   0 44   24   660 2200   0 730   410   8700 49000  
score (135 tasks, max score: 230) -104
Run set sv-comp17.ReachSafety-Arrays