Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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 timeout 0 wit inspect 900 890 13000 750 180   0      error (invalid witness file) .59 .37 9.1 39 error (invalid witness file) 5.7 3.0 100 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 wit inspect 46 46 640 160 170   0      error (invalid witness file) .50 .33 11   41 error (invalid witness file) 7.2 3.8 86 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 wit inspect 46 46 610 160 170   0      error (invalid witness file) .67 .41 7.9 41 error (invalid witness file) 5.9 3.1 95 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 wit inspect 890 900 10000 330 14   0      error (invalid witness file) .50 .31 12   39 error (invalid witness file) 7.3 3.8 72 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 wit inspect 890 900 8200 330 14   0      error (invalid witness file) .64 .40 8.0 40 error (invalid witness file) 6.4 3.4 86 290 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 0 wit inspect 900 900 9300 1500 120   0      error (invalid witness file) .48 .32 12   39 error (invalid witness file) 7.0 3.7 75 290 - -
array-examples/standard_copy1_false-unreach-call_ground.i unknown 0 wit inspect 79 78 1000 100 260   .13   error (invalid witness file) .56 .38 10   42 error (invalid witness file) 7.3 3.8 100 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i unknown 0 wit inspect 890 900 9700 190 100   0      error (invalid witness file) .56 .37 11   39 error (invalid witness file) 7.5 4.0 73 300 - -
array-examples/standard_copy3_false-unreach-call_ground.i unknown 0 wit inspect 890 900 10000 200 100   0      error (invalid witness file) .65 .42 8.7 41 error (invalid witness file) 6.2 3.3 79 300 - -
array-examples/standard_copy4_false-unreach-call_ground.i unknown 0 wit inspect 890 900 11000 190 98   .13   error (invalid witness file) .64 .42 7.2 41 error (invalid witness file) 6.2 3.3 120 310 - -
array-examples/standard_copy5_false-unreach-call_ground.i unknown 0 wit inspect 900 900 11000 210 100   0      error (invalid witness file) .56 .36 8.9 39 error (invalid witness file) 7.1 3.7 80 300 - -
array-examples/standard_copy6_false-unreach-call_ground.i unknown 0 wit inspect 890 900 9300 240 96   0      error (invalid witness file) .52 .33 10   39 error (invalid witness file) 5.7 3.1 120 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i unknown 0 wit inspect 900 900 9700 270 99   0      error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.8 3.1 110 300 - -
array-examples/standard_copy8_false-unreach-call_ground.i unknown 0 wit inspect 900 900 9900 300 94   0      error (invalid witness file) .60 .38 5.8 40 error (invalid witness file) 6.4 3.4 110 290 - -
array-examples/standard_copy9_false-unreach-call_ground.i unknown 0 wit inspect 900 900 9200 330 110   0      error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.3 3.3 120 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unknown 0 wit inspect 890 900 9900 240 77   0      error (invalid witness file) .65 .41 8.3 41 error (invalid witness file) 6.6 3.5 89 310 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 770 4.2 33      error 3.8  2.1  80   280 timeout 97   59   1100 1200 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 800 4.2 0      error 4.8  2.7  56   270 timeout 97   61   1800 1500 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900 870 14000 710 4.2 0      error 3.8  2.1  78   280 timeout 97   63   1900 2200 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 750 4.2 34      error 3.9  2.2  72   270 timeout 96   58   980 2000 - -
array-examples/standard_init5_false-unreach-call_ground.i unknown 0 wit inspect 900 900 9400 230 110   0      error (invalid witness file) .56 .35 10   40 error (invalid witness file) 5.7 3.0 120 300 - -
array-examples/standard_init6_false-unreach-call_ground.i unknown 0 wit inspect 890 900 11000 240 95   0      error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.3 3.3 130 300 - -
array-examples/standard_init7_false-unreach-call_ground.i unknown 0 wit inspect 890 900 11000 270 110   0      error (invalid witness file) .52 .34 10   39 error (invalid witness file) 8.0 4.2 96 310 - -
array-examples/standard_init8_false-unreach-call_ground.i unknown 0 wit inspect 900 900 8200 290 110   0      error (invalid witness file) .49 .31 9.3 39 error (invalid witness file) 6.8 3.6 79 300 - -
array-examples/standard_init9_false-unreach-call_ground.i unknown 0 wit inspect 900 900 8400 320 97   0      error (invalid witness file) .54 .33 10   39 error (invalid witness file) 7.3 3.8 75 300 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 0 wit inspect 97 97 1400 120 260   0      error (invalid witness file) .53 .34 10   39 error (invalid witness file) 5.8 3.1 120 290 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 4.2 0      error 4.5  2.4  68   280 timeout 97   63   1900 2000 - -
array-examples/standard_running_false-unreach-call.i unknown 0 wit inspect 890 900 11000 310 82   0      error (invalid witness file) .62 .39 9.0 40 error (invalid witness file) 7.8 4.1 90 310 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 900 900 12000 1200 28   0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 5.8 3.1 92 300
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 wit inspect 900 900 8300 260 59   0      - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 5.7 3.0 55 300
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 890 900 11000 190 24   0      - - error (invalid witness file) .61 .40 10   40 error (invalid witness file) 6.2 3.3 100 300
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 0 wit inspect 310 310 3700 180 260   0      - - error (invalid witness file) .61 .39 9.5 40 error (invalid witness file) 5.5 2.9 98 300
array-examples/sanfoundry_10_true-unreach-call_ground.i unknown 0 wit inspect 900 900 9800 180 87   0      - - error (invalid witness file) .55 .34 9.3 42 error (invalid witness file) 5.6 3.0 67 300
array-examples/sanfoundry_24_true-unreach-call.i timeout 0 wit inspect 900 860 12000 3900 4.2 0      - - error 5.1  2.8  44   280 true 9.3 5.1 150 340
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 0 wit inspect 120 110 1500 120 270   0      - - error (invalid witness file) .61 .38 8.3 40 error (invalid witness file) 5.8 3.1 82 290
array-examples/sanfoundry_43_true-unreach-call_ground.i unknown 0 wit inspect 52 51 760 100 170   0      - - error (invalid witness file) .51 .31 13   39 error (invalid witness file) 5.7 3.0 89 290
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 0 wit inspect 46 46 630 160 170   0      - - error (invalid witness file) .63 .41 6.5 39 error (invalid witness file) 5.3 2.8 73 290
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 wit inspect 890 900 8900 380 14   34      - - error (invalid witness file) .57 .36 8.9 45 error (invalid witness file) 5.6 3.0 63 300
array-examples/standard_compareModified_true-unreach-call_ground.i unknown 0 wit inspect 890 900 11000 220 100   0      - - error (invalid witness file) .49 .32 8.7 39 error (invalid witness file) 7.3 3.8 88 310
array-examples/standard_compare_true-unreach-call_ground.i unknown 0 wit inspect 110 110 1300 170 260   .045  - - error (invalid witness file) .65 .40 9.2 40 error (invalid witness file) 5.5 2.9 98 300
array-examples/standard_copy1_true-unreach-call_ground.i unknown 0 wit inspect 900 900 9200 200 110   0      - - error (invalid witness file) .66 .42 8.0 43 error (invalid witness file) 5.9 3.1 52 310
array-examples/standard_copy2_true-unreach-call_ground.i unknown 0 wit inspect 900 900 8400 260 83   0      - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.5 3.4 110 310
array-examples/standard_copy3_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9300 300 73   0      - - error (invalid witness file) .64 .41 7.6 41 error (invalid witness file) 6.9 3.7 110 300
array-examples/standard_copy4_true-unreach-call_ground.i unknown 0 wit inspect 890 900 10000 330 62   0      - - error (invalid witness file) .64 .41 7.0 39 error (invalid witness file) 5.9 3.1 76 290
array-examples/standard_copy5_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9700 270 54   0      - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 6.2 3.2 82 300
array-examples/standard_copy6_true-unreach-call_ground.i unknown 0 wit inspect 890 900 8400 270 55   0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.7 3.1 67 300
array-examples/standard_copy7_true-unreach-call_ground.i unknown 0 wit inspect 890 900 8900 310 49   0      - - error (invalid witness file) .52 .35 12   39 error (invalid witness file) 6.0 3.2 120 290
array-examples/standard_copy8_true-unreach-call_ground.i unknown 0 wit inspect 890 900 12000 400 40   0      - - error (invalid witness file) .63 .40 8.6 43 error (invalid witness file) 5.4 3.0 96 290
array-examples/standard_copy9_true-unreach-call_ground.i unknown 0 wit inspect 890 900 7600 340 39   0      - - error (invalid witness file) .68 .43 8.6 40 error (invalid witness file) 5.5 2.9 57 290
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unknown 0 wit inspect 900 900 10000 160 93   0      - - error (invalid witness file) .64 .41 8.7 42 error (invalid witness file) 7.0 3.6 110 320
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unknown 0 wit inspect 890 900 12000 220 70   0      - - error (invalid witness file) .66 .42 7.2 40 error (invalid witness file) 7.1 3.7 110 320
array-examples/standard_copyInitSum_true-unreach-call_ground.i unknown 0 wit inspect 890 900 8100 180 80   0      - - error (invalid witness file) .58 .36 12   44 error (invalid witness file) 5.7 3.0 81 300
array-examples/standard_copyInit_true-unreach-call_ground.i unknown 0 wit inspect 890 900 11000 220 78   .13   - - error (invalid witness file) .49 .33 9.3 41 error (invalid witness file) 7.1 3.7 63 300
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 2200 4.2 0      - - error 3.7  2.1  65   270 timeout 960   790   15000 3900
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 730 4.2 0      - - error 3.9  2.2  62   270 timeout 960   790   15000 3600
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 730 4.2 0      - - error 4.6  2.6  29   270 timeout 960   830   14000 4200
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 790 4.2 0      - - error 3.9  2.2  90   270 timeout 960   850   18000 4400
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 740 4.2 0      - - error 4.0  2.2  53   270 timeout 960   850   17000 4800
array-examples/standard_init5_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9600 210 98   0      - - error (invalid witness file) .51 .34 12   39 error (invalid witness file) 7.3 3.8 60 310
array-examples/standard_init6_true-unreach-call_ground.i unknown 0 wit inspect 890 900 12000 240 100   0      - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 5.7 3.1 74 300
array-examples/standard_init7_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9200 270 110   0      - - error (invalid witness file) .66 .41 8.1 39 error (invalid witness file) 5.1 2.8 55 290
array-examples/standard_init8_true-unreach-call_ground.i unknown 0 wit inspect 890 900 12000 290 99   0      - - error (invalid witness file) .56 .36 9.6 40 error (invalid witness file) 5.5 2.9 92 300
array-examples/standard_init9_true-unreach-call_ground.i unknown 0 wit inspect 900 900 9700 320 100   0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.8 3.1 99 290
array-examples/standard_maxInArray_true-unreach-call_ground.i unknown 0 wit inspect 120 120 1600 150 260   33      - - error (invalid witness file) .55 .36 9.8 40 error (invalid witness file) 5.4 2.9 110 300
array-examples/standard_minInArray_true-unreach-call_ground.i unknown 0 wit inspect 100 99 1500 120 260   0      - - error (invalid witness file) .48 .30 11   39 error (invalid witness file) 5.9 3.1 82 300
array-examples/standard_palindrome_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9200 160 80   0      - - error (invalid witness file) .49 .30 12   40 error (invalid witness file) 5.2 2.8 80 290
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 1400 4.2 0      - - error 4.4  2.4  49   270 timeout 960   820   21000 3800
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2300 4.2 0      - - error 4.0  2.2  80   280 timeout 960   830   17000 3700
array-examples/standard_partition_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9200 250 90   0      - - error (invalid witness file) .49 .31 8.4 40 error (invalid witness file) 5.6 3.0 80 300
array-examples/standard_password_true-unreach-call_ground.i unknown 0 wit inspect 110 110 1400 170 260   0      - - error (invalid witness file) .58 .37 7.3 39 error (invalid witness file) 5.7 3.0 88 300
array-examples/standard_reverse_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9300 180 98   0      - - error (invalid witness file) .52 .34 9.2 41 error (invalid witness file) 5.9 3.2 76 300
array-examples/standard_running_true-unreach-call.i unknown 0 wit inspect 890 900 9400 260 77   0      - - error (invalid witness file) .64 .41 7.9 40 error (invalid witness file) 6.0 3.2 110 290
array-examples/standard_sentinel_true-unreach-call_true-termination.i unknown 0 wit inspect 100 100 1300 75 260   0      - - error (invalid witness file) .52 .33 13   39 error (invalid witness file) 6.2 3.3 52 320
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 740 4.2 0      - - error 4.0  2.2  57   270 timeout 960   790   15000 4200
array-examples/standard_strcmp_true-unreach-call_ground.i unknown 0 wit inspect 120 120 1400 130 260   .0041 - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.3 2.8 81 290
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900 860 12000 2200 4.2 0      - - error 4.3  2.4  62   270 timeout 960   780   18000 3500
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 0 wit inspect 890 900 9900 300 62   0      - - error (invalid witness file) .58 .36 11   39 error (invalid witness file) 5.2 2.8 48 300
array-examples/standard_two_index_01_true-unreach-call.i unknown 0 wit inspect 890 900 12000 230 93   21      - - error (invalid witness file) .50 .33 11   41 error (invalid witness file) 6.0 3.2 100 290
array-examples/standard_two_index_02_true-unreach-call.i unknown 0 wit inspect 890 900 8800 210 100   0      - - error (invalid witness file) .67 .43 7.9 41 error (invalid witness file) 5.7 3.0 77 300
array-examples/standard_two_index_03_true-unreach-call.i unknown 0 wit inspect 890 900 9700 220 100   0      - - error (invalid witness file) .56 .36 12   42 error (invalid witness file) 5.6 3.0 86 300
array-examples/standard_two_index_04_true-unreach-call.i unknown 0 wit inspect 890 900 9900 170 100   0      - - error (invalid witness file) .48 .31 10   39 error (invalid witness file) 5.3 2.9 69 310
array-examples/standard_two_index_05_true-unreach-call.i unknown 0 wit inspect 890 900 8800 180 93   0      - - error (invalid witness file) .65 .41 9.5 41 error (invalid witness file) 5.9 3.1 99 300
array-examples/standard_two_index_06_true-unreach-call.i unknown 0 wit inspect 900 900 9200 170 95   0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.3 2.8 79 290
array-examples/standard_two_index_07_true-unreach-call.i unknown 0 wit inspect 900 900 8700 190 100   0      - - error (invalid witness file) .48 .31 8.3 42 error (invalid witness file) 5.6 3.0 74 300
array-examples/standard_two_index_08_true-unreach-call.i unknown 0 wit inspect 890 900 9800 180 95   0      - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.4 3.4 87 300
array-examples/standard_two_index_09_true-unreach-call.i unknown 0 wit inspect 890 900 9900 170 98   0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 5.5 3.0 98 280
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 97 96 1400 100 260   0      - - error (invalid witness file) .53 .35 9.2 41 error (invalid witness file) 6.1 3.3 110 290
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 4.2 0      - - error 5.1  2.8  47   280 timeout 960   790   14000 3800
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i unknown 0 wit inspect 890 900 8900 320 130   0      error (invalid witness file) .65 .41 8.0 41 error (invalid witness file) 7.7 4.0 100 310 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 wit inspect 890 900 8300 310 130   0      error (invalid witness file) .58 .37 11   43 error (invalid witness file) 5.7 3.1 120 300 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i unknown 0 wit inspect 890 900 9600 230 67   0      error (invalid witness file) .61 .39 11   42 error (invalid witness file) 7.2 3.8 61 310 - -
array-industry-pattern/array_range_init_false-unreach-call.i unknown 0 wit inspect 900 900 8500 190 81   0      error (invalid witness file) .66 .42 7.9 39 error (invalid witness file) 6.2 3.3 70 300 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i unknown 0 wit inspect 890 900 11000 250 42   0      error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.1 3.2 56 300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900 590 8700 6000 4.3 34      timeout 92    75    1400   3200 timeout 97   58   1200 1400 - -
array-industry-pattern/array_monotonic_true-unreach-call.i unknown 0 wit inspect 890 900 12000 340 72   34      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.9 3.6 81 310
array-industry-pattern/array_mul_init_true-unreach-call.i unknown 0 wit inspect 890 900 10000 1700 48   0      - - error (invalid witness file) .60 .37 7.2 40 error (invalid witness file) 6.3 3.3 110 310
array-industry-pattern/array_of_struct_break_true-unreach-call.i unknown 0 wit inspect 890 900 9400 210 85   0      - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.2 3.2 76 310
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900 600 10000 3800 4.2 0      - - timeout 900    890    15000   3100 timeout 960   940   11000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 wit inspect 530 530 4900 670 260   0      - - error (invalid witness file) .64 .41 8.7 41 error (invalid witness file) 6.8 3.5 50 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900 610 8200 4100 4.2 0      - - timeout 900    890    14000   3400 timeout 960   940   11000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 wit inspect 890 900 9300 240 54   0      - - error (invalid witness file) .72 .45 9.2 44 error (invalid witness file) 5.7 3.0 96 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 wit inspect 890 900 8600 360 77   0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.8 3.1 93 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unknown 0 wit inspect 890 900 7900 400 76   .13   - - error (invalid witness file) .66 .42 7.2 40 error (invalid witness file) 5.8 3.1 67 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unknown 0 wit inspect 890 900 8700 370 62   0      - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 7.7 4.1 60 300
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900 540 8100 3600 4.2 0      - - timeout 910    900    15000   5600 timeout 960   800   12000 2800
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 490 490 5700 180 14   0      false(unreach-call) 6.2  3.8  110   380 false(unreach-call) 23   14   400 650 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 500 500 5800 180 26   0      false(unreach-call) 10    6.2  100   400 out of memory 79   52   700 7000 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 650 650 9000 180 61   0      false(unreach-call) 13    8.4  180   470 timeout 93   59   810 7000 - -
reducercommutativity/rangesum40_false-unreach-call.i unknown 0 wit inspect 890 900 11000 180 64   .020  error (invalid witness file) .65 .42 8.0 40 error (invalid witness file) 7.0 3.7 69 300 - -
reducercommutativity/rangesum60_false-unreach-call.i unknown 0 wit inspect 900 900 9100 180 64   .10   error (invalid witness file) .52 .33 10   41 error (invalid witness file) 5.5 2.9 76 290 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 490 490 6000 180 10   0      false(unreach-call) 6.6  4.0  110   380 false(unreach-call) 17   9.6 220 450 - -
reducercommutativity/avg05_true-unreach-call.i timeout 0 wit inspect 900 890 9100 2200 14   0      - - timeout 900    900    14000   1800 true 140   120   2400 1200
reducercommutativity/avg10_true-unreach-call.i timeout 0 wit inspect 900 890 8800 3600 27   .65   - - timeout 900    890    20000   3500 timeout 960   920   15000 1500
reducercommutativity/avg20_true-unreach-call.i unknown 0 wit inspect 900 900 7800 700 53   .54   - - timeout 900    890    15000   6500 timeout 960   860   19000 4100
reducercommutativity/avg40_true-unreach-call.i unknown 0 wit inspect 890 900 7800 270 52   .10   - - error (invalid witness file) .66 .41 9.4 44 error (invalid witness file) 5.7 3.1 120 290
reducercommutativity/avg60_true-unreach-call.i unknown 0 wit inspect 890 900 7900 270 54   .10   - - error (invalid witness file) .60 .37 10   40 error (invalid witness file) 6.5 3.4 120 300
reducercommutativity/avg_true-unreach-call.i unknown 0 wit inspect 890 900 11000 180 11   .10   - - error (invalid witness file) .70 .45 8.7 41 error (invalid witness file) 5.8 3.1 71 300
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890 9500 1600 14   .10   - - true 110    100    1400   810 timeout 960   910   15000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880 9500 2500 27   .11   - - timeout 900    890    15000   1800 timeout 960   890   13000 2200
reducercommutativity/max20_true-unreach-call.i unknown 0 wit inspect 890 900 12000 190 51   .10   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.6 3.0 78 300
reducercommutativity/max40_true-unreach-call.i unknown 0 wit inspect 890 900 9400 230 65   .10   - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 5.6 3.0 97 300
reducercommutativity/max60_true-unreach-call.i unknown 0 wit inspect 890 900 8200 250 65   .57   - - error (invalid witness file) .58 .38 11   41 error (invalid witness file) 5.6 3.0 71 300
reducercommutativity/max_true-unreach-call.i unknown 0 wit inspect 890 900 11000 260 4.2 .10   - - timeout 900    890    12000   3100 timeout 960   920   16000 4100
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 850 790 11000 1400 10   0      - - true 140    130    3100   1000 true 210   150   3100 2900
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900 540 8400 4800 19   .10   - - timeout 900    890    13000   1300 out of memory 770   650   9400 7000
reducercommutativity/sep20_true-unreach-call.i unknown 0 wit inspect 890 900 12000 190 36   0      - - timeout 900    890    11000   1300 out of memory 350   230   3100 7000
reducercommutativity/sep40_true-unreach-call.i unknown 0 wit inspect 900 900 10000 190 69   .10   - - error (invalid witness file) .53 .34 11   42 error (invalid witness file) 5.5 2.9 84 290
reducercommutativity/sep60_true-unreach-call.i unknown 0 wit inspect 900 900 11000 190 100   0      - - error (invalid witness file) .53 .34 11   39 error (invalid witness file) 5.3 2.8 78 290
reducercommutativity/sep_true-unreach-call.i unknown 0 wit inspect 890 900 8400 190 4.2 0      - - timeout 900    890    15000   2700 out of memory 610   500   8000 7000
reducercommutativity/sum05_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890 11000 3900 14   0      - - timeout 900    890    16000   1000 true 35   22   740 740
reducercommutativity/sum10_true-unreach-call.i timeout 0 wit inspect 900 890 11000 2400 27   0      - - timeout 900    890    31000   2100 true 110   71   1600 1200
reducercommutativity/sum20_true-unreach-call.i unknown 0 wit inspect 900 900 7900 240 52   .020  - - timeout 910    890    12000   6700 timeout 960   910   12000 5100
reducercommutativity/sum40_true-unreach-call.i unknown 0 wit inspect 890 900 7500 270 47   .10   - - error (invalid witness file) .59 .38 10   42 error (invalid witness file) 5.8 3.1 93 300
reducercommutativity/sum60_true-unreach-call.i unknown 0 wit inspect 890 900 8700 200 52   .10   - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.1 3.2 96 300
reducercommutativity/sum_true-unreach-call.i unknown 0 wit inspect 890 900 10000 240 4.2 .10   - - timeout 900    890    14000   3900 timeout 960   950   13000 4800
../../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 6 110000 100000 1200000 93000 11000 230   135 170 120 2500 7400   135 990 600 14000 34000   135 14000 14000 240000 55000   135 22000 19000 340000 120000  
    correct results 5 6 3000 2900 38000 2100 120 0   4 36 22 500 1600   2 210 140 2100 15000   1 140 130 3100 1000   1 210 150 3100 2900  
        correct true 1 2 850 790 11000 1400 10 0   0 0 0 0 0   0 0 0 0 0   1 140 130 3100 1000   1 210 150 3100 2900  
        correct false 4 4 2100 2100 27000 730 110 0   4 36 22 500 1600   2 210 140 2100 15000   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) 6
Run set sv-comp17.ReachSafety-Arrays