Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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 64    64    860   15000 .84 0      .53 .35 9.4 43 6.0 3.2 130 300
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 150    150    1100   15000 .84 0      .50 .32 9.8 40 5.6 3.0 100 300
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 140    140    1100   15000 .84 0      .65 .42 6.6 40 5.8 3.1 84 290
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 34    34    320   15000 .84 0      .58 .37 10   41 5.1 2.8 70 290
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 34    34    310   15000 .84 0      .51 .32 12   39 6.0 3.2 100 310
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 40    40    440   15000 .84 0      .49 .31 11   40 6.2 3.3 98 310
array-examples/standard_copy1_false-unreach-call_ground.i 1 310    310    4000   670 1.9  0      7.8  4.1  130   460 98   62   1100 7000
array-examples/standard_copy2_false-unreach-call_ground.i 1 490    490    5800   820 2.0  0      9.7  5.1  190   520 96   58   780 6500
array-examples/standard_copy3_false-unreach-call_ground.i 1 660    660    8500   970 2.1  0      13    6.9  130   520 86   52   920 7000
array-examples/standard_copy4_false-unreach-call_ground.i 1 810    810    11000   1100 2.2  .094  12    6.3  140   510 96   57   880 6600
array-examples/standard_copy5_false-unreach-call_ground.i 1 890    890    10000   1200 1.7  0      7.2  3.8  94   320 96   57   920 5600
array-examples/standard_copy6_false-unreach-call_ground.i 1 890    890    12000   1200 1.7  0      5.2  2.8  81   300 97   61   1900 5800
array-examples/standard_copy7_false-unreach-call_ground.i 1 900    900    10000   1300 1.7  0      6.4  3.4  120   310 97   62   1400 5900
array-examples/standard_copy8_false-unreach-call_ground.i 1 890    900    10000   1400 1.7  0      7.2  3.8  120   330 97   60   1300 5600
array-examples/standard_copy9_false-unreach-call_ground.i 1 890    890    9800   1400 1.7  0      5.7  3.1  80   300 96   59   1100 6200
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 1 340    340    4200   680 2.0  0      9.1  4.8  160   500 97   60   1300 6100
array-examples/standard_init1_false-unreach-call_ground.i 1 160    160    1800   530 1.9  0      9.0  4.7  140   470 97   59   770 6700
array-examples/standard_init2_false-unreach-call_ground.i 1 490    490    6000   790 2.0  .094  11    5.8  160   500 97   61   1300 6900
array-examples/standard_init3_false-unreach-call_ground.i 1 790    790    11000   1100 2.1  0      9.3  4.9  160   510 98   61   1100 7000
array-examples/standard_init4_false-unreach-call_ground.i 1 900    900    12000   1200 1.7  0      6.1  3.3  100   310 97   61   1400 5600
array-examples/standard_init5_false-unreach-call_ground.i 1 890    890    12000   1300 1.7  0      5.6  3.0  120   300 97   62   1000 6200
array-examples/standard_init6_false-unreach-call_ground.i 1 900    900    10000   1400 1.7  0      7.0  3.7  65   310 96   62   900 6100
array-examples/standard_init7_false-unreach-call_ground.i 1 890    900    10000   1500 1.7  0      5.6  3.0  100   310 97   61   890 6200
array-examples/standard_init8_false-unreach-call_ground.i 1 890    890    10000   1600 1.7  0      5.7  3.1  94   310 97   62   870 5900
array-examples/standard_init9_false-unreach-call_ground.i 1 890    890    12000   1800 1.7  0      5.7  3.1  110   300 97   59   820 6200
array-examples/standard_minInArray_false-unreach-call_ground.i 1 33    33    380   1300 2.0  0      12    6.3  190   580 98   61   1300 6900
array-examples/standard_partition_false-unreach-call_ground.i 1 890    890    10000   12000 1.7  0      7.7  4.1  63   360 97   73   1800 5000
array-examples/standard_running_false-unreach-call.i 1 900    900    13000   1400 1.7  0      4.2  2.3  71   270 97   59   930 6400
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 61    61    610   15000 1.7  0      12    6.6  170   430 9.1 4.9 150 360
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 63    63    760   15000 .84 .14   .63 .42 8.1 41 7.1 3.8 61 300
array-examples/relax_true-unreach-call.i 2 890    900    10000   3200 1.7  0      900    880    14000   5800 960   900   18000 1500
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 900    900    10000   440 .87 0      .52 .34 4.4 40 6.6 3.5 77 310
array-examples/sanfoundry_10_true-unreach-call_ground.i 2 900    900    13000   2600 1.7  0      710    670    10000   7000 960   780   12000 3200
array-examples/sanfoundry_24_true-unreach-call.i 2 40    40    560   1700 3.5  0      8.0  4.3  94   330 11   6.0 130 360
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 900    900    10000   360 .99 0      .65 .41 7.9 39 5.9 3.1 48 300
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 .80 .80 8.4 65 2.2  0      5.9  3.2  72   290 7.8 4.1 87 330
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 150    150    1000   15000 .84 0      .63 .40 8.5 40 5.6 3.0 90 290
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 34    34    330   15000 .84 0      .62 .40 8.8 41 6.0 3.2 91 310
array-examples/standard_compareModified_true-unreach-call_ground.i 2 29    29    440   2300 3.0  0      43    36    730   940 960   820   17000 4000
array-examples/standard_compare_true-unreach-call_ground.i 2 13    13    160   1200 2.5  0      29    23    450   480 960   800   13000 4200
array-examples/standard_copy1_true-unreach-call_ground.i 2 3.9  3.9  52   420 2.3  0      10    6.0  150   390 960   800   19000 3900
array-examples/standard_copy2_true-unreach-call_ground.i 2 4.1  4.1  46   450 2.5  .0041 20    14    290   530 960   840   17000 4600
array-examples/standard_copy3_true-unreach-call_ground.i 2 4.2  4.2  48   470 2.7  0      29    24    360   470 960   850   13000 4800
array-examples/standard_copy4_true-unreach-call_ground.i 2 4.3  4.3  54   500 2.9  0      40    33    550   880 960   860   12000 4700
array-examples/standard_copy5_true-unreach-call_ground.i 2 4.5  4.5  52   520 3.1  0      47    42    530   1100 960   870   17000 4700
array-examples/standard_copy6_true-unreach-call_ground.i 2 4.7  4.7  55   550 3.3  0      81    76    1400   790 960   860   19000 4700
array-examples/standard_copy7_true-unreach-call_ground.i 2 4.8  4.8  63   570 3.5  0      110    100    2400   970 960   860   15000 4700
array-examples/standard_copy8_true-unreach-call_ground.i 2 5.0  5.0  58   600 3.7  0      150    140    1900   1900 960   870   25000 4700
array-examples/standard_copy9_true-unreach-call_ground.i 2 5.2  5.2  70   620 3.9  0      190    180    2900   2500 960   860   15000 4800
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 4.3  4.3  50   470 2.7  0      25    19    300   620 960   860   15000 4600
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 4.4  4.4  48   490 2.9  0      48    41    510   570 960   860   17000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 4.3  4.3  55   470 2.7  .0082 8.3  4.4  84   310 960   860   17000 4600
array-examples/standard_copyInit_true-unreach-call_ground.i 2 4.1  4.1  56   450 2.5  0      24    17    220   430 960   840   18000 4100
array-examples/standard_find_true-unreach-call_ground.i 2 15    15    220   900 2.8  0      22    16    360   530 960   790   17000 4600
array-examples/standard_init1_true-unreach-call_ground.i 2 3.9  3.9  47   420 2.3  0      12    7.3  140   420 960   790   16000 3900
array-examples/standard_init2_true-unreach-call_ground.i 2 4.1  4.1  51   440 2.5  0      21    15    280   430 960   830   15000 3700
array-examples/standard_init3_true-unreach-call_ground.i 2 4.1  4.1  50   470 2.7  0      24    19    270   590 960   850   15000 4400
array-examples/standard_init4_true-unreach-call_ground.i 2 4.3  4.3  50   490 2.9  0      40    33    620   790 960   850   12000 4600
array-examples/standard_init5_true-unreach-call_ground.i 2 4.4  4.4  51   510 3.1  0      59    52    880   1600 960   860   16000 4800
array-examples/standard_init6_true-unreach-call_ground.i 2 4.5  4.5  52   540 3.3  0      83    76    1200   1500 960   860   15000 4700
array-examples/standard_init7_true-unreach-call_ground.i 2 4.7  4.7  57   560 3.5  0      100    94    1300   1700 960   870   14000 4800
array-examples/standard_init8_true-unreach-call_ground.i 2 4.7  4.7  70   580 3.7  0      150    140    2300   860 960   870   14000 4900
array-examples/standard_init9_true-unreach-call_ground.i 2 4.9  4.9  54   610 3.9  0      180    180    3200   2500 960   870   13000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 900    900    10000   310 .84 0      .49 .32 11   40 6.0 3.2 110 300
array-examples/standard_minInArray_true-unreach-call_ground.i 0 900    900    11000   350 .84 0      .60 .38 8.2 43 7.3 3.8 56 310
array-examples/standard_palindrome_true-unreach-call_ground.i 2 4.0  4.0  49   420 2.3  0      12    7.8  170   390 960   790   14000 3900
array-examples/standard_partial_init_true-unreach-call_ground.i 0 900    900    6600   2300 .84 0      .64 .40 7.4 39 5.9 3.1 100 300
array-examples/standard_partition_original_true-unreach-call_ground.i 0 900    900    9600   2200 .84 0      .63 .41 8.1 41 6.2 3.2 97 300
array-examples/standard_partition_true-unreach-call_ground.i 0 900    900    9200   1700 .84 0      .65 .41 9.2 40 6.9 3.7 56 300
array-examples/standard_password_true-unreach-call_ground.i 2 13    13    160   1200 2.8  0      20    15    360   440 960   800   12000 4600
array-examples/standard_reverse_true-unreach-call_ground.i -16 440    440    5700   680 1.9  0      10    5.5  130   500 100   64   940 7000
array-examples/standard_running_true-unreach-call.i 0 900    900    9700   1200 .84 0      .48 .31 5.8 40 5.2 2.8 64 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 14    14    190   140 2.0  0      7.8  4.2  71   300 14   7.6 130 360
array-examples/standard_seq_init_true-unreach-call_ground.i 2 3.9  3.9  46   420 2.3  0      14    8.8  220   390 960   790   16000 3300
array-examples/standard_strcmp_true-unreach-call_ground.i 2 5.6  5.6  70   550 2.7  0      31    26    560   470 960   810   17000 5000
array-examples/standard_strcpy_original_true-unreach-call.i 2 890    890    12000   1200 1.7  0      9.2  4.9  120   300 960   790   13000 3600
array-examples/standard_strcpy_true-unreach-call_ground.i 0 900    900    13000   1200 .84 0      .58 .37 8.9 40 5.9 3.1 78 290
array-examples/standard_two_index_01_true-unreach-call.i 2 4.4  4.4  51   480 2.5  0      16    11    190   400 960   820   13000 2900
array-examples/standard_two_index_02_true-unreach-call.i 2 4.4  4.4  61   490 2.5  0      11    6.9  110   410 960   820   15000 2700
array-examples/standard_two_index_03_true-unreach-call.i 2 4.4  4.4  58   490 2.5  0      15    9.6  190   420 960   820   14000 2800
array-examples/standard_two_index_04_true-unreach-call.i 2 4.4  4.4  61   490 2.5  0      15    9.5  190   410 960   820   15000 2900
array-examples/standard_two_index_05_true-unreach-call.i 2 4.5  4.5  54   490 2.5  0      14    8.9  200   400 960   820   13000 2800
array-examples/standard_two_index_06_true-unreach-call.i 2 4.4  4.4  53   490 2.5  0      10    6.2  130   400 960   820   14000 3000
array-examples/standard_two_index_07_true-unreach-call.i 2 4.5  4.5  52   490 2.5  0      16    10    170   410 960   830   15000 2900
array-examples/standard_two_index_08_true-unreach-call.i 2 4.5  4.5  58   490 2.5  0      15    9.3  180   400 960   820   12000 2800
array-examples/standard_two_index_09_true-unreach-call.i 2 4.4  4.4  53   490 2.5  0      15    9.6  210   400 960   820   12000 2700
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 2 14    14    180   850 2.6  0      9.2  4.9  87   300 960   820   15000 2800
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 3.9  3.9  46   420 2.3  0      13    8.6  210   400 960   790   11000 3500
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 1 520    520    7200   830 2.0  0      7.3  3.8  150   480 97   67   1400 5000
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 1 61    61    450   4900 2.0  0      96    85    3200   1100 97   89   2100 4600
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i -32 14    14    160   1100 3.3  0      92    87    1600   780 97   62   2200 2100
array-industry-pattern/array_range_init_false-unreach-call.i -32 670    670    7000   790 2.3  0      15    9.6  230   460 96   87   1000 4600
array-industry-pattern/array_single_elem_init_false-unreach-call.i -32 14    14    150   1100 3.3  0      93    87    1900   1700 97   63   910 2300
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900    900    12000   4200 .84 0      .54 .35 11   40 5.7 3.0 99 300
array-industry-pattern/array_monotonic_true-unreach-call.i 0 900    900    9400   730 .84 0      .65 .41 5.9 40 6.5 3.4 68 310
array-industry-pattern/array_mul_init_true-unreach-call.i 0 900    900    10000   1300 .84 0      .58 .36 9.8 40 5.6 2.9 64 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 70    70    580   5200 2.7  0      910    890    18000   5300 960   940   9800 4800
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 320    320    2600   15000 1.7  0      900    890    13000   3300 960   940   9300 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 2 130    130    930   12000 3.0  0      910    890    14000   5100 960   820   19000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 330    330    2900   15000 1.7  .0082 900    890    28000   3600 960   940   11000 5300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 350    350    2300   15000 1.7  0      390    370    6900   7000 960   940   15000 4900
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 2 70    70    480   4700 3.2  0      910    890    17000   6600 15   7.6 130 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 2 170    170    1000   14000 2.6  0      900    890    13000   4000 960   940   14000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 480    480    4300   15000 1.7  0      900    890    17000   3700 960   940   13000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i 2 890    890    12000   1300 1.8  0      910    890    13000   5900 960   810   14000 2700
reducercommutativity/rangesum05_false-unreach-call.i 1 .20 .20 2.4 24 1.7  0      6.9  4.3  100   370 8.7 4.7 99 350
reducercommutativity/rangesum10_false-unreach-call.i 1 .24 .23 3.3 23 1.7  0      7.3  4.6  130   400 11   6.1 180 380
reducercommutativity/rangesum20_false-unreach-call.i 1 .43 .43 4.8 24 1.7  0      11    7.3  190   450 12   6.2 150 410
reducercommutativity/rangesum40_false-unreach-call.i 1 6.1  6.0  78   36 1.7  .094  13    8.8  260   610 13   6.8 170 540
reducercommutativity/rangesum60_false-unreach-call.i 1 .96 .95 13   32 1.7  0      20    13    220   700 14   7.5 200 540
reducercommutativity/rangesum_false-unreach-call.i 1 890    890    9200   2800 1.7  .0041 95    87    2100   2300 23   12   330 930
reducercommutativity/avg05_true-unreach-call.i 2 150    150    1800   90 1.7  0      900    900    12000   1800 170   140   3800 1200
reducercommutativity/avg10_true-unreach-call.i 0 900    900    11000   270 .84 0      .62 .39 8.1 40 5.7 3.0 77 300
reducercommutativity/avg20_true-unreach-call.i 0 900    900    11000   330 .84 0      .52 .33 8.4 42 5.8 3.1 110 300
reducercommutativity/avg40_true-unreach-call.i 0 900    900    12000   390 .84 0      .52 .32 7.8 40 5.3 2.9 76 290
reducercommutativity/avg60_true-unreach-call.i 0 900    900    11000   470 .84 0      .59 .38 9.2 42 6.1 3.2 99 300
reducercommutativity/avg_true-unreach-call.i 0 900    900    11000   410 .84 0      .63 .41 6.3 40 6.1 3.2 76 300
reducercommutativity/max05_true-unreach-call_true-termination.i 2 6.5  6.5  12   26 1.7  0      110    98    1700   830 960   910   22000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i 2 44    44    520   58 1.7  0      900    890    13000   1900 960   880   18000 2500
reducercommutativity/max20_true-unreach-call.i 2 850    850    12000   130 1.7  0      900    890    16000   1800 960   800   17000 5300
reducercommutativity/max40_true-unreach-call.i 0 900    900    11000   220 .84 0      .65 .41 7.7 40 5.7 3.1 95 300
reducercommutativity/max60_true-unreach-call.i 0 900    900    12000   280 .84 .0082 .58 .37 10   43 7.3 3.8 69 300
reducercommutativity/max_true-unreach-call.i 0 900    900    12000   450 .84 0      .54 .34 8.5 39 5.6 3.0 110 290
reducercommutativity/sep05_true-unreach-call.i 2 .61 .61 7.4 23 1.7  0      150    140    2700   1000 200   140   1900 2800
reducercommutativity/sep10_true-unreach-call.i 2 .60 .60 8.1 23 1.7  0      900    890    14000   1300 840   710   16000 7000
reducercommutativity/sep20_true-unreach-call.i 2 .65 .65 7.0 23 1.7  0      900    890    14000   1300 310   210   4900 7000
reducercommutativity/sep40_true-unreach-call.i 2 .69 .69 9.3 29 1.8  0      900    880    14000   2200 730   590   12000 7000
reducercommutativity/sep60_true-unreach-call.i 2 .74 .74 8.8 35 1.8  0      900    880    13000   4100 960   830   17000 5500
reducercommutativity/sep_true-unreach-call.i 0 900    900    10000   450 .84 0      .57 .37 10   40 5.8 3.1 91 300
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 .16 .16 2.0 23 1.7  0      900    890    15000   1000 34   21   770 710
reducercommutativity/sum10_true-unreach-call.i 2 .20 .20 1.9 23 1.7  0      900    890    15000   2100 84   56   1200 1300
reducercommutativity/sum20_true-unreach-call.i 2 .19 .19 2.8 23 1.7  0      900    890    15000   6700 960   910   10000 5200
reducercommutativity/sum40_true-unreach-call.i 2 .23 .23 3.0 23 1.7  0      440    420    7900   7000 960   810   14000 4700
reducercommutativity/sum60_true-unreach-call.i 2 .28 .28 3.1 24 1.8  0      510    490    8400   7000 960   840   15000 6200
reducercommutativity/sum_true-unreach-call.i 0 900    900    12000   530 .84 0      .58 .37 11   41 6.9 3.6 97 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 48 46000 46000 540000 350000 260   .45  135 630 490 13000 18000   135 2700 1800 34000 160000   135 21000 21000   350000 130000   135 58000 51000 910000 280000  
    correct results 95 160 23000 23000 280000 110000 220   .30  5 430 300 9000 15000   6 2400 1500 29000 150000   3 18000 18000   290000 110000   7 54000 47000 860000 250000  
        correct true 65 130 5400 5400 67000 70000 160   .012 0 0 0 0 0   6 0 0 0 0   3 18000 18000   290000 110000   7 54000 47000 860000 250000  
        correct false 30 30 17000 17000 210000 45000 55   .29  5 430 300 9000 15000   0 2400 1500 29000 150000   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 4 -112 1100 1100 13000 3600 11   0     0 200 180 3800 3000   0 290 210 4100 9000   0 10 5.5 130 500   0 100 64 940 7000  
        incorrect true 3 -96 700 700 7300 2900 8.9 0     0 200 180 3800 3000   0 290 210 4100 9000   0 0 0   0 0   0 0 0 0 0  
        incorrect false 1 -16 440 440 5700 680 1.9 0     0 0 0 0 0   0 0 0 0 0   0 10 5.5 130 500   0 100 64 940 7000  
score (135 tasks, max score: 230) 48
Run set sv-comp17.ReachSafety-Arrays