Tool Ceagle Ceagle 1.3 @ 53cfa89
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.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 1 .058 .068 .41 11   0   2.7   3.3 1.8 63 270 9.3 4.9 94 320
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 1 24     24     250    8.3 0   0     3.6 2.0 72 270 8.2 4.3 120 320
array-examples/sorting_bubblesort_false-unreach-call_ground.i 1 18     18     230    11   0   2.4   3.3 1.8 78 270 8.9 4.7 83 320
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 1 .067 .077 .36 11   0   2.5   3.2 1.8 61 270 7.6 4.0 130 320
array-examples/sorting_selectionsort_false-unreach-call_ground.i 1 .056 .073 .56 13   0   4.7   3.4 1.9 74 270 7.3 3.9 130 320
array-examples/standard_allDiff2_false-unreach-call_ground.i 1 9.2   9.2   130    11   0   2.5   3.1 1.8 61 260 7.2 3.9 120 320
array-examples/standard_copy1_false-unreach-call_ground.i 1 .053 .056 .31 9.3 0   .89  3.2 1.8 54 270 8.6 4.5 84 310
array-examples/standard_copy2_false-unreach-call_ground.i 1 .082 .091 .33 11   0   2.5   3.4 1.9 65 280 9.7 5.1 98 330
array-examples/standard_copy3_false-unreach-call_ground.i 1 .052 .061 .43 11   0   2.4   3.3 1.9 75 270 12   6.1 99 340
array-examples/standard_copy4_false-unreach-call_ground.i 1 .044 .045 .41 8.2 0   0     3.4 1.9 54 270 9.0 4.7 130 320
array-examples/standard_copy5_false-unreach-call_ground.i 1 .076 .076 .33 8.3 0   0     3.3 1.9 70 270 7.2 3.9 110 320
array-examples/standard_copy6_false-unreach-call_ground.i 1 .053 .053 .38 8.4 0   0     3.4 1.9 71 270 8.7 4.6 100 310
array-examples/standard_copy7_false-unreach-call_ground.i 1 .050 .060 .41 11   0   2.5   3.2 1.8 72 270 7.7 4.1 130 320
array-examples/standard_copy8_false-unreach-call_ground.i 1 .062 .078 .45 12   0   4.7   3.4 1.9 59 270 7.3 3.9 160 320
array-examples/standard_copy9_false-unreach-call_ground.i 1 .055 .065 .46 11   0   2.4   3.4 1.9 75 280 7.1 3.8 160 320
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 1 .049 .051 .37 8.6 0   .025 3.4 1.9 77 280 7.3 3.9 140 320
array-examples/standard_init1_false-unreach-call_ground.i 1 .061 .070 .45 11   0   2.4   3.1 1.8 67 270 6.7 3.6 120 310
array-examples/standard_init2_false-unreach-call_ground.i 1 .056 .071 .47 13   0   4.7   3.4 1.9 64 260 8.1 4.3 74 310
array-examples/standard_init3_false-unreach-call_ground.i 1 .051 .060 .42 11   0   2.5   3.3 1.8 73 270 8.3 4.5 88 310
array-examples/standard_init4_false-unreach-call_ground.i 1 .090 .22  .97 49   0   41     3.3 1.9 74 260 8.4 4.5 120 330
array-examples/standard_init5_false-unreach-call_ground.i 1 .077 .086 .28 11   0   2.4   3.2 1.8 47 280 6.9 3.7 150 320
array-examples/standard_init6_false-unreach-call_ground.i 1 .051 .051 .38 8.3 0   0     3.2 1.8 59 270 8.8 4.6 100 320
array-examples/standard_init7_false-unreach-call_ground.i 1 .063 .072 .46 11   0   2.5   3.3 1.9 64 260 7.3 3.9 110 310
array-examples/standard_init8_false-unreach-call_ground.i 1 .075 .086 .39 11   0   2.4   3.4 1.9 70 270 8.8 4.7 95 320
array-examples/standard_init9_false-unreach-call_ground.i 1 .052 .053 .35 8.4 0   0     3.3 1.8 64 260 7.5 4.0 150 320
array-examples/standard_minInArray_false-unreach-call_ground.i 1 .049 .059 .44 11   0   2.4   3.2 1.8 54 270 8.5 4.6 110 320
array-examples/standard_partition_false-unreach-call_ground.i 1 .046 .047 .38 8.2 0   0     3.5 1.9 68 270 7.9 4.2 130 320
array-examples/standard_running_false-unreach-call.i 1 .052 .070 .60 13   0   4.7   3.5 2.0 70 280 7.3 3.9 130 330
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 .055 .065 .47 11   0   2.6   4.6  2.5  81   280 8.9 4.9 170 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 2 .068 .080 .42 11   0   2.6   4.3  2.4  65   270 960   830   19000 4800
array-examples/relax_true-unreach-call.i 0 .031 .033 .14 8.2 0   .045 .59 .40 8.8 40 6.1 3.3 100 300
array-examples/sanfoundry_02_true-unreach-call_ground.i 2 .047 .047 .49 8.5 0   0     3.8  2.1  75   270 960   840   32000 3300
array-examples/sanfoundry_10_true-unreach-call_ground.i 2 .067 .084 .37 13   0   4.0   700    660    12000   7000 960   790   15000 3100
array-examples/sanfoundry_24_true-unreach-call.i 0 .027 .028 .11 7.8 0   0     .55 .35 13   44 6.4 3.4 110 310
array-examples/sanfoundry_27_true-unreach-call_ground.i 2 .11  .11  .30 8.3 0   0     3.7  2.0  74   270 960   820   23000 3800
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 .12  .13  .35 11   0   2.4   3.9  2.2  48   270 6.9 3.6 120 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i 2 26     26     300    12   0   4.6   3.5  2.0  72   270 960   820   31000 3800
array-examples/sorting_selectionsort_true-unreach-call_ground.i 2 .45  .46  5.2  11   0   2.4   4.5  2.5  48   270 960   790   16000 3900
array-examples/standard_compareModified_true-unreach-call_ground.i 2 .048 .048 .42 8.2 0   0     3.7  2.1  50   280 960   820   25000 3900
array-examples/standard_compare_true-unreach-call_ground.i 2 .070 .079 .39 11   0   2.4   3.4  1.9  58   270 960   810   14000 4500
array-examples/standard_copy1_true-unreach-call_ground.i 2 .056 .056 .40 8.4 0   0     4.4  2.5  52   270 960   800   23000 4000
array-examples/standard_copy2_true-unreach-call_ground.i 2 .051 .051 .34 8.2 0   0     3.8  2.1  85   270 960   840   21000 4300
array-examples/standard_copy3_true-unreach-call_ground.i 2 .059 .060 .39 8.5 0   .074 3.7  2.1  76   270 960   860   23000 4800
array-examples/standard_copy4_true-unreach-call_ground.i 2 .053 .053 .36 8.4 0   0     4.8  2.7  54   270 960   860   17000 4700
array-examples/standard_copy5_true-unreach-call_ground.i 2 .075 .091 .45 13   0   4.7   3.9  2.2  78   270 960   860   24000 4600
array-examples/standard_copy6_true-unreach-call_ground.i 2 .063 .072 .34 11   0   2.4   4.9  2.7  48   270 960   870   22000 4800
array-examples/standard_copy7_true-unreach-call_ground.i 2 .047 .047 .34 8.3 0   0     4.5  2.5  51   270 960   860   24000 4800
array-examples/standard_copy8_true-unreach-call_ground.i 2 .078 .087 .34 11   0   2.4   4.8  2.6  55   270 960   860   21000 5000
array-examples/standard_copy9_true-unreach-call_ground.i 2 .082 .092 .45 11   0   2.5   4.8  2.6  48   270 960   870   28000 4700
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 .051 .061 .42 11   0   2.4   4.8  2.7  43   270 960   860   21000 4700
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 .061 .072 .33 11   0   2.4   3.8  2.1  73   280 960   860   25000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 .058 .059 .32 8.5 0   .025 3.7  2.0  42   270 960   850   24000 4500
array-examples/standard_copyInit_true-unreach-call_ground.i 2 .052 .052 .39 8.4 0   0     3.7  2.1  68   270 960   840   16000 4500
array-examples/standard_find_true-unreach-call_ground.i 2 .046 .057 .54 11   0   2.5   3.8  2.1  85   280 960   800   13000 4300
array-examples/standard_init1_true-unreach-call_ground.i 2 .053 .062 .42 11   0   2.4   3.7  2.1  67   290 960   790   23000 3700
array-examples/standard_init2_true-unreach-call_ground.i 2 .058 .058 .32 8.2 0   0     4.1  2.3  48   270 960   820   24000 3400
array-examples/standard_init3_true-unreach-call_ground.i 2 .10  .11  .34 11   0   2.5   3.6  2.0  70   270 960   840   27000 4400
array-examples/standard_init4_true-unreach-call_ground.i 2 .067 .067 .36 8.4 0   0     4.1  2.3  68   270 960   850   28000 4800
array-examples/standard_init5_true-unreach-call_ground.i 2 .073 .089 .43 13   0   4.7   4.6  2.6  52   270 960   860   20000 4800
array-examples/standard_init6_true-unreach-call_ground.i 2 .049 .049 .39 8.2 0   0     4.2  2.3  76   290 960   860   18000 4700
array-examples/standard_init7_true-unreach-call_ground.i 2 .054 .064 .42 11   0   2.3   3.8  2.1  60   270 960   860   21000 4700
array-examples/standard_init8_true-unreach-call_ground.i 2 .058 .074 .52 13   0   4.7   4.1  2.3  55   280 960   870   25000 4700
array-examples/standard_init9_true-unreach-call_ground.i 2 .087 .10  .41 11   0   2.4   4.8  2.7  69   280 960   860   18000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i 2 .078 .094 .39 13   0   4.7   3.4  1.9  48   270 960   820   22000 4100
array-examples/standard_minInArray_true-unreach-call_ground.i 2 .067 .077 .36 11   0   2.5   4.4  2.5  51   270 960   820   13000 4400
array-examples/standard_palindrome_true-unreach-call_ground.i 2 .059 .076 .36 13   0   4.6   3.6  2.1  75   270 960   800   18000 4200
array-examples/standard_partial_init_true-unreach-call_ground.i 2 .074 .084 .40 11   0   2.5   3.8  2.1  76   270 960   820   24000 3600
array-examples/standard_partition_original_true-unreach-call_ground.i 2 .092 .092 .31 8.2 0   0     3.6  2.0  77   270 960   820   15000 4300
array-examples/standard_partition_true-unreach-call_ground.i 2 .098 .11  .31 11   0   2.5   4.0  2.3  61   270 960   850   16000 4800
array-examples/standard_password_true-unreach-call_ground.i 2 .071 .084 .39 11   0   2.4   3.8  2.1  68   280 960   800   23000 4500
array-examples/standard_reverse_true-unreach-call_ground.i 2 .053 .070 .44 13   0   4.7   4.4  2.5  56   270 960   800   21000 3800
array-examples/standard_running_true-unreach-call.i 2 .077 .087 .39 11   0   2.4   4.4  2.5  69   270 960   860   21000 4700
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 .066 .076 .41 11   0   2.6   3.6  2.0  60   280 13   6.9 260 390
array-examples/standard_seq_init_true-unreach-call_ground.i 2 .091 .091 .23 8.1 0   0     3.6  2.0  55   270 960   790   17000 3600
array-examples/standard_strcmp_true-unreach-call_ground.i 2 .058 .068 .47 11   0   2.5   3.9  2.2  65   270 960   810   29000 5000
array-examples/standard_strcpy_original_true-unreach-call.i 0 .027 .027 .12 7.9 0   0     .49 .32 12   39 6.4 3.4 110 300
array-examples/standard_strcpy_true-unreach-call_ground.i 0 .043 .043 .11 7.7 0   0     .65 .42 6.8 40 6.0 3.2 110 300
array-examples/standard_two_index_01_true-unreach-call.i 2 .046 .055 .51 11   0   2.4   4.1  2.2  81   280 960   810   19000 2800
array-examples/standard_two_index_02_true-unreach-call.i 2 .050 .050 .38 8.2 0   0     4.2  2.3  57   280 960   820   15000 2500
array-examples/standard_two_index_03_true-unreach-call.i 2 .052 .052 .28 8.2 0   0     4.5  2.5  56   280 960   830   25000 2800
array-examples/standard_two_index_04_true-unreach-call.i 2 .050 .060 .42 11   0   2.5   4.6  2.6  54   280 960   820   20000 2700
array-examples/standard_two_index_05_true-unreach-call.i 2 .070 .081 .40 11   0   2.5   4.3  2.4  58   270 960   820   29000 2700
array-examples/standard_two_index_06_true-unreach-call.i 2 .070 .070 .27 8.2 0   0     3.9  2.2  62   270 960   820   14000 2700
array-examples/standard_two_index_07_true-unreach-call.i 2 .051 .061 .33 11   0   2.5   4.5  2.5  57   270 960   830   21000 2800
array-examples/standard_two_index_08_true-unreach-call.i 2 .071 .071 .34 8.3 0   0     4.4  2.4  73   280 960   830   27000 2700
array-examples/standard_two_index_09_true-unreach-call.i 2 .057 .067 .36 11   0   2.5   4.2  2.3  65   280 960   830   21000 2900
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 2 .038 .049 .79 11   0   2.5   4.3  2.4  54   270 960   810   28000 2900
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 .065 .075 .30 11   0   2.4   3.5  2.0  43   270 960   790   18000 4000
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 1 .052 .052 .34 8.2 0   0     3.3 1.9 74 270 7.7 4.1 100 320
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 1 .11  .11  .29 8.2 0   0     97   87   2600 1700 97   90   1900 4600
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 1 .051 .061 .53 11   0   2.4   3.1 1.8 53 270 7.4 3.9 110 320
array-industry-pattern/array_range_init_false-unreach-call.i 1 .050 .061 .44 11   0   2.4   3.1 1.8 56 260 97   90   1600 4500
array-industry-pattern/array_single_elem_init_false-unreach-call.i 1 .087 .096 .47 11   0   2.4   3.4 1.9 65 260 6.7 3.6 100 310
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 1 .061 .072 .55 11   0   2.5   97   81   2500 4100 7.6 4.0 160 320
array-industry-pattern/array_monotonic_true-unreach-call.i 2 .052 .055 .41 8.2 0   0     4.3  2.4  57   270 960   830   22000 2800
array-industry-pattern/array_mul_init_true-unreach-call.i 2 .064 .074 .50 11   0   2.6   3.5  2.0  47   270 960   840   22000 3500
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 .046 .046 .42 8.3 0   0     900    890    15000   4800 960   940   15000 4900
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 2 .080 .090 .46 11   0   2.6   900    890    20000   3000 960   940   18000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 2 .062 .074 .43 11   0   2.6   900    890    21000   5800 960   830   13000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 2 .073 .083 .38 11   0   2.6   900    890    19000   3500 960   940   10000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 2 .076 .082 .31 9.9 0   1.5   380    370    7400   7000 960   940   19000 5300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 2 .076 .086 .38 11   0   2.6   910    890    14000   6000 10   5.5 140 310
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 2 .077 .087 .38 11   0   2.5   900    890    18000   4300 960   940   17000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 2 .080 .081 .49 8.4 0   .16  900    890    18000   3600 960   940   14000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i 2 .070 .088 .39 13   0   4.5   910    900    9900   6400 960   810   23000 2700
reducercommutativity/rangesum05_false-unreach-call.i 1 .052 .052 .32 8.3 0   0     5.6 3.4 110 380 7.9 4.2 140 320
reducercommutativity/rangesum10_false-unreach-call.i 1 .049 .059 .50 11   0   2.4   7.0 4.3 140 380 10   5.8 120 310
reducercommutativity/rangesum20_false-unreach-call.i 1 .057 .067 .33 11   0   2.3   9.6 6.2 220 450 9.0 4.8 130 320
reducercommutativity/rangesum40_false-unreach-call.i 1 .059 .077 .37 13   0   4.6   14   8.9 290 630 8.1 4.3 160 330
reducercommutativity/rangesum60_false-unreach-call.i 1 .056 .074 .62 13   0   4.8   19   12   360 720 7.3 3.9 150 310
reducercommutativity/rangesum_false-unreach-call.i 1 .075 .083 .35 10   0   1.6   98   82   2800 3100 9.5 5.0 79 320
reducercommutativity/avg05_true-unreach-call.i 2 .028 .028 .13 7.9 0   .11  900    900    20000   1800 190   160   5400 1100
reducercommutativity/avg10_true-unreach-call.i 2 .029 .030 .11 7.9 0   0     900    890    14000   3400 310   270   8600 1600
reducercommutativity/avg20_true-unreach-call.i 2 .035 .036 .13 8.0 0   .11  910    900    17000   6600 960   860   23000 4100
reducercommutativity/avg40_true-unreach-call.i 2 .032 .033 .12 7.7 0   .045 530    520    9000   7000 220   170   5000 4700
reducercommutativity/avg60_true-unreach-call.i 2 .021 .021 .15 7.7 0   0     400    390    8000   7000 360   280   8200 5000
reducercommutativity/avg_true-unreach-call.i 0 .11  .11  1.3  8.1 0   .23  .69 .44 7.9 44 5.9 3.2 120 290
reducercommutativity/max05_true-unreach-call_true-termination.i 2 .026 .026 .13 7.8 0   0     94    84    1500   820 960   910   26000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i 2 .034 .034 .15 7.7 0   0     900    890    20000   1800 960   880   12000 2400
reducercommutativity/max20_true-unreach-call.i 2 .018 .019 .14 7.9 0   .11  900    890    16000   1800 960   810   23000 5200
reducercommutativity/max40_true-unreach-call.i 2 .027 .028 .11 8.0 0   .22  900    890    20000   2100 960   790   19000 4900
reducercommutativity/max60_true-unreach-call.i 2 .022 .022 .12 7.8 0   0     900    890    25000   3500 960   800   22000 5100
reducercommutativity/max_true-unreach-call.i 0 .11  .11  1.1  7.9 0   .20  .49 .31 6.5 40 6.4 3.4 87 300
reducercommutativity/sep05_true-unreach-call.i 2 .029 .029 .13 7.9 0   .11  170    160    3100   980 240   170   4600 2700
reducercommutativity/sep10_true-unreach-call.i 2 .021 .021 .16 7.8 0   0     900    890    15000   1300 770   650   18000 7000
reducercommutativity/sep20_true-unreach-call.i 2 .026 .027 .13 7.9 0   .11  900    890    17000   1200 320   220   3000 7000
reducercommutativity/sep40_true-unreach-call.i 2 .021 .021 .17 7.8 0   0     900    890    19000   1800 800   640   19000 7000
reducercommutativity/sep60_true-unreach-call.i 2 .032 .033 .12 7.7 0   0     900    890    14000   3600 960   820   15000 5600
reducercommutativity/sep_true-unreach-call.i 0 .14  .14  1.1  8.0 0   .094 .56 .36 9.2 40 6.1 3.2 120 300
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 .020 .020 .14 7.9 0   0     900    900    20000   1100 36   23   850 720
reducercommutativity/sum10_true-unreach-call.i 2 .017 .017 .18 7.9 0   0     900    890    25000   2000 90   58   2200 1300
reducercommutativity/sum20_true-unreach-call.i 2 .026 .027 .15 7.8 0   .098 900    890    18000   6800 960   910   18000 5100
reducercommutativity/sum40_true-unreach-call.i 2 .048 .048 .13 7.8 0   0     380    370    4400   7000 960   800   13000 4800
reducercommutativity/sum60_true-unreach-call.i 2 .023 .024 .14 7.9 0   .11  460    450    8900   7000 960   840   17000 6300
reducercommutativity/sum_true-unreach-call.i 0 .14  .14  1.2  7.9 0   .094 .51 .35 7.0 41 6.1 3.2 110 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 214 86 87 960 1400 0   250 135 450 340 11000 20000   135 500 340 7900 21000   135 23000 23000 460000 140000   135 74000 64000 1600000 340000  
    correct results 127 214 85 86 960 1300 0   250 5 450 340 11000 20000   38 500 340 7900 21000   3 23000 23000 460000 140000   8 73000 64000 1600000 340000  
        correct true 87 174 31 32 330 840 0   130 0 0 0 0 0   38 0 0 0 0   3 23000 23000 460000 140000   8 73000 64000 1600000 340000  
        correct false 40 40 54 54 630 450 0   120 5 450 340 11000 20000   0 500 340 7900 21000   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) 214
Run set sv-comp17.ReachSafety-Arrays