Tool CBMC 5.6
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:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.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/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.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 error (1) 0 wit inspect 130    130    1700   14000 3.2   0      error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.9 3.1 110 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 0 wit inspect 22    22    250   15000 .15  0      error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.3 3.3 120 310 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 0 wit inspect 22    22    290   15000 .15  0      error (invalid witness file) .50 .32 11   39 error (invalid witness file) 7.0 3.7 98 310 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error (134) 0 wit inspect 58    58    760   13000 .029 0      error (invalid witness file) .49 .32 9.5 41 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i error (134) 0 wit inspect 70    70    910   13000 .029 0      error (invalid witness file) .53 .35 12   44 error (invalid witness file) 6.6 3.5 94 300 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i error (1) 0 wit inspect 410    410    2400   10000 5.3   0      error (invalid witness file) .53 .34 12   40 error (invalid witness file) 5.5 2.9 99 290 - -
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 0 wit inspect 130    130    1700   15000 .65  0      error (invalid witness file) .51 .34 10   39 error (invalid witness file) 5.7 3.0 130 300 - -
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 0 wit inspect 83    83    1000   15000 .34  0      error (invalid witness file) .52 .34 12   42 error (invalid witness file) 6.4 3.4 110 300 - -
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 0 wit inspect 94    94    1500   15000 .43  0      error (invalid witness file) .53 .35 12   40 error (invalid witness file) 7.4 3.9 91 300 - -
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 0 wit inspect 100    100    1400   15000 .50  0      error (invalid witness file) .56 .36 15   41 error (invalid witness file) 5.9 3.1 120 290 - -
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 0 wit inspect 120    120    1500   15000 .60  .0041 error (invalid witness file) .48 .32 7.9 41 error (invalid witness file) 7.0 3.7 65 310 - -
array-examples/standard_copy6_false-unreach-call_ground.i error (134) 0 wit inspect 93    93    1200   15000 .45  0      error (invalid witness file) .56 .35 10   40 error (invalid witness file) 5.8 3.1 110 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 0 wit inspect 100    100    1600   15000 .45  0      error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_copy8_false-unreach-call_ground.i error (134) 0 wit inspect 82    82    1200   14000 .36  .074  error (invalid witness file) .51 .32 13   39 error (invalid witness file) 5.3 2.8 59 290 - -
array-examples/standard_copy9_false-unreach-call_ground.i error (134) 0 wit inspect 89    89    1400   14000 .39  0      error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 0 wit inspect 78    78    1200   15000 .43  0      error (invalid witness file) .49 .32 6.4 39 error (invalid witness file) 5.5 2.9 85 300 - -
array-examples/standard_init1_false-unreach-call_ground.i out of memory 0 wit inspect 130    130    1800   15000 .65  .0041 error (invalid witness file) .53 .34 9.7 40 error (invalid witness file) 6.3 3.3 84 300 - -
array-examples/standard_init2_false-unreach-call_ground.i out of memory 0 wit inspect 67    67    880   15000 .34  0      error (invalid witness file) .57 .37 4.0 44 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/standard_init3_false-unreach-call_ground.i out of memory 0 wit inspect 70    70    910   15000 .42  0      error (invalid witness file) .49 .33 10   40 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/standard_init4_false-unreach-call_ground.i out of memory 0 wit inspect 73    73    890   15000 .50  0      error (invalid witness file) .61 .40 8.3 39 error (invalid witness file) 6.9 3.7 74 300 - -
array-examples/standard_init5_false-unreach-call_ground.i out of memory 0 wit inspect 76    76    990   15000 .59  0      error (invalid witness file) .50 .32 8.0 41 error (invalid witness file) 6.2 3.3 81 290 - -
array-examples/standard_init6_false-unreach-call_ground.i out of memory 0 wit inspect 79    79    1000   15000 .67  0      error (invalid witness file) .48 .31 8.4 39 error (invalid witness file) 5.9 3.1 120 300 - -
array-examples/standard_init7_false-unreach-call_ground.i out of memory 0 wit inspect 55    55    720   15000 .45  0      error (invalid witness file) .53 .34 14   40 error (invalid witness file) 6.5 3.4 87 290 - -
array-examples/standard_init8_false-unreach-call_ground.i out of memory 0 wit inspect 57    57    800   15000 .51  0      error (invalid witness file) .52 .35 5.4 40 error (invalid witness file) 6.5 3.4 120 310 - -
array-examples/standard_init9_false-unreach-call_ground.i out of memory 0 wit inspect 59    59    920   15000 .55  0      error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.7 3.6 96 300 - -
array-examples/standard_minInArray_false-unreach-call_ground.i error (42) 0 wit inspect 850    850    3500   1300 10     0      error (invalid witness file) .54 .34 10   39 error (invalid witness file) 7.0 3.7 83 300 - -
array-examples/standard_partition_false-unreach-call_ground.i error (134) 0 wit inspect 68    68    810   14000 .15  0      error (invalid witness file) .52 .32 14   40 error (invalid witness file) 6.8 3.6 77 300 - -
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 94    94    1300   15000 .41  0      error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.8 3.6 64 290 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (42) 0 wit inspect 850    850    4300   1500 10     0      - - error (invalid witness file) .58 .37 11   42 error (invalid witness file) 6.6 3.5 110 300
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) 0 wit inspect 26    26    340   13000 .016 0      - - error (invalid witness file) .50 .33 14   40 error (invalid witness file) 6.0 3.2 130 300
array-examples/relax_true-unreach-call.i error (42) 0 wit inspect 850    850    3300   4800 .38  0      - - error (invalid witness file) .51 .32 14   39 error (invalid witness file) 6.4 3.5 100 290
array-examples/sanfoundry_02_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    3500   2300 21     0      - - error (invalid witness file) .57 .36 9.6 40 error (invalid witness file) 6.2 3.3 120 310
array-examples/sanfoundry_10_true-unreach-call_ground.i error (134) 0 wit inspect 28    28    370   13000 0     0      - - error (invalid witness file) .54 .34 11   40 error (invalid witness file) 6.0 3.2 120 300
array-examples/sanfoundry_24_true-unreach-call.i error (42) 0 wit inspect 850    850    9300   4200 7.5   0      - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 7.2 3.8 92 300
array-examples/sanfoundry_27_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    3500   1200 11     0      - - error (invalid witness file) .61 .39 9.6 39 error (invalid witness file) 5.8 3.1 130 300
array-examples/sanfoundry_43_true-unreach-call_ground.i out of memory 0 wit inspect 110    110    1600   15000 .51  0      - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.2 3.3 110 290
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 0 wit inspect 19    19    240   15000 .15  0      - - error (invalid witness file) .67 .44 9.2 44 error (invalid witness file) 5.5 2.9 110 290
array-examples/sorting_selectionsort_true-unreach-call_ground.i error (134) 0 wit inspect 70    70    890   13000 .029 0      - - error (invalid witness file) .71 .44 9.0 43 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_compareModified_true-unreach-call_ground.i error (1) 0 wit inspect 140    140    2100   15000 1.5   0      - - error (invalid witness file) .48 .31 9.7 40 error (invalid witness file) 6.1 3.2 130 300
array-examples/standard_compare_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    3700   1400 9.8   0      - - error (invalid witness file) .73 .46 7.0 43 error (invalid witness file) 6.6 3.4 120 310
array-examples/standard_copy1_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1500   15000 .65  0      - - error (invalid witness file) .62 .40 9.3 40 error (invalid witness file) 6.0 3.1 140 300
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 0 wit inspect 83    83    1100   15000 .34  0      - - error (invalid witness file) .64 .41 8.6 40 error (invalid witness file) 6.3 3.3 140 300
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 0 wit inspect 94    94    1400   15000 .42  0      - - error (invalid witness file) .50 .32 10   41 error (invalid witness file) 5.7 3.0 110 310
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 0 wit inspect 110    110    1500   15000 .50  0      - - error (invalid witness file) .63 .39 8.1 39 error (invalid witness file) 6.5 3.4 140 300
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 0 wit inspect 120    120    1800   15000 .55  .35   - - error (invalid witness file) .52 .35 13   40 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_copy6_true-unreach-call_ground.i error (134) 0 wit inspect 92    92    1300   15000 .45  0      - - error (invalid witness file) .67 .43 7.8 42 error (invalid witness file) 6.2 3.3 120 300
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 0 wit inspect 100    100    1400   15000 .45  0      - - error (invalid witness file) .50 .32 9.9 41 error (invalid witness file) 6.0 3.2 130 300
array-examples/standard_copy8_true-unreach-call_ground.i error (134) 0 wit inspect 82    82    1100   14000 .36  0      - - error (invalid witness file) .64 .40 8.5 40 error (invalid witness file) 6.3 3.3 130 300
array-examples/standard_copy9_true-unreach-call_ground.i error (134) 0 wit inspect 89    89    1200   14000 .39  0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.3 3.4 100 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 0 wit inspect 78    78    1000   15000 .40  0      - - error (invalid witness file) .66 .42 8.2 43 error (invalid witness file) 5.6 2.9 110 300
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 0 wit inspect 81    81    1000   15000 .53  0      - - error (invalid witness file) .56 .36 9.4 39 error (invalid witness file) 5.8 3.1 120 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 0 wit inspect 78    78    1000   15000 .43  0      - - error (invalid witness file) .69 .44 7.2 42 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 0 wit inspect 74    74    970   15000 .34  0      - - error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_find_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1600   15000 .94  0      - - error (invalid witness file) .66 .42 7.1 40 error (invalid witness file) 6.4 3.4 68 300
array-examples/standard_init1_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1600   15000 .64  0      - - error (invalid witness file) .58 .38 8.1 39 error (invalid witness file) 6.5 3.5 120 310
array-examples/standard_init2_true-unreach-call_ground.i out of memory 0 wit inspect 67    67    760   15000 .34  0      - - error (invalid witness file) .56 .37 6.6 40 error (invalid witness file) 6.2 3.3 140 300
array-examples/standard_init3_true-unreach-call_ground.i out of memory 0 wit inspect 70    70    970   15000 .42  0      - - error (invalid witness file) .48 .31 10   39 error (invalid witness file) 5.7 3.0 120 300
array-examples/standard_init4_true-unreach-call_ground.i out of memory 0 wit inspect 73    73    950   15000 .50  0      - - error (invalid witness file) .65 .42 8.2 40 error (invalid witness file) 5.4 2.9 100 300
array-examples/standard_init5_true-unreach-call_ground.i out of memory 0 wit inspect 76    76    1100   15000 .57  0      - - error (invalid witness file) .65 .41 8.5 41 error (invalid witness file) 7.7 4.0 80 300
array-examples/standard_init6_true-unreach-call_ground.i out of memory 0 wit inspect 79    79    990   15000 .67  0      - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 5.7 3.0 97 290
array-examples/standard_init7_true-unreach-call_ground.i out of memory 0 wit inspect 55    55    720   15000 .45  0      - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.9 3.1 84 300
array-examples/standard_init8_true-unreach-call_ground.i out of memory 0 wit inspect 57    57    710   15000 .51  0      - - error (invalid witness file) .67 .42 9.4 40 error (invalid witness file) 5.4 2.9 120 280
array-examples/standard_init9_true-unreach-call_ground.i out of memory 0 wit inspect 59    59    750   15000 .55  0      - - error (invalid witness file) .68 .43 7.8 40 error (invalid witness file) 5.6 3.0 100 290
array-examples/standard_maxInArray_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    4500   1300 9.9   0      - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.7 3.5 120 300
array-examples/standard_minInArray_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    3900   1200 9.9   0      - - error (invalid witness file) .68 .44 7.8 39 error (invalid witness file) 6.4 3.4 120 310
array-examples/standard_palindrome_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1800   15000 .65  0      - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 6.1 3.3 120 300
array-examples/standard_partial_init_true-unreach-call_ground.i error (134) 0 wit inspect 91    91    1100   13000 .21  .074  - - error (invalid witness file) .55 .36 12   41 error (invalid witness file) 5.7 3.1 110 300
array-examples/standard_partition_original_true-unreach-call_ground.i error (134) 0 wit inspect 77    77    940   14000 .13  0      - - error (invalid witness file) .52 .32 9.3 42 error (invalid witness file) 6.8 3.6 130 310
array-examples/standard_partition_true-unreach-call_ground.i error (134) 0 wit inspect 68    68    860   14000 .11  .074  - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.5 3.4 120 320
array-examples/standard_password_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    4100   1400 9.9   0      - - error (invalid witness file) .62 .40 9.1 43 error (invalid witness file) 5.7 3.0 110 300
array-examples/standard_reverse_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1800   15000 .65  0      - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 5.4 2.9 110 290
array-examples/standard_running_true-unreach-call.i out of memory 0 wit inspect 94    94    1300   15000 .41  0      - - error (invalid witness file) .66 .42 7.3 39 error (invalid witness file) 5.9 3.1 100 290
array-examples/standard_sentinel_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850    11000   3900 1.2   0      - - error (invalid witness file) .62 .40 8.0 39 error (invalid witness file) 6.0 3.1 110 290
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 0 wit inspect 130    130    1700   15000 .65  0      - - error (invalid witness file) .62 .40 8.6 42 error (invalid witness file) 6.2 3.3 110 300
array-examples/standard_strcmp_true-unreach-call_ground.i error (42) 0 wit inspect 850    850    4200   3300 7.6   0      - - error (invalid witness file) .64 .41 7.6 40 error (invalid witness file) 6.2 3.2 120 300
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 0 wit inspect 79    79    1200   15000 .40  0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.0 3.2 120 290
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 0 wit inspect 79    79    960   15000 .39  .0041 - - error (invalid witness file) .63 .40 7.7 40 error (invalid witness file) 6.1 3.2 100 290
array-examples/standard_two_index_01_true-unreach-call.i out of memory 0 wit inspect 160    160    2100   15000 10     0      - - error (invalid witness file) .54 .36 9.7 39 error (invalid witness file) 7.2 3.8 86 300
array-examples/standard_two_index_02_true-unreach-call.i out of memory 0 wit inspect 130    130    1600   15000 .85  0      - - error (invalid witness file) .65 .40 7.6 40 error (invalid witness file) 6.1 3.2 96 300
array-examples/standard_two_index_03_true-unreach-call.i out of memory 0 wit inspect 160    160    2000   15000 10     0      - - error (invalid witness file) .63 .40 7.6 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_two_index_04_true-unreach-call.i out of memory 0 wit inspect 130    130    1700   15000 .85  0      - - error (invalid witness file) .63 .40 11   42 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_two_index_05_true-unreach-call.i out of memory 0 wit inspect 130    130    1800   15000 .85  0      - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect 100    100    1500   8800 9.8   0      - - error 37    25    710   700 timeout 960   820   15000 4700
array-examples/standard_two_index_07_true-unreach-call.i out of memory 0 wit inspect 130    130    1600   15000 .85  0      - - error (invalid witness file) .51 .33 9.4 40 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_two_index_08_true-unreach-call.i out of memory 0 wit inspect 130    130    1600   15000 .85  0      - - error (invalid witness file) .69 .43 8.7 39 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_two_index_09_true-unreach-call.i out of memory 0 wit inspect 130    130    1600   15000 .85  0      - - error (invalid witness file) .50 .32 9.4 39 error (invalid witness file) 7.2 3.8 160 310
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (42) 0 wit inspect 850    850    5000   7700 9.4   0      - - error (invalid witness file) .69 .43 7.3 41 error (invalid witness file) 6.0 3.2 140 300
array-examples/standard_vector_difference_true-unreach-call_ground.i error (1) 0 wit inspect 140    140    2100   15000 .82  0      - - error (invalid witness file) .55 .36 9.0 43 error (invalid witness file) 6.0 3.2 130 290
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i out of memory 0 wit inspect 66    66    970   15000 .29  0      error (invalid witness file) .51 .33 14   40 error (invalid witness file) 6.0 3.3 96 290 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 0 wit inspect 550    550    8000   15000 500     .012  error (invalid witness file) .50 .32 9.3 41 error (invalid witness file) 6.8 3.6 110 300 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 75    75    1200   15000 .45  0      error (invalid witness file) .56 .36 10   41 error (invalid witness file) 6.5 3.4 110 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i error (42) 0 wit inspect 850    850    11000   14000 1500     .0041 error (invalid witness file) .47 .31 13   39 error (invalid witness file) 7.0 3.7 69 300 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 75    75    1000   15000 .44  0      error (invalid witness file) .56 .36 9.6 42 error (invalid witness file) 5.8 3.0 100 300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) 0 wit inspect 23    23    290   12000 0     0      error (invalid witness file) .51 .33 6.6 41 error (invalid witness file) 6.3 3.3 96 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i out of memory 0 wit inspect 110    110    1700   15000 .34  0      - - error (invalid witness file) .63 .40 7.7 40 error (invalid witness file) 7.0 3.7 85 300
array-industry-pattern/array_mul_init_true-unreach-call.i out of memory 0 wit inspect 130    130    1600   15000 .48  .0041 - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.2 2.8 100 290
array-industry-pattern/array_of_struct_break_true-unreach-call.i out of memory 0 wit inspect 290    290    3400   15000 190     0      - - error (invalid witness file) .62 .38 7.8 40 error (invalid witness file) 6.0 3.2 120 290
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (1) 0 wit inspect 230    230    3000   4200 370     .0082 - - error (invalid witness file) .61 .39 11   44 error (invalid witness file) 6.9 3.7 91 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i out of memory 0 wit inspect 180    180    2700   15000 1.2   0      - - error (invalid witness file) .65 .42 7.7 40 error (invalid witness file) 5.9 3.1 110 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (1) 0 wit inspect 230    230    2900   4200 360     .0041 - - error (invalid witness file) .51 .32 12   42 error (invalid witness file) 6.0 3.2 120 310
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i error (42) 0 wit inspect 850    850    12000   10000 950     .020  - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.8 3.1 110 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 0 wit inspect 150    150    1800   15000 21     0      - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 6.2 3.2 120 310
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i out of memory 0 wit inspect 830    830    12000   15000 760     .020  - - error (invalid witness file) .53 .34 12   43 error (invalid witness file) 5.8 3.1 97 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i error (1) 0 wit inspect 120    120    1400   4600 19     0      - - error (invalid witness file) .64 .41 8.4 43 error (invalid witness file) 6.3 3.3 130 310
array-industry-pattern/array_shadowinit_true-unreach-call.i error (42) 0 wit inspect 850    850    6200   5500 .35  0      - - error (invalid witness file) .56 .35 9.5 42 error (invalid witness file) 5.9 3.1 120 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect .25 .25 3.4 21 .045 0      false(unreach-call) 6.2  3.8  150   380 false(unreach-call) 18   11   350 410 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect .39 .38 4.2 20 .11  0      false(unreach-call) 8.4  5.4  130   400 false(unreach-call) 16   8.7 310 510 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 1.1  1.1  13   24 .30  0      false(unreach-call) 12    7.9  270   460 timeout 97   61   980 6800 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 1.1  1.1  14   27 .67  .13   false(unreach-call) 18    12    440   720 timeout 96   58   930 6700 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 7.4  7.4  84   50 .79  0      false(unreach-call) 21    13    160   820 out of memory 78   49   960 7000 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect .52 .51 6.5 40 .053 0      false(unreach-call) 6.6  4.0  150   390 false(unreach-call) 14   7.7 250 410 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect 36    36    430   40 .029 0      - - timeout 900    900    18000   1800 true 180   160   4000 1200
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect 540    540    7800   170 .086 0      - - timeout 900    890    17000   3500 true 290   250   4300 1600
reducercommutativity/avg20_true-unreach-call.i error (42) 0 wit inspect 850    850    10000   280 .19  0      - - error (invalid witness file) .59 .38 9.8 41 error (invalid witness file) 7.1 3.7 47 300
reducercommutativity/avg40_true-unreach-call.i error (42) 0 wit inspect 850    850    9600   290 .47  0      - - error (invalid witness file) .51 .32 9.1 39 error (invalid witness file) 6.0 3.2 110 290
reducercommutativity/avg60_true-unreach-call.i error (42) 0 wit inspect 850    850    11000   340 .47  0      - - error (invalid witness file) .68 .43 10   42 error (invalid witness file) 6.0 3.2 130 310
reducercommutativity/avg_true-unreach-call.i error (42) 0 wit inspect 850    850    11000   220 .033 0      - - error (invalid witness file) .52 .32 10   40 error (invalid witness file) 5.9 3.1 120 300
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 1.9  1.9  20   23 .045 0      - - true 120    100    2200   830 timeout 960   900   29000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 89    89    1100   56 .11  0      - - timeout 900    890    14000   1900 timeout 960   880   14000 2300
reducercommutativity/max20_true-unreach-call.i error (42) 0 wit inspect 850    850    13000   180 .22  0      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.8 3.0 130 290
reducercommutativity/max40_true-unreach-call.i error (42) 0 wit inspect 850    850    8700   220 .56  0      - - error (invalid witness file) .55 .36 12   42 error (invalid witness file) 5.8 3.1 120 300
reducercommutativity/max60_true-unreach-call.i error (42) 0 wit inspect 850    850    8500   260 .56  .0041 - - error (invalid witness file) .51 .33 14   40 error (invalid witness file) 6.9 3.6 130 310
reducercommutativity/max_true-unreach-call.i error (42) 0 wit inspect 850    850    10000   230 .12  0      - - error (invalid witness file) .60 .39 8.2 40 error (invalid witness file) 5.9 3.2 110 290
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect .40 .40 4.7 23 .045 0      - - true 170    150    3300   1100 true 210   150   3400 2800
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect .77 .77 8.1 27 .12  0      - - timeout 900    890    19000   1300 out of memory 760   640   13000 7000
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 3.5  3.5  40   36 .38  0      - - timeout 900    890    15000   1400 out of memory 310   210   4100 7000
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect 34    34    430   93 .86  0      - - timeout 900    890    25000   2700 out of memory 830   660   15000 7000
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect 160    160    1900   160 .97  0      - - timeout 900    880    16000   4500 timeout 960   820   16000 5400
reducercommutativity/sep_true-unreach-call.i error (134) 0 wit inspect 640    640    4600   13000 .64  0      - - error (invalid witness file) .62 .41 8.4 39 error (invalid witness file) 6.6 3.5 78 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 4.2  4.2  51   25 .037 .10   - - timeout 900    900    22000   1000 true 36   22   670 730
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect 180    180    2300   110 .086 0      - - timeout 900    890    24000   2200 true 110   70   1300 1300
reducercommutativity/sum20_true-unreach-call.i error (42) 0 wit inspect 850    850    11000   260 .19  0      - - error (invalid witness file) .51 .32 9.2 39 error (invalid witness file) 5.5 3.0 100 290
reducercommutativity/sum40_true-unreach-call.i error (42) 0 wit inspect 850    850    10000   280 .47  0      - - error (invalid witness file) .60 .40 7.9 40 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sum60_true-unreach-call.i error (42) 0 wit inspect 850    850    11000   260 .47  0      - - error (invalid witness file) .54 .35 10   39 error (invalid witness file) 6.1 3.2 110 300
reducercommutativity/sum_true-unreach-call.i error (42) 0 wit inspect 850    850    11000   250 .041 0      - - error (invalid witness file) .48 .32 7.6 40 error (invalid witness file) 5.6 3.0 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 30 36000 36000 370000 1400000 4900   .90 135 90 57 1600 4500   135 530 310 7100 32000   135 8500 8300 180000 26000   135 7100 5900 130000 67000  
    correct results 18 30 1200 1200 16000 9700 15   .23 6 72 46 1300 3200   3 320 200 3800 22000   2 8400 8300 180000 23000   5 6600 5600 120000 42000  
        correct true 12 24 1100 1100 16000 9500 13   .10 0 0 0 0 0   0 0 0 0 0   2 8400 8300 180000 23000   5 6600 5600 120000 42000  
        correct false 6 6 11 11 130 180 2.0 .13 6 72 46 1300 3200   3 320 200 3800 22000   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) 30
Run set sv-comp17.ReachSafety-Arrays