Tool SMACK+Corral 1.7.2
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:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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 false(unreach-call) 1 wit inspect 2.7 2.7 29 85 .90 0      unknown 3.7 2.0 66 280 true 7.3 3.9 110 320 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i false(unreach-call) 1 wit inspect 2.2 2.1 25 94 .95 0      unknown 3.1 1.8 43 270 true 9.4 5.0 100 330 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.2 2.1 27 90 .95 0      unknown 3.4 1.9 68 270 true 9.6 5.0 87 340 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i false(unreach-call) 1 wit inspect 18   17   230 560 1.5  0      unknown 3.5 2.0 75 280 true 31   18   380 710 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 120   120   1400 650 2.0  0      unknown 3.8 2.1 76 270 true 24   14   400 670 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 20   19   240 130 .87 0      unknown 4.0 2.2 49 280 timeout 98   59   950 6900 - -
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.7 25 83 .87 .0082 unknown 3.4 1.9 70 270 true 8.7 4.6 62 320 - -
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.8 26 77 .91 0      unknown 3.1 1.7 45 270 true 9.7 5.1 97 330 - -
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 23 80 .94 0      unknown 3.3 1.9 56 270 true 7.7 4.1 62 320 - -
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.0 2.0 25 85 .97 0      unknown 3.4 1.9 78 260 true 6.6 3.5 91 310 - -
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.0 2.0 28 83 1.0  0      unknown 3.4 1.9 60 270 true 7.2 3.8 74 320 - -
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.1 2.1 26 88 1.0  0      unknown 3.6 2.0 71 270 true 6.9 3.6 53 320 - -
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.2 2.1 27 91 1.1  0      unknown 3.3 1.9 53 260 true 9.5 5.1 110 320 - -
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.3 2.2 25 93 1.1  0      unknown 3.3 1.9 60 270 true 7.2 3.8 65 320 - -
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.3 2.2 28 93 1.2  0      unknown 3.2 1.8 51 260 true 6.9 3.7 95 320 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 29 84 .93 0      unknown 3.1 1.8 48 270 true 7.5 4.0 100 330 - -
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.7 1.7 23 77 .84 0      unknown 3.4 1.9 61 270 true 7.3 3.9 81 330 - -
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.7 1.7 23 85 .87 0      unknown 3.1 1.8 64 270 true 7.6 4.0 56 330 - -
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.7 23 86 .88 0      unknown 3.3 1.8 67 270 true 7.2 3.9 100 320 - -
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.7 23 82 .89 0      unknown 3.2 1.8 54 280 true 7.4 3.9 110 320 - -
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.8 21 79 .91 0      unknown 3.3 1.8 43 270 true 9.6 5.0 85 330 - -
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8 1.9 22 86 .93 0      unknown 3.2 1.8 56 270 true 8.7 4.7 97 310 - -
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 25 80 .94 .49   unknown 3.2 1.8 43 260 true 9.1 4.8 130 340 - -
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 26 78 .97 0      unknown 3.2 1.8 68 270 true 9.1 4.8 110 320 - -
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 26 81 .98 0      unknown 3.2 1.8 59 270 true 6.8 3.6 57 310 - -
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.9 1.9 23 90 .89 0      unknown 3.4 1.9 67 270 true 8.3 4.5 130 330 - -
array-examples/standard_partition_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.0 2.0 29 91 1.0  0      unknown 3.4 1.9 63 270 true 7.5 4.1 110 330 - -
array-examples/standard_running_false-unreach-call.i false(unreach-call) 1 wit inspect 2.3 2.3 23 100 1.1  16      unknown 3.3 1.9 71 270 true 6.7 3.6 44 320 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 2.3 2.2 27 100 .94 0      - - error 4.4  2.5  78   280 true 12   6.3 130 340
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i true 2 wit inspect 880   880   9900 220 .91 2.2    - - error 4.4  2.5  65   270 timeout 960   820   20000 4800
array-examples/relax_true-unreach-call.i true 2 wit inspect 880   880   11000 370 .98 0      - - timeout 910    880    19000   5800 timeout 960   910   26000 1300
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 wit inspect 1.5 1.5 21 77 1.1  0      - - error 5.1  2.8  43   270 timeout 960   840   20000 3300
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 wit inspect 4.2 4.1 60 91 .87 0      - - out of memory 600    570    16000   7000 timeout 960   780   19000 2600
array-examples/sanfoundry_24_true-unreach-call.i true 2 wit inspect 880   880   12000 310 .87 0      - - error 3.9  2.1  80   270 true 11   6.1 140 340
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect 1.8 1.9 20 77 .89 0      - - error 4.0  2.2  79   270 timeout 960   820   20000 3800
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 1.2 1.2 14 69 .91 0      - - true 4.3  2.4  36   270 true 7.4 4.0 130 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i true 2 wit inspect 23   23   260 140 .95 0      - - error 3.8  2.1  65   280 timeout 960   820   28000 3900
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 880   930   9900 770 1.5  0      - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 7.3 3.9 81 300
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect 1.4 1.4 20 75 1.0  0      - - error 3.6  2.0  71   270 timeout 960   820   26000 4100
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect 1.7 1.8 21 74 .89 0      - - error 3.5  2.0  48   270 timeout 960   800   22000 4300
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 1.6 1.6 29 82 .87 0      - - error 4.5  2.5  63   270 timeout 960   800   24000 3700
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 1.8 1.8 20 78 .91 .0041 - - error 3.7  2.0  57   270 timeout 960   840   26000 4300
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 1.8 1.8 20 83 .94 0      - - error 3.9  2.2  72   270 timeout 960   840   18000 4700
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 1.9 1.9 25 87 .97 0      - - error 3.8  2.2  76   270 timeout 960   850   22000 4700
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 2.0 2.0 26 87 1.0  0      - - error 3.7  2.1  75   270 timeout 960   860   29000 4700
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 2.1 2.1 28 90 1.0  0      - - error 4.4  2.5  66   270 timeout 960   860   26000 4700
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 2.2 2.2 28 94 1.1  0      - - error 3.8  2.2  70   270 timeout 960   870   27000 4800
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 2.5 2.4 28 92 1.1  0      - - error 4.8  2.6  59   270 timeout 960   860   33000 4700
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect 2.5 2.4 30 100 1.2  0      - - error 4.9  2.7  58   280 timeout 960   870   26000 5000
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 2.1 2.1 28 83 .93 0      - - error 4.4  2.5  63   270 timeout 960   850   23000 4800
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 2.5 2.5 35 88 .98 0      - - error 4.2  2.3  57   270 timeout 960   860   18000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 2.0 2.0 24 81 .94 0      - - error 4.7  2.6  50   270 timeout 960   850   22000 4800
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 1.7 1.7 22 78 .88 0      - - error 3.9  2.2  62   270 timeout 960   840   29000 4000
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 2.4 2.4 27 81 .88 0      - - error 4.5  2.5  63   270 timeout 960   790   19000 3900
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 1.5 1.5 19 74 .84 0      - - error 3.5  2.0  67   270 timeout 960   790   17000 3100
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 1.6 1.6 22 86 .87 0      - - error 4.5  2.6  48   270 timeout 960   820   15000 3600
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 1.7 1.6 22 78 .88 0      - - error 4.8  2.7  58   270 timeout 960   850   21000 3900
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 1.8 1.8 21 75 .89 0      - - error 3.7  2.1  81   270 timeout 960   850   16000 4800
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 1.9 1.9 23 78 .91 0      - - error 5.1  2.9  49   280 timeout 960   860   24000 4700
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 1.9 1.9 23 83 .93 0      - - error 3.7  2.1  76   270 timeout 960   860   21000 4700
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 2.0 2.0 24 84 .94 0      - - error 4.3  2.4  71   270 timeout 960   860   22000 4800
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 2.0 2.0 24 86 .97 0      - - error 3.8  2.1  59   270 timeout 960   870   23000 4700
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 2.1 2.1 27 81 .98 0      - - error 4.9  2.7  53   280 timeout 960   860   15000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect 1.9 1.9 24 73 .89 0      - - error 3.8  2.1  69   270 timeout 960   820   17000 3500
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect 1.9 1.9 24 73 .89 0      - - error 4.9  2.7  57   270 timeout 960   820   23000 3500
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect 1.4 1.4 18 81 .86 0      - - error 3.8  2.2  67   270 timeout 960   800   21000 4100
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 wit inspect 120   120   1700 100 .94 0      - - error 4.4  2.5  57   270 timeout 960   810   22000 3600
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 wit inspect 64   64   820 95 .97 0      - - error 3.8  2.1  53   270 timeout 960   820   20000 3700
array-examples/standard_partition_true-unreach-call_ground.i true 2 wit inspect 21   21   330 86 1.0  0      - - error 4.7  2.6  60   280 timeout 960   850   27000 4700
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect 1.7 1.6 20 82 .91 0      - - error 3.8  2.1  60   280 timeout 960   800   16000 3900
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect 1.7 1.6 25 80 .87 0      - - error 3.6  2.0  65   270 timeout 960   800   17000 4000
array-examples/standard_running_true-unreach-call.i true 2 wit inspect 1.7 1.8 25 71 1.0  0      - - error 3.7  2.1  52   280 timeout 960   850   20000 4700
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 1.6 1.6 20 86 .84 0      - - error 3.8  2.1  66   280 true 14   7.3 260 380
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect 1.7 1.7 22 79 .87 0      - - error 3.8  2.1  70   270 timeout 960   790   22000 3700
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect 1.7 1.7 20 74 .89 0      - - error 3.7  2.1  79   270 timeout 960   800   13000 4800
array-examples/standard_strcpy_original_true-unreach-call.i true 2 wit inspect 6.1 6.0 77 97 .88 0      - - error 3.8  2.1  77   270 timeout 960   790   23000 3700
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 wit inspect 4.2 4.2 64 90 .88 0      - - error 4.6  2.6  50   270 timeout 960   790   25000 4000
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 880   930   13000 900 .84 0      - - error (invalid witness file) .57 .37 8.7 41 error (invalid witness file) 8.0 4.2 83 320
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect 1.5 1.4 19 79 .86 0      - - error 3.9  2.1  75   280 timeout 960   800   22000 2700
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900   930   12000 4100 12    0      - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 7.0 3.7 58 290
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect 1.4 1.5 17 95 .84 17      - - error 4.6  2.5  51   270 timeout 960   810   19000 2600
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect 1.4 1.4 16 83 .84 0      - - error 4.6  2.6  51   270 timeout 960   810   17000 2600
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 890   930   11000 1000 6.3  0      - - error (invalid witness file) .73 .46 8.4 45 error (invalid witness file) 7.6 4.0 110 320
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect 1.4 1.4 17 76 .84 0      - - error 4.8  2.6  37   290 timeout 960   820   26000 2800
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect 1.4 1.5 16 80 .84 0      - - error 4.6  2.5  53   280 timeout 960   820   26000 2700
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect 1.3 1.3 18 75 .84 0      - - error 4.9  2.7  58   280 timeout 960   830   23000 2600
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 wit inspect 880   880   12000 480 .86 .0041 - - error 4.0  2.2  57   270 timeout 960   820   21000 2500
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 2.1 2.1 22 76 .89 0      - - error 4.7  2.6  46   270 timeout 960   790   24000 3500
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect 1.8 1.7 21 81 .86 0      unknown 3.2 1.8 63 270 true 8.6 4.6 97 330 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect 1.8 1.7 22 80 .86 0      timeout 96   88   2400 1700 timeout 97   90   2000 4600 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i false(unreach-call) 1 wit inspect 2.5 2.4 27 88 1.0  0      unknown 3.5 2.0 63 270 true 11   5.8 160 370 - -
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 1.8 1.7 25 87 .89 0      unknown 3.4 1.9 67 270 timeout 96   87   1200 4800 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i false(unreach-call) 1 wit inspect 2.5 2.4 30 94 1.0  0      unknown 3.7 2.1 80 280 true 9.7 5.2 140 350 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i false(unreach-call) 1 wit inspect 4.9 4.8 64 110 .90 0      timeout 97   79   1800 3800 true 7.4 3.9 84 330 - -
array-industry-pattern/array_monotonic_true-unreach-call.i true 2 wit inspect 1.6 1.6 17 75 .88 0      - - error 3.4  1.9  59   270 timeout 960   840   22000 3200
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 880   930   13000 170 .97 0      - - error (invalid witness file) .53 .34 12   44 error (invalid witness file) 7.5 4.0 86 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect 1.7 1.7 19 80 .88 0      - - timeout 900    890    15000   4900 timeout 960   940   16000 4700
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i true 2 wit inspect 4.2 4.2 49 88 .97 0      - - timeout 900    890    15000   3000 timeout 960   940   19000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i true 2 wit inspect 1.8 1.8 22 77 .91 0      - - timeout 910    890    13000   5000 timeout 960   830   28000 4800
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i true 2 wit inspect 1.8 1.8 23 78 .91 0      - - timeout 900    890    16000   3200 timeout 960   940   15000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 880   930   9800 680 .91 0      - - error (invalid witness file) .66 .41 6.5 40 error (invalid witness file) 5.5 2.9 94 290
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i true 2 wit inspect 7.4 7.4 91 94 .96 0      - - timeout 900    890    20000   6600 error 12   6.7 140 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect 1.6 1.6 19 85 .88 0      - - timeout 900    890    16000   4200 timeout 960   940   25000 5300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 2 wit inspect 14   14   200 100 1.1  0      - - timeout 900    890    15000   3500 timeout 960   940   19000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i true 2 wit inspect 880   880   13000 390 .87 0      - - timeout 910    890    18000   6100 timeout 960   810   21000 2600
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 1.6 1.6 22 75 .90 0      false(unreach-call) 5.7 3.7 110 370 true 8.8 4.8 120 350 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 1.7 1.7 20 73 .95 0      false(unreach-call) 8.4 5.4 120 390 true 12   7.1 110 350 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 1.9 1.9 24 75 1.0  .0082 false(unreach-call) 11   7.4 200 450 true 9.0 4.9 100 350 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 2.3 2.2 29 94 1.2  0      false(unreach-call) 12   7.8 230 650 true 11   6.1 140 360 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 2.8 2.7 35 120 1.4  0      false(unreach-call) 16   11   370 690 true 9.4 5.0 130 350 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 2.0 2.0 30 79 .91 0      true 22   17   460 410 false(unreach-call) 15   8.9 250 420 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect 1.3 1.4 17 68 .90 .25   - - timeout 900    900    15000   1700 true 160   130   3300 1200
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect 1.3 1.4 18 67 .93 0      - - timeout 900    890    16000   3400 true 300   260   7100 1700
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect 1.5 1.5 18 84 1.0  0      - - timeout 910    890    15000   6600 timeout 960   850   19000 3900
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect 1.9 1.9 20 130 1.2  0      - - out of memory 470    460    12000   7000 unknown 290   210   4400 4700
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect 2.8 2.8 35 200 1.4  0      - - out of memory 410    400    7400   7000 unknown 390   300   7600 5000
reducercommutativity/avg_true-unreach-call.i true 2 wit inspect 880   880   12000 140 .89 .15   - - timeout 900    890    16000   2700 timeout 960   900   17000 2300
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 1.3 1.4 16 66 .92 0      - - true 110    99    2000   830 timeout 960   900   22000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 1.6 1.6 21 80 1.0  0      - - timeout 900    890    17000   1800 timeout 960   880   25000 2400
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect 3.6 3.6 44 100 1.1  0      - - timeout 900    890    17000   1900 timeout 960   800   23000 4900
reducercommutativity/max40_true-unreach-call.i true 2 wit inspect 26   26   200 180 1.4  0      - - timeout 900    890    15000   2100 timeout 960   790   20000 4800
reducercommutativity/max60_true-unreach-call.i true 2 wit inspect 180   180   1100 320 1.7  0      - - timeout 900    890    15000   3500 timeout 960   800   20000 5000
reducercommutativity/max_true-unreach-call.i true 2 wit inspect 880   880   9200 390 .89 0      - - timeout 900    890    16000   2900 timeout 960   910   17000 3000
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 1.3 1.3 16 67 .91 0      - - true 160    150    2800   980 true 220   160   3700 3200
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 2.2 2.2 28 74 .97 0      - - timeout 900    890    19000   1300 out of memory 870   740   17000 7000
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 880   930   12000 100 1.1  0      - - error (invalid witness file) .70 .44 8.0 45 error (invalid witness file) 7.4 3.9 76 300
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 880   930   11000 160 1.3  0      - - error (invalid witness file) .66 .43 7.7 41 error (invalid witness file) 6.0 3.1 120 300
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 880   930   8800 250 1.6  0      - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 6.3 3.3 97 300
reducercommutativity/sep_true-unreach-call.i true 2 wit inspect 880   880   11000 180 .89 0      - - timeout 900    890    16000   2400 out of memory 730   600   19000 7000
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 1.3 1.3 18 70 .90 0      - - timeout 900    890    19000   1000 true 41   26   630 720
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect 1.3 1.3 23 70 .93 0      - - timeout 900    890    21000   2100 true 110   67   1800 1200
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect 1.4 1.4 16 82 1.0  0      - - timeout 900    890    27000   6800 timeout 960   900   23000 5200
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect 1.8 1.8 23 120 1.2  0      - - out of memory 370    360    12000   7000 unknown 410   330   6600 4700
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect 2.8 2.8 33 200 1.4  .24   - - out of memory 440    420    7300   7000 timeout 960   840   25000 6100
reducercommutativity/sum_true-unreach-call.i true 2 wit inspect 880   880   11000 390 .89 0      - - timeout 900    890    16000   3800 timeout 960   950   31000 4700
../../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 212 17000 17000 210000 23000 150 36 135 370 280 7600 17000   135 650 430 8500 29000   135 24000 24000 470000 140000   135 72000 63000 1600000 330000  
    correct results 126 212 8800 8700 110000 14000 120 36 6 370 280 7600 17000   37 650 430 8500 29000   3 24000 24000 470000 140000   9 72000 63000 1600000 320000  
        correct true 86 172 8500 8500 110000 9900 83 20 1 0 0 0 0   36 0 0 0 0   3 24000 24000 470000 140000   9 72000 63000 1600000 320000  
        correct false 40 40 240 230 2900 4500 40 16 5 370 280 7600 17000   1 650 430 8500 29000   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) 212
Run set sv-comp17.ReachSafety-Arrays