Tool 2LS 0.5.0
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 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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 out of memory 0 wit inspect 41   41   470 15000 0      0    error (invalid witness file) .55 .35 13   42 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 0 wit inspect 38   38   530 15000 0      0    error (invalid witness file) .54 .35 13   44 error (invalid witness file) 6.5 3.4 85 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 0 wit inspect 38   38   540 15000 0      0    error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.2 3.2 110 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 0 wit inspect 39   39   540 15000 0      0    error (invalid witness file) .51 .34 13   39 error (invalid witness file) 5.8 3.1 100 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 0 wit inspect 40   39   520 15000 0      0    error (invalid witness file) .67 .43 9.2 42 error (invalid witness file) 6.9 3.6 92 320 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 0 wit inspect 220   220   1900 15000 0      0    error (invalid witness file) .49 .31 5.0 40 error (invalid witness file) 6.3 3.3 120 300 - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   900   12000 13000 0      0    error (invalid witness file) .50 .32 10   39 error (invalid witness file) 7.3 3.8 89 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 0 wit inspect 38   38   510 15000 0      0    error (invalid witness file) .46 .32 7.1 39 error (invalid witness file) 5.5 2.9 100 290 - -
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 0 wit inspect 39   38   560 15000 0      0    error (invalid witness file) .58 .37 9.9 40 error (invalid witness file) 5.8 3.1 110 300 - -
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 0 wit inspect 38   38   610 15000 0      0    error (invalid witness file) .55 .36 10   44 error (invalid witness file) 6.0 3.2 99 300 - -
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 0 wit inspect 39   38   550 15000 0      0    error (invalid witness file) .52 .34 12   42 error (invalid witness file) 5.9 3.1 97 300 - -
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 0 wit inspect 39   38   570 15000 0      0    error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 0 wit inspect 39   38   470 15000 0      0    error (invalid witness file) .52 .33 8.6 41 error (invalid witness file) 6.1 3.2 120 300 - -
array-examples/standard_copy8_false-unreach-call_ground.i out of memory 0 wit inspect 39   38   460 15000 0      0    error (invalid witness file) .47 .30 6.8 39 error (invalid witness file) 6.6 3.5 87 300 - -
array-examples/standard_copy9_false-unreach-call_ground.i out of memory 0 wit inspect 38   38   530 15000 0      0    error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.0 3.2 99 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 0 wit inspect 41   41   520 15000 0      0    error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.6 3.5 82 300 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   900   11000 9800 0      0    error (invalid witness file) .63 .41 8.6 41 error (invalid witness file) 5.8 3.1 120 290 - -
array-examples/standard_init2_false-unreach-call_ground.i out of memory 0 wit inspect 43   42   550 15000 0      0    error (invalid witness file) .52 .35 13   41 error (invalid witness file) 5.8 3.1 120 290 - -
array-examples/standard_init3_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   570 15000 0      0    error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.0 3.1 130 300 - -
array-examples/standard_init4_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   540 15000 0      0    error (invalid witness file) .52 .33 10   43 error (invalid witness file) 6.2 3.3 120 310 - -
array-examples/standard_init5_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   540 15000 0      0    error (invalid witness file) .57 .36 11   40 error (invalid witness file) 5.7 3.1 98 300 - -
array-examples/standard_init6_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   500 15000 0      0    error (invalid witness file) .48 .31 13   40 error (invalid witness file) 5.7 3.1 110 300 - -
array-examples/standard_init7_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   620 15000 0      0    error (invalid witness file) .50 .34 10   39 error (invalid witness file) 5.6 3.0 110 290 - -
array-examples/standard_init8_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   600 15000 0      0    error (invalid witness file) .50 .33 7.2 41 error (invalid witness file) 6.0 3.2 120 290 - -
array-examples/standard_init9_false-unreach-call_ground.i out of memory 0 wit inspect 42   42   570 15000 0      0    error (invalid witness file) .49 .33 9.1 39 error (invalid witness file) 6.2 3.2 95 310 - -
array-examples/standard_minInArray_false-unreach-call_ground.i out of memory 0 wit inspect 320   320   3300 15000 0      0    error (invalid witness file) .55 .34 9.5 42 error (invalid witness file) 5.9 3.1 110 290 - -
array-examples/standard_partition_false-unreach-call_ground.i out of memory 0 wit inspect 40   40   510 15000 0      0    error (invalid witness file) .51 .34 7.7 39 error (invalid witness file) 6.3 3.3 130 320 - -
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 42   42   580 15000 0      0    error (invalid witness file) .51 .33 12   42 error (invalid witness file) 5.4 2.9 110 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 41   40   600 15000 0      0    - - error (invalid witness file) .60 .39 8.8 39 error (invalid witness file) 5.6 3.0 97 290
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i out of memory 0 wit inspect 41   41   560 15000 0      0    - - error (invalid witness file) .61 .38 7.7 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/relax_true-unreach-call.i false(unreach-call) -16 wit inspect 5.7 5.7 48 170 .0082 0    - - timeout 950    900    18000   5200 true 10   5.4 190 360
array-examples/sanfoundry_02_true-unreach-call_ground.i out of memory 0 wit inspect 320   320   3100 15000 0      0    - - error (invalid witness file) .62 .41 5.9 39 error (invalid witness file) 6.4 3.4 90 300
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   900   11000 15000 0      0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.9 3.7 88 310
array-examples/sanfoundry_24_true-unreach-call.i true 2 wit inspect 41   41   520 5500 0      0    - - error 5.0  2.8  50   270 true 10   5.5 210 350
array-examples/sanfoundry_27_true-unreach-call_ground.i out of memory 0 wit inspect 330   330   3500 15000 0      0    - - error (invalid witness file) .54 .36 8.2 39 error (invalid witness file) 7.5 3.9 89 300
array-examples/sanfoundry_43_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   470 15000 0      0    - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 6.0 3.2 110 290
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 0 wit inspect 38   38   470 15000 0      0    - - error (invalid witness file) .53 .34 9.1 42 error (invalid witness file) 5.8 3.1 120 300
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 0 wit inspect 39   39   520 15000 0      0    - - error (invalid witness file) .58 .38 8.6 40 error (invalid witness file) 5.7 3.0 100 310
array-examples/standard_compareModified_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   670 15000 0      0    - - error (invalid witness file) .59 .38 14   43 error (invalid witness file) 5.9 3.2 97 300
array-examples/standard_compare_true-unreach-call_ground.i out of memory 0 wit inspect 190   190   2000 15000 0      0    - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900   900   9100 14000 0      0    - - error (invalid witness file) .49 .30 6.1 40 error (invalid witness file) 7.2 3.8 120 300
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 0 wit inspect 38   38   630 15000 0      0    - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.8 3.1 120 300
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   480 15000 0      0    - - error (invalid witness file) .61 .39 7.8 40 error (invalid witness file) 5.5 3.0 100 280
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   510 15000 0      0    - - error (invalid witness file) .70 .44 8.5 40 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   520 15000 0      0    - - error (invalid witness file) .65 .41 7.9 42 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   470 15000 0      0    - - error (invalid witness file) .53 .35 14   44 error (invalid witness file) 6.5 3.4 100 300
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 0 wit inspect 44   44   510 15000 0      0    - - error (invalid witness file) .65 .42 8.8 41 error (invalid witness file) 6.3 3.3 130 300
array-examples/standard_copy8_true-unreach-call_ground.i out of memory 0 wit inspect 38   38   520 15000 0      0    - - error (invalid witness file) .63 .39 6.7 40 error (invalid witness file) 7.4 3.9 88 300
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 0 wit inspect 39   38   560 15000 0      0    - - error (invalid witness file) .62 .39 8.8 40 error (invalid witness file) 6.1 3.2 120 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 0 wit inspect 41   41   580 15000 0      0    - - error (invalid witness file) .50 .32 10   41 error (invalid witness file) 5.7 3.1 110 290
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 0 wit inspect 41   41   540 15000 0      0    - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.3 3.3 100 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 0 wit inspect 40   40   520 15000 0      0    - - error (invalid witness file) .56 .35 9.2 39 error (invalid witness file) 6.8 3.5 94 290
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 0 wit inspect 41   41   510 15000 0      0    - - error (invalid witness file) .58 .38 10   41 error (invalid witness file) 7.3 3.8 92 300
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   900   9400 12000 0      0    - - error (invalid witness file) .71 .44 9.4 45 error (invalid witness file) 6.2 3.3 110 300
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   900   9600 9800 0      0    - - error (invalid witness file) .57 .36 8.7 39 error (invalid witness file) 6.0 3.1 100 290
array-examples/standard_init2_true-unreach-call_ground.i out of memory 0 wit inspect 43   42   570 15000 0      0    - - error (invalid witness file) .50 .33 8.6 41 error (invalid witness file) 5.9 3.2 130 290
array-examples/standard_init3_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   630 15000 0      0    - - error (invalid witness file) .53 .35 8.0 40 error (invalid witness file) 6.2 3.3 84 290
array-examples/standard_init4_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   550 15000 0      0    - - error (invalid witness file) .56 .37 9.2 39 error (invalid witness file) 5.8 3.1 84 300
array-examples/standard_init5_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   540 15000 0      0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.2 82 290
array-examples/standard_init6_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   580 15000 0      0    - - error (invalid witness file) .57 .36 9.3 40 error (invalid witness file) 6.4 3.4 110 290
array-examples/standard_init7_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   480 15000 0      0    - - error (invalid witness file) .61 .39 7.6 40 error (invalid witness file) 5.9 3.1 110 290
array-examples/standard_init8_true-unreach-call_ground.i out of memory 0 wit inspect 42   42   620 15000 0      0    - - error (invalid witness file) .65 .40 9.4 42 error (invalid witness file) 5.9 3.1 120 290
array-examples/standard_init9_true-unreach-call_ground.i out of memory 0 wit inspect 43   42   510 15000 0      0    - - error (invalid witness file) .64 .40 9.1 40 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_maxInArray_true-unreach-call_ground.i out of memory 0 wit inspect 400   400   4600 15000 0      0    - - error (invalid witness file) .68 .44 7.4 40 error (invalid witness file) 5.9 3.1 110 290
array-examples/standard_minInArray_true-unreach-call_ground.i out of memory 0 wit inspect 330   330   3200 15000 0      0    - - error (invalid witness file) .62 .40 10   40 error (invalid witness file) 6.2 3.2 81 300
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900   900   10000 13000 0      0    - - error (invalid witness file) .66 .42 7.5 40 error (invalid witness file) 5.6 3.0 120 290
array-examples/standard_partial_init_true-unreach-call_ground.i out of memory 0 wit inspect 40   40   520 15000 0      0    - - error (invalid witness file) .61 .38 7.0 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 0 wit inspect 37   36   480 15000 0      0    - - error (invalid witness file) .66 .42 8.6 40 error (invalid witness file) 6.3 3.3 110 300
array-examples/standard_partition_true-unreach-call_ground.i out of memory 0 wit inspect 40   40   520 15000 0      0    - - error (invalid witness file) .61 .39 11   43 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_password_true-unreach-call_ground.i out of memory 0 wit inspect 190   190   2300 15000 0      0    - - error (invalid witness file) .55 .35 12   41 error (invalid witness file) 7.5 3.9 90 300
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900   900   12000 14000 0      0    - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 5.6 3.0 110 300
array-examples/standard_running_true-unreach-call.i out of memory 0 wit inspect 42   42   500 15000 0      0    - - error (invalid witness file) .50 .31 11   39 error (invalid witness file) 6.0 3.1 120 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i out of memory 0 wit inspect 320   320   3600 15000 0      0    - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   900   11000 13000 0      0    - - error (invalid witness file) .56 .35 10   43 error (invalid witness file) 5.8 3.1 88 300
array-examples/standard_strcmp_true-unreach-call_ground.i false(unreach-call) -16 wit inspect 84   84   830 10000 0      0    - - unknown 3.3  1.9  68   270 true 11   5.8 160 360
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 0 wit inspect 40   40   480 15000 0      0    - - error (invalid witness file) .59 .38 8.9 40 error (invalid witness file) 6.2 3.3 130 300
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 0 wit inspect 40   40   530 15000 0      0    - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 5.7 3.0 97 290
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900   900   11000 5600 0      0    - - error (invalid witness file) .67 .43 6.3 43 error (invalid witness file) 6.3 3.3 120 310
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900   900   11000 14000 0      0    - - error (invalid witness file) .64 .40 7.3 39 error (invalid witness file) 6.3 3.3 110 300
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900   900   9800 5700 0      0    - - error (invalid witness file) .62 .39 9.0 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900   900   12000 14000 0      0    - - error (invalid witness file) .61 .38 7.5 39 error (invalid witness file) 5.9 3.2 120 290
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900   900   9700 14000 0      0    - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.9 3.6 92 300
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900   900   8800 5600 0      0    - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.9 3.1 110 290
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900   900   10000 14000 0      0    - - error (invalid witness file) .52 .33 12   42 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900   900   12000 14000 0      0    - - error (invalid witness file) .62 .40 8.1 40 error (invalid witness file) 5.8 3.1 95 300
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900   900   12000 14000 0      0    - - error (invalid witness file) .64 .41 7.6 40 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 260   260   2900 15000 0      0    - - error (invalid witness file) .57 .36 9.8 44 error (invalid witness file) 6.1 3.2 130 300
array-examples/standard_vector_difference_true-unreach-call_ground.i out of memory 0 wit inspect 40   40   520 15000 0      0    - - error (invalid witness file) .62 .39 6.6 41 error (invalid witness file) 5.9 3.2 110 300
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i out of memory 0 wit inspect 41   40   550 15000 0      0    error (invalid witness file) .51 .32 7.8 40 error (invalid witness file) 5.9 3.1 120 300 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 0 wit inspect 41   41   470 15000 0      0    error (invalid witness file) .50 .32 8.5 40 error (invalid witness file) 6.5 3.5 83 300 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 32   31   380 15000 0      0    error (invalid witness file) .51 .33 13   39 error (invalid witness file) 7.4 3.9 93 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900   900   9100 12000 0      0    error (invalid witness file) .47 .30 8.7 39 error (invalid witness file) 5.9 3.1 110 290 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 32   31   460 15000 0      0    error (invalid witness file) .50 .33 12   41 error (invalid witness file) 6.2 3.3 120 300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i out of memory 0 wit inspect 39   38   510 15000 0      0    error (invalid witness file) .51 .33 7.6 39 error (invalid witness file) 6.2 3.2 120 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i out of memory 0 wit inspect 39   38   520 15000 0      0    - - error (invalid witness file) .61 .39 7.7 40 error (invalid witness file) 5.8 3.1 120 300
array-industry-pattern/array_mul_init_true-unreach-call.i out of memory 0 wit inspect 38   37   530 15000 0      0    - - error (invalid witness file) .68 .42 8.3 40 error (invalid witness file) 7.1 3.8 83 290
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   900   11000 10000 0      2.1  - - error (invalid witness file) .58 .36 9.8 39 error (invalid witness file) 7.3 3.8 130 300
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   900   12000 9200 .0082 0    - - error (invalid witness file) .65 .41 8.0 39 error (invalid witness file) 7.1 3.7 120 310
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   900   10000 13000 .0082 0    - - error (invalid witness file) .61 .39 4.5 40 error (invalid witness file) 6.0 3.2 100 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   900   11000 9200 .0082 0    - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.0 3.2 98 300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 0 wit inspect 42   41   510 15000 0      0    - - error (invalid witness file) .64 .40 6.7 39 error (invalid witness file) 6.1 3.2 91 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 0 wit inspect 37   37   520 15000 0      0    - - error (invalid witness file) .52 .33 14   40 error (invalid witness file) 5.5 3.0 98 290
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i out of memory 0 wit inspect 43   43   510 15000 .0082 0    - - error (invalid witness file) .49 .31 10   40 error (invalid witness file) 5.7 3.1 120 290
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   900   11000 9200 .0082 0    - - error (invalid witness file) .64 .41 9.7 40 error (invalid witness file) 6.5 3.4 130 300
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900   900   5900 14000 0      0    - - error (invalid witness file) .48 .32 12   39 error (invalid witness file) 6.2 3.3 110 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 13   13   150 110 0      0    exception 3.8  2.1  68   280 false(unreach-call) 16   9.9 360 420 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 13   13   150 140 0      0    exception 4.6  2.4  100   280 false(unreach-call) 15   8.4 270 490 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 21   21   210 220 0      0    exception 5.6  3.0  120   300 out of memory 84   55   1300 7000 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 56   56   510 450 0      0    exception 6.9  3.7  150   360 out of memory 66   40   1100 7000 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 320   320   2600 1300 0      0    exception 8.8  4.7  170   400 timeout 98   58   960 6300 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 39   39   290 400 0      0    error (invalid witness file) 2.8  1.6  54   170 false(unreach-call) 13   6.7 130 380 - -
reducercommutativity/avg05_true-unreach-call.i timeout 0 wit inspect 900   900   9100 1600 0      0    - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 7.1 3.7 97 310
reducercommutativity/avg10_true-unreach-call.i timeout 0 wit inspect 900   900   9300 2100 0      0    - - error (invalid witness file) .56 .35 10   40 error (invalid witness file) 5.9 3.1 130 300
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   900   8500 3600 0      0    - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.5 3.4 140 310
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900   900   10000 2200 0      0    - - error (invalid witness file) .53 .34 9.7 43 error (invalid witness file) 7.3 3.9 85 300
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900   900   7000 1500 0      0    - - error (invalid witness file) .57 .36 9.1 39 error (invalid witness file) 6.1 3.2 110 300
reducercommutativity/avg_true-unreach-call.i timeout 0 wit inspect 900   900   7000 3300 0      0    - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 6.4 3.4 100 300
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 8.3 8.3 96 84 0      0    - - true 120    110    2300   820 timeout 960   900   20000 1200
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 160   160   2200 1100 0      0    - - timeout 900    890    19000   1900 timeout 960   880   22000 2300
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   900   8600 4200 0      0    - - error (invalid witness file) .70 .45 7.1 40 error (invalid witness file) 5.8 3.1 120 290
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900   900   6400 2600 0      0    - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.9 3.2 120 300
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   900   6100 1800 0      0    - - error (invalid witness file) .54 .34 9.8 39 error (invalid witness file) 5.9 3.1 97 300
reducercommutativity/max_true-unreach-call.i timeout 0 wit inspect 900   900   4400 1700 0      0    - - error (invalid witness file) .62 .41 7.8 40 error (invalid witness file) 5.5 3.0 120 290
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 5.2 5.2 61 73 0      0    - - true 150    140    3200   1000 true 210   150   3700 3300
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 10   10   110 110 0      0    - - timeout 900    890    16000   1400 out of memory 790   670   16000 7000
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 17   17   200 230 0      0    - - timeout 900    890    17000   1500 out of memory 310   210   4100 7000
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect 470   470   5000 1700 0      0    - - timeout 900    890    21000   1900 out of memory 750   610   12000 7000
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900   900   7100 2900 0      0    - - error (invalid witness file) .70 .45 8.2 42 error (invalid witness file) 5.9 3.1 110 300
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 900   900   3600 9400 0      0    - - error (invalid witness file) .60 .37 9.8 40 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 20   20   230 220 0      0    - - timeout 900    890    19000   1000 true 36   22   630 740
reducercommutativity/sum10_true-unreach-call.i timeout 0 wit inspect 900   900   9800 2300 0      .13 - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.5 3.0 100 290
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900   900   10000 3600 0      .13 - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900   900   7300 1600 0      0    - - error (invalid witness file) .51 .34 9.9 40 error (invalid witness file) 6.2 3.3 110 300
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900   900   7600 2000 0      0    - - error (invalid witness file) .63 .38 10   41 error (invalid witness file) 5.5 2.9 120 300
reducercommutativity/sum_true-unreach-call.i timeout 0 wit inspect 900   900   4800 2000 0      0    - - error (invalid witness file) .68 .43 9.3 42 error (invalid witness file) 8.4 4.4 100 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 135 -10 45000 45000 470000 1500000 .049  2.3 135 50 29 1000 3200   135 500 290 7800 32000   135 5800 5600 120000 19000   135 4600 3700 88000 55000  
    correct results 14 22 1200 1200 12000 12000 0      0   0 33 18 670 1800   3 290 180 4100 22000   2 4800 4700 98000 9800   3 4000 3400 78000 29000  
        correct true 8 16 730 730 8400 9000 0      0   0 0 0 0 0   0 0 0 0 0   2 4800 4700 98000 9800   3 4000 3400 78000 29000  
        correct false 6 6 460 460 3900 2700 0      0   0 33 18 670 1800   3 290 180 4100 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 2 -32 89 89 880 10000 .0082 0   0 0 0 0 0   0 0 0 0 0   0 950 900 18000 5400   2 21 11 350 720  
        incorrect true 0
        incorrect false 2 -32 89 89 880 10000 .0082 0   0 0 0 0 0   0 0 0 0 0   0 950 900 18000 5400   0 21 11 350 720  
score (135 tasks, max score: 230) -10
Run set sv-comp17.ReachSafety-Arrays