Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 2.5  2.7  28   300   .012 12      13    7.4  260   970 89   60   1500 7000
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 900    900    9700   4200   .012 0      .49 .31 12   39 5.8 3.0 87 300
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 900    900    9300   4200   .012 0      .54 .34 13   40 5.8 3.1 110 300
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 340    340    3500   71   .012 0      .50 .32 13   40 5.7 3.0 70 300
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 340    340    3300   70   .012 0      .62 .40 6.3 40 6.0 3.2 92 290
array-examples/standard_allDiff2_false-unreach-call_ground.i 1 1.0  1.1  13   150   .012 8.1    3.2  1.8  64   260 7.6 4.1 110 330
array-examples/standard_copy1_false-unreach-call_ground.i 1 1.8  1.8  21   230   .012 0      3.3  1.8  49   270 7.9 4.2 100 310
array-examples/standard_copy2_false-unreach-call_ground.i 1 4.6  4.6  50   560   .012 0      23    13    440   1500 97   66   2100 6300
array-examples/standard_copy3_false-unreach-call_ground.i 1 5.9  5.9  64   840   .012 0      32    18    530   3100 97   69   1400 6200
array-examples/standard_copy4_false-unreach-call_ground.i 1 7.4  7.4  84   1100   .012 0      55    31    650   3000 98   65   1600 6600
array-examples/standard_copy5_false-unreach-call_ground.i 1 8.7  8.7  110   1400   .012 0      58    34    960   3600 96   66   1300 6000
array-examples/standard_copy6_false-unreach-call_ground.i 1 10    10    130   1700   .012 0      63    36    1300   4500 98   68   1300 6600
array-examples/standard_copy7_false-unreach-call_ground.i 1 11    11    170   1900   .012 0      90    52    1300   4700 98   66   1700 6700
array-examples/standard_copy8_false-unreach-call_ground.i 1 13    13    160   2200   .012 0      83    49    1500   5300 91   59   1600 7000
array-examples/standard_copy9_false-unreach-call_ground.i 1 14    14    160   2500   .012 0      95    56    1500   5700 97   65   1500 6700
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 1 2.6  2.6  35   560   .012 0      23    13    370   1600 97   69   1700 5900
array-examples/standard_init1_false-unreach-call_ground.i 1 1.4  1.4  18   280   .012 0      13    7.1  310   940 98   68   1300 5900
array-examples/standard_init2_false-unreach-call_ground.i 1 2.7  2.7  33   560   .012 .32   24    13    500   1500 98   70   1300 6100
array-examples/standard_init3_false-unreach-call_ground.i 1 3.9  3.8  49   840   .012 0      33    19    570   3000 96   68   960 5800
array-examples/standard_init4_false-unreach-call_ground.i 1 5.1  5.1  52   1100   .012 0      55    31    760   3100 98   66   1600 6600
array-examples/standard_init5_false-unreach-call_ground.i 1 6.5  6.5  82   1400   .012 0      68    39    900   4000 97   67   1300 6000
array-examples/standard_init6_false-unreach-call_ground.i 1 7.7  7.7  93   1700   .012 0      69    39    1200   4200 97   66   1200 6100
array-examples/standard_init7_false-unreach-call_ground.i 1 8.5  8.5  97   1900   .012 0      84    48    1600   4900 98   68   2000 6900
array-examples/standard_init8_false-unreach-call_ground.i 1 9.9  9.9  120   2200   .012 .32   98    56    880   4900 97   65   1500 6700
array-examples/standard_init9_false-unreach-call_ground.i 1 11    11    130   2500   .012 0      97    56    2100   5600 94   60   1300 7000
array-examples/standard_minInArray_false-unreach-call_ground.i 0 .50 .50 5.8 100   .012 0      .56 .36 8.7 40 5.6 2.9 120 300
array-examples/standard_partition_false-unreach-call_ground.i 0 900    900    8900   12000   .012 0      .58 .38 7.9 41 5.4 2.9 81 300
array-examples/standard_running_false-unreach-call.i 0 1.2  1.2  14   160   .012 0      .54 .35 9.0 40 6.0 3.2 110 300
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 .16 .15 1.7 9.6 .012 0      4.2  2.3  69   280 9.4 5.1 170 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 900    900    10000   1300   .012 0      .55 .35 9.1 41 6.7 3.6 81 300
array-examples/relax_true-unreach-call.i 0 150    150    1600   54   .074 0      .50 .33 12   40 6.4 3.4 120 310
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 320    320    2300   120   .012 0      .52 .33 11   39 6.1 3.3 110 300
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 900    900    10000   940   .012 0      .48 .32 12   41 5.9 3.1 120 290
array-examples/sanfoundry_24_true-unreach-call.i 0 900    900    7900   6400   .012 0      .52 .34 11   42 6.6 3.6 77 290
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 .47 .47 5.8 97   .012 0      .56 .36 7.1 41 7.0 3.7 71 300
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 .16 .16 1.5 9.3 .012 0      3.5  2.0  44   270 9.4 4.9 120 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 900    900    9200   4200   .012 0      .51 .33 11   41 6.1 3.3 74 300
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 330    330    3200   69   .012 0      .59 .39 10   41 7.1 3.7 95 310
array-examples/standard_compareModified_true-unreach-call_ground.i 0 100    100    680   170   .012 0      .50 .33 11   40 7.0 3.7 67 300
array-examples/standard_compare_true-unreach-call_ground.i 0 100    100    780   170   .012 0      .54 .35 11   41 7.4 3.9 100 310
array-examples/standard_copy1_true-unreach-call_ground.i 2 1.1  1.1  16   100   .012 0      4.5  2.5  40   280 960   800   19000 3600
array-examples/standard_copy2_true-unreach-call_ground.i 2 1.5  1.5  22   120   .012 0      3.6  2.0  65   270 960   840   20000 4400
array-examples/standard_copy3_true-unreach-call_ground.i 2 1.8  1.8  21   140   .012 0      3.5  2.0  63   270 960   850   19000 4700
array-examples/standard_copy4_true-unreach-call_ground.i 2 2.2  2.2  29   160   .012 0      3.7  2.1  54   270 960   850   21000 4700
array-examples/standard_copy5_true-unreach-call_ground.i 2 2.5  2.5  34   180   .012 .32   4.5  2.5  50   270 960   870   19000 4700
array-examples/standard_copy6_true-unreach-call_ground.i 2 2.8  2.8  35   200   .012 0      3.9  2.1  67   270 960   860   22000 4700
array-examples/standard_copy7_true-unreach-call_ground.i 2 3.2  3.2  49   230   .012 0      4.0  2.2  90   270 960   870   33000 4700
array-examples/standard_copy8_true-unreach-call_ground.i 2 3.5  3.5  47   250   .012 0      3.8  2.1  53   270 960   870   31000 4800
array-examples/standard_copy9_true-unreach-call_ground.i 2 3.9  3.9  50   270   .012 0      4.0  2.2  67   270 960   870   24000 5100
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 1.4  1.4  17   98   .012 0      4.6  2.5  51   290 960   850   21000 4500
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 1.8  1.8  29   120   .012 0      4.1  2.2  38   270 960   860   20000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 1.5  1.5  19   130   .012 0      3.5  2.0  61   270 960   850   23000 4800
array-examples/standard_copyInit_true-unreach-call_ground.i 2 1.1  1.1  14   79   .012 0      3.6  2.0  83   270 960   830   17000 3200
array-examples/standard_find_true-unreach-call_ground.i 0 900    900    10000   88   .012 0      .50 .31 7.5 42 7.7 4.1 74 290
array-examples/standard_init1_true-unreach-call_ground.i 2 .84 .95 13   67   .012 8.4    3.6  2.0  67   280 960   790   18000 3400
array-examples/standard_init2_true-unreach-call_ground.i 2 1.0  1.0  12   77   .012 0      4.4  2.5  53   270 960   830   18000 3700
array-examples/standard_init3_true-unreach-call_ground.i 2 1.2  1.2  17   93   .012 0      3.5  1.9  46   270 960   850   26000 4000
array-examples/standard_init4_true-unreach-call_ground.i 2 1.4  1.4  17   110   .012 0      3.6  2.0  34   270 960   840   16000 4800
array-examples/standard_init5_true-unreach-call_ground.i 2 1.6  1.6  20   130   .012 0      3.7  2.1  42   290 960   850   18000 4800
array-examples/standard_init6_true-unreach-call_ground.i 2 1.8  1.8  34   140   .012 0      4.1  2.3  53   290 960   860   13000 4700
array-examples/standard_init7_true-unreach-call_ground.i 2 2.1  2.1  28   160   .012 0      4.9  2.7  45   280 960   860   18000 4700
array-examples/standard_init8_true-unreach-call_ground.i 2 2.2  2.2  33   180   .012 0      3.9  2.2  53   280 960   860   19000 4700
array-examples/standard_init9_true-unreach-call_ground.i 2 2.5  2.5  37   200   .012 0      4.7  2.6  66   270 960   860   19000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 .47 .47 5.8 98   .012 0      .53 .33 11   40 6.0 3.2 100 300
array-examples/standard_minInArray_true-unreach-call_ground.i 0 .52 .51 6.9 100   .012 0      .62 .38 8.7 40 5.8 3.1 88 290
array-examples/standard_palindrome_true-unreach-call_ground.i 2 .67 .67 9.9 57   .012 0      3.8  2.1  63   270 960   800   12000 4000
array-examples/standard_partial_init_true-unreach-call_ground.i 0 900    900    8400   3900   .012 0      .53 .33 10   41 6.7 3.5 91 300
array-examples/standard_partition_original_true-unreach-call_ground.i 0 16    16    170   15000   .012 0      .59 .37 12   41 6.2 3.3 98 290
array-examples/standard_partition_true-unreach-call_ground.i 0 900    900    10000   12000   .012 8.8    .51 .33 12   40 5.8 3.1 130 300
array-examples/standard_password_true-unreach-call_ground.i 0 94    94    610   170   .012 0      .49 .31 9.3 41 6.9 3.6 91 300
array-examples/standard_reverse_true-unreach-call_ground.i 2 1.2  1.2  15   100   .012 0      4.6  2.6  53   270 960   790   14000 4100
array-examples/standard_running_true-unreach-call.i 0 1.3  1.3  17   220   .012 0      .50 .33 8.7 40 5.6 3.0 91 290
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 900    900    9200   460   .012 0      .53 .34 11   42 6.1 3.2 100 300
array-examples/standard_seq_init_true-unreach-call_ground.i 2 .93 .93 13   61   .012 0      4.1  2.3  45   270 960   790   12000 3800
array-examples/standard_strcmp_true-unreach-call_ground.i 0 900    900    8700   670   .012 0      .61 .40 9.1 41 6.5 3.5 110 300
array-examples/standard_strcpy_original_true-unreach-call.i 0 900    900    11000   89   .012 0      .62 .38 7.4 41 6.0 3.2 100 310
array-examples/standard_strcpy_true-unreach-call_ground.i 0 900    900    12000   88   .012 0      .59 .37 8.6 39 7.2 3.8 71 290
array-examples/standard_two_index_01_true-unreach-call.i 2 .24 .24 3.2 18   .012 0      4.0  2.2  66   290 960   810   15000 2600
array-examples/standard_two_index_02_true-unreach-call.i 2 .74 .74 8.6 58   .012 0      4.5  2.5  52   290 960   830   13000 3000
array-examples/standard_two_index_03_true-unreach-call.i 2 .20 .20 2.2 12   .012 0      3.9  2.2  58   280 960   810   15000 2500
array-examples/standard_two_index_04_true-unreach-call.i 2 .47 .47 6.4 35   .012 0      3.7  2.0  67   270 960   820   26000 2700
array-examples/standard_two_index_05_true-unreach-call.i 2 .36 .36 4.6 30   .012 0      3.4  1.9  66   270 960   810   22000 2100
array-examples/standard_two_index_06_true-unreach-call.i 2 .18 .18 1.7 11   .012 0      3.8  2.1  61   270 960   820   13000 2900
array-examples/standard_two_index_07_true-unreach-call.i 2 .30 .29 3.6 26   .012 0      4.1  2.3  66   290 960   820   22000 2800
array-examples/standard_two_index_08_true-unreach-call.i 2 .34 .34 3.7 24   .012 .45   4.3  2.4  49   280 960   820   18000 2800
array-examples/standard_two_index_09_true-unreach-call.i 2 .30 .30 4.1 23   .012 0      3.6  2.0  66   270 960   810   21000 2700
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 900    900    12000   560   .012 0      .55 .36 8.4 43 6.9 3.7 69 290
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 1.7  1.8  26   200   .012 7.9    3.9  2.2  75   280 960   780   13000 3600
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 1 1.3  1.3  18   280   .012 0      13    7.3  280   940 96   65   2400 5900
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 1 1.4  1.4  20   280   .012 0      97    83    3100   1700 97   86   1800 4800
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 0 900    900    11000   130   .012 0      .51 .32 11   39 6.1 3.2 82 300
array-industry-pattern/array_range_init_false-unreach-call.i 1 1.6  1.6  20   330   .012 0      18    9.9  320   1200 97   87   1600 4700
array-industry-pattern/array_single_elem_init_false-unreach-call.i 0 900    900    11000   4200   .012 0      .49 .31 9.3 40 7.0 3.7 72 290
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900    900    9000   1300   .012 0      .52 .33 11   42 6.7 3.5 92 300
array-industry-pattern/array_monotonic_true-unreach-call.i 0 9.6  9.4  120   15000   .012 0      .51 .34 5.1 40 6.2 3.3 95 290
array-industry-pattern/array_mul_init_true-unreach-call.i 0 15    15    190   15000   .012 0      .53 .33 13   40 5.6 3.0 87 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 .81 .81 10   60   .012 0      900    890    15000   5300 960   940   22000 4800
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 900    900    9300   210   .016 0      .51 .32 8.6 41 7.3 3.9 66 290
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 2 1.0  1.0  14   74   .012 0      900    890    12000   5800 960   830   26000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 900    900    9600   4100   .012 0      .60 .38 9.6 40 7.2 3.8 86 290
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 900    900    12000   7200   .012 .0082 .60 .39 9.7 41 7.3 3.8 110 310
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 2 3.0  3.0  41   180   .012 0      910    900    21000   6900 12   6.6 160 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 2 .97 .96 12   67   .012 0      900    890    8900   4300 960   940   18000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 900    900    8500   4300   .012 0      .55 .36 11   41 6.3 3.3 110 300
array-industry-pattern/array_shadowinit_true-unreach-call.i 0 .17 .17 1.8 10   .012 0      .51 .32 13   40 7.6 4.0 82 300
reducercommutativity/rangesum05_false-unreach-call.i 1 .15 .15 1.8 11   .012 0      3.8  2.1  63   270 9.2 4.9 85 310
reducercommutativity/rangesum10_false-unreach-call.i 1 .18 .18 1.6 11   .012 0      4.3  2.4  88   270 9.5 5.5 140 310
reducercommutativity/rangesum20_false-unreach-call.i 1 .23 .23 3.1 22   .012 0      5.1  2.8  93   280 8.3 4.4 160 330
reducercommutativity/rangesum40_false-unreach-call.i 1 .27 .27 2.7 25   .012 0      7.8  4.2  76   290 8.8 4.7 130 340
reducercommutativity/rangesum60_false-unreach-call.i 1 .30 .30 3.1 29   .012 0      7.3  3.9  150   310 9.4 5.0 140 320
reducercommutativity/rangesum_false-unreach-call.i 0 900    900    7300   210   .012 0      .62 .40 9.3 40 6.3 3.4 120 310
reducercommutativity/avg05_true-unreach-call.i 2 .15 .15 1.8 9.3 .012 0      900    900    16000   1700 180   160   4200 1100
reducercommutativity/avg10_true-unreach-call.i 2 .17 .17 1.8 9.5 .012 0      900    890    11000   3400 320   270   7000 1500
reducercommutativity/avg20_true-unreach-call.i 2 .17 .17 1.6 9.5 .012 0      900    900    6800   6600 960   850   17000 3700
reducercommutativity/avg40_true-unreach-call.i 2 .17 .17 1.7 9.3 .012 0      500    490    8200   7000 220   160   3900 4800
reducercommutativity/avg60_true-unreach-call.i 2 .19 .18 1.7 9.5 .012 0      380    370    8200   7000 360   270   7600 5100
reducercommutativity/avg_true-unreach-call.i 0 .16 .16 1.7 9.9 .012 0      .52 .32 12   41 5.9 3.1 120 300
reducercommutativity/max05_true-unreach-call_true-termination.i 2 1.6  1.6  18   12   .012 0      110    99    2100   830 960   910   16000 1200
reducercommutativity/max10_true-unreach-call_true-termination.i 2 52    52    530   34   .012 0      900    890    17000   1800 960   860   15000 2500
reducercommutativity/max20_true-unreach-call.i 0 900    900    10000   140   .012 0      .61 .39 8.8 40 5.7 3.0 120 290
reducercommutativity/max40_true-unreach-call.i 0 900    900    11000   260   .012 0      .56 .37 9.5 40 5.3 2.9 89 290
reducercommutativity/max60_true-unreach-call.i 0 900    900    11000   300   .012 0      .62 .40 9.8 43 7.1 3.7 72 300
reducercommutativity/max_true-unreach-call.i 0 .18 .17 1.8 10   .012 0      .67 .43 8.2 40 7.9 4.2 77 300
reducercommutativity/sep05_true-unreach-call.i 2 .18 .18 1.6 9.4 .012 0      130    120    3900   970 210   150   1900 3200
reducercommutativity/sep10_true-unreach-call.i 2 .16 .15 1.8 9.4 .012 0      900    890    12000   1300 740   630   10000 7000
reducercommutativity/sep20_true-unreach-call.i 2 .16 .16 1.7 9.4 .012 0      900    890    12000   1300 400   270   5800 7000
reducercommutativity/sep40_true-unreach-call.i 2 .18 .17 2.2 9.2 .012 0      900    890    17000   1800 910   740   19000 7000
reducercommutativity/sep60_true-unreach-call.i 2 .19 .18 1.9 9.4 .012 0      900    890    12000   3300 960   820   29000 5500
reducercommutativity/sep_true-unreach-call.i 0 .16 .16 2.0 10   .012 0      .50 .33 9.7 41 5.7 3.0 110 290
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 .17 .17 1.6 9.3 .012 0      900    900    16000   1100 38   23   380 730
reducercommutativity/sum10_true-unreach-call.i 2 .28 .40 2.3 19   .012 8.8    900    890    17000   2000 92   60   1600 1300
reducercommutativity/sum20_true-unreach-call.i 2 .18 .18 1.9 9.4 .012 0      900    890    10000   6700 960   900   15000 5000
reducercommutativity/sum40_true-unreach-call.i 2 .17 .17 2.0 9.3 .012 0      390    380    4500   7000 350   280   9300 4700
reducercommutativity/sum60_true-unreach-call.i 2 .27 .38 1.7 17   .012 7.6    420    410    6800   7000 960   850   19000 6300
reducercommutativity/sum_true-unreach-call.i 0 .17 .16 2.1 10   .012 0      .51 .33 11   39 7.5 4.0 74 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 145 25000 25000 280000 150000 1.7  63 135 1200 740 22000 72000   135 2200 1600 36000 140000   135 16000 15000 240000 95000   135 46000 40000 920000 230000  
    correct results 87 145 260 260 3100 31000 1.1  54 5 1200 740 22000 72000   7 2200 1500 35000 140000   3 16000 15000 240000 93000   7 46000 40000 920000 220000  
        correct true 58 116 110 110 1400 4500 .71 33 5 0 0 0 0   7 0 0 0 0   3 16000 15000 240000 93000   7 46000 40000 920000 220000  
        correct false 29 29 150 150 1800 27000 .36 20 0 1200 740 22000 72000   0 2200 1500 35000 140000   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) 145
Run set sv-comp17.ReachSafety-Arrays