Tool Ceagle Ceagle 1.3 @ 53cfa89
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:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.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/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.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 false(unreach-call) 1 wit inspect .058 .068 .41 11   0   2.7   unknown 3.3 1.8 63 270 true 9.3 4.9 94 320 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i false(unreach-call) 1 wit inspect 24     24     250    8.3 0   0     unknown 3.6 2.0 72 270 true 8.2 4.3 120 320 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 18     18     230    11   0   2.4   unknown 3.3 1.8 78 270 true 8.9 4.7 83 320 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i false(unreach-call) 1 wit inspect .067 .077 .36 11   0   2.5   unknown 3.2 1.8 61 270 true 7.6 4.0 130 320 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .056 .073 .56 13   0   4.7   unknown 3.4 1.9 74 270 true 7.3 3.9 130 320 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 9.2   9.2   130    11   0   2.5   unknown 3.1 1.8 61 260 true 7.2 3.9 120 320 - -
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .053 .056 .31 9.3 0   .89  unknown 3.2 1.8 54 270 true 8.6 4.5 84 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .082 .091 .33 11   0   2.5   unknown 3.4 1.9 65 280 true 9.7 5.1 98 330 - -
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .052 .061 .43 11   0   2.4   unknown 3.3 1.9 75 270 true 12   6.1 99 340 - -
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .044 .045 .41 8.2 0   0     unknown 3.4 1.9 54 270 true 9.0 4.7 130 320 - -
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .076 .076 .33 8.3 0   0     unknown 3.3 1.9 70 270 true 7.2 3.9 110 320 - -
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .053 .053 .38 8.4 0   0     unknown 3.4 1.9 71 270 true 8.7 4.6 100 310 - -
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .050 .060 .41 11   0   2.5   unknown 3.2 1.8 72 270 true 7.7 4.1 130 320 - -
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .062 .078 .45 12   0   4.7   unknown 3.4 1.9 59 270 true 7.3 3.9 160 320 - -
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .055 .065 .46 11   0   2.4   unknown 3.4 1.9 75 280 true 7.1 3.8 160 320 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .049 .051 .37 8.6 0   .025 unknown 3.4 1.9 77 280 true 7.3 3.9 140 320 - -
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .061 .070 .45 11   0   2.4   unknown 3.1 1.8 67 270 true 6.7 3.6 120 310 - -
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .056 .071 .47 13   0   4.7   unknown 3.4 1.9 64 260 true 8.1 4.3 74 310 - -
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .051 .060 .42 11   0   2.5   unknown 3.3 1.8 73 270 true 8.3 4.5 88 310 - -
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .090 .22  .97 49   0   41     unknown 3.3 1.9 74 260 true 8.4 4.5 120 330 - -
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .077 .086 .28 11   0   2.4   unknown 3.2 1.8 47 280 true 6.9 3.7 150 320 - -
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .051 .051 .38 8.3 0   0     unknown 3.2 1.8 59 270 true 8.8 4.6 100 320 - -
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .063 .072 .46 11   0   2.5   unknown 3.3 1.9 64 260 true 7.3 3.9 110 310 - -
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .075 .086 .39 11   0   2.4   unknown 3.4 1.9 70 270 true 8.8 4.7 95 320 - -
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .052 .053 .35 8.4 0   0     unknown 3.3 1.8 64 260 true 7.5 4.0 150 320 - -
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .049 .059 .44 11   0   2.4   unknown 3.2 1.8 54 270 true 8.5 4.6 110 320 - -
array-examples/standard_partition_false-unreach-call_ground.i false(unreach-call) 1 wit inspect .046 .047 .38 8.2 0   0     unknown 3.5 1.9 68 270 true 7.9 4.2 130 320 - -
array-examples/standard_running_false-unreach-call.i false(unreach-call) 1 wit inspect .052 .070 .60 13   0   4.7   unknown 3.5 2.0 70 280 true 7.3 3.9 130 330 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect .055 .065 .47 11   0   2.6   - - error 4.6  2.5  81   280 true 8.9 4.9 170 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i true 2 wit inspect .068 .080 .42 11   0   2.6   - - error 4.3  2.4  65   270 timeout 960   830   19000 4800
array-examples/relax_true-unreach-call.i unknown 0 wit inspect .031 .033 .14 8.2 0   .045 - - error (invalid witness file) .59 .40 8.8 40 error (invalid witness file) 6.1 3.3 100 300
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 wit inspect .047 .047 .49 8.5 0   0     - - error 3.8  2.1  75   270 timeout 960   840   32000 3300
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 wit inspect .067 .084 .37 13   0   4.0   - - out of memory 700    660    12000   7000 timeout 960   790   15000 3100
array-examples/sanfoundry_24_true-unreach-call.i unknown 0 wit inspect .027 .028 .11 7.8 0   0     - - error (invalid witness file) .55 .35 13   44 error (invalid witness file) 6.4 3.4 110 310
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect .11  .11  .30 8.3 0   0     - - error 3.7  2.0  74   270 timeout 960   820   23000 3800
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect .12  .13  .35 11   0   2.4   - - true 3.9  2.2  48   270 true 6.9 3.6 120 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i true 2 wit inspect 26     26     300    12   0   4.6   - - error 3.5  2.0  72   270 timeout 960   820   31000 3800
array-examples/sorting_selectionsort_true-unreach-call_ground.i true 2 wit inspect .45  .46  5.2  11   0   2.4   - - error 4.5  2.5  48   270 timeout 960   790   16000 3900
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect .048 .048 .42 8.2 0   0     - - error 3.7  2.1  50   280 timeout 960   820   25000 3900
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect .070 .079 .39 11   0   2.4   - - error 3.4  1.9  58   270 timeout 960   810   14000 4500
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect .056 .056 .40 8.4 0   0     - - error 4.4  2.5  52   270 timeout 960   800   23000 4000
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect .051 .051 .34 8.2 0   0     - - error 3.8  2.1  85   270 timeout 960   840   21000 4300
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect .059 .060 .39 8.5 0   .074 - - error 3.7  2.1  76   270 timeout 960   860   23000 4800
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect .053 .053 .36 8.4 0   0     - - error 4.8  2.7  54   270 timeout 960   860   17000 4700
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect .075 .091 .45 13   0   4.7   - - error 3.9  2.2  78   270 timeout 960   860   24000 4600
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect .063 .072 .34 11   0   2.4   - - error 4.9  2.7  48   270 timeout 960   870   22000 4800
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect .047 .047 .34 8.3 0   0     - - error 4.5  2.5  51   270 timeout 960   860   24000 4800
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect .078 .087 .34 11   0   2.4   - - error 4.8  2.6  55   270 timeout 960   860   21000 5000
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect .082 .092 .45 11   0   2.5   - - error 4.8  2.6  48   270 timeout 960   870   28000 4700
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect .051 .061 .42 11   0   2.4   - - error 4.8  2.7  43   270 timeout 960   860   21000 4700
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect .061 .072 .33 11   0   2.4   - - error 3.8  2.1  73   280 timeout 960   860   25000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect .058 .059 .32 8.5 0   .025 - - error 3.7  2.0  42   270 timeout 960   850   24000 4500
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect .052 .052 .39 8.4 0   0     - - error 3.7  2.1  68   270 timeout 960   840   16000 4500
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect .046 .057 .54 11   0   2.5   - - error 3.8  2.1  85   280 timeout 960   800   13000 4300
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect .053 .062 .42 11   0   2.4   - - error 3.7  2.1  67   290 timeout 960   790   23000 3700
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect .058 .058 .32 8.2 0   0     - - error 4.1  2.3  48   270 timeout 960   820   24000 3400
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect .10  .11  .34 11   0   2.5   - - error 3.6  2.0  70   270 timeout 960   840   27000 4400
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect .067 .067 .36 8.4 0   0     - - error 4.1  2.3  68   270 timeout 960   850   28000 4800
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect .073 .089 .43 13   0   4.7   - - error 4.6  2.6  52   270 timeout 960   860   20000 4800
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect .049 .049 .39 8.2 0   0     - - error 4.2  2.3  76   290 timeout 960   860   18000 4700
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect .054 .064 .42 11   0   2.3   - - error 3.8  2.1  60   270 timeout 960   860   21000 4700
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect .058 .074 .52 13   0   4.7   - - error 4.1  2.3  55   280 timeout 960   870   25000 4700
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect .087 .10  .41 11   0   2.4   - - error 4.8  2.7  69   280 timeout 960   860   18000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect .078 .094 .39 13   0   4.7   - - error 3.4  1.9  48   270 timeout 960   820   22000 4100
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect .067 .077 .36 11   0   2.5   - - error 4.4  2.5  51   270 timeout 960   820   13000 4400
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect .059 .076 .36 13   0   4.6   - - error 3.6  2.1  75   270 timeout 960   800   18000 4200
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 wit inspect .074 .084 .40 11   0   2.5   - - error 3.8  2.1  76   270 timeout 960   820   24000 3600
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 wit inspect .092 .092 .31 8.2 0   0     - - error 3.6  2.0  77   270 timeout 960   820   15000 4300
array-examples/standard_partition_true-unreach-call_ground.i true 2 wit inspect .098 .11  .31 11   0   2.5   - - error 4.0  2.3  61   270 timeout 960   850   16000 4800
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect .071 .084 .39 11   0   2.4   - - error 3.8  2.1  68   280 timeout 960   800   23000 4500
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect .053 .070 .44 13   0   4.7   - - error 4.4  2.5  56   270 timeout 960   800   21000 3800
array-examples/standard_running_true-unreach-call.i true 2 wit inspect .077 .087 .39 11   0   2.4   - - error 4.4  2.5  69   270 timeout 960   860   21000 4700
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect .066 .076 .41 11   0   2.6   - - error 3.6  2.0  60   280 true 13   6.9 260 390
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect .091 .091 .23 8.1 0   0     - - error 3.6  2.0  55   270 timeout 960   790   17000 3600
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect .058 .068 .47 11   0   2.5   - - error 3.9  2.2  65   270 timeout 960   810   29000 5000
array-examples/standard_strcpy_original_true-unreach-call.i unknown 0 wit inspect .027 .027 .12 7.9 0   0     - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.4 3.4 110 300
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 0 wit inspect .043 .043 .11 7.7 0   0     - - error (invalid witness file) .65 .42 6.8 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect .046 .055 .51 11   0   2.4   - - error 4.1  2.2  81   280 timeout 960   810   19000 2800
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect .050 .050 .38 8.2 0   0     - - error 4.2  2.3  57   280 timeout 960   820   15000 2500
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect .052 .052 .28 8.2 0   0     - - error 4.5  2.5  56   280 timeout 960   830   25000 2800
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect .050 .060 .42 11   0   2.5   - - error 4.6  2.6  54   280 timeout 960   820   20000 2700
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect .070 .081 .40 11   0   2.5   - - error 4.3  2.4  58   270 timeout 960   820   29000 2700
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect .070 .070 .27 8.2 0   0     - - error 3.9  2.2  62   270 timeout 960   820   14000 2700
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect .051 .061 .33 11   0   2.5   - - error 4.5  2.5  57   270 timeout 960   830   21000 2800
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect .071 .071 .34 8.3 0   0     - - error 4.4  2.4  73   280 timeout 960   830   27000 2700
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect .057 .067 .36 11   0   2.5   - - error 4.2  2.3  65   280 timeout 960   830   21000 2900
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 wit inspect .038 .049 .79 11   0   2.5   - - error 4.3  2.4  54   270 timeout 960   810   28000 2900
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect .065 .075 .30 11   0   2.4   - - error 3.5  2.0  43   270 timeout 960   790   18000 4000
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect .052 .052 .34 8.2 0   0     unknown 3.3 1.9 74 270 true 7.7 4.1 100 320 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .11  .29 8.2 0   0     timeout 97   87   2600 1700 timeout 97   90   1900 4600 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i false(unreach-call) 1 wit inspect .051 .061 .53 11   0   2.4   unknown 3.1 1.8 53 270 true 7.4 3.9 110 320 - -
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect .050 .061 .44 11   0   2.4   unknown 3.1 1.8 56 260 timeout 97   90   1600 4500 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i false(unreach-call) 1 wit inspect .087 .096 .47 11   0   2.4   unknown 3.4 1.9 65 260 true 6.7 3.6 100 310 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i false(unreach-call) 1 wit inspect .061 .072 .55 11   0   2.5   timeout 97   81   2500 4100 true 7.6 4.0 160 320 - -
array-industry-pattern/array_monotonic_true-unreach-call.i true 2 wit inspect .052 .055 .41 8.2 0   0     - - error 4.3  2.4  57   270 timeout 960   830   22000 2800
array-industry-pattern/array_mul_init_true-unreach-call.i true 2 wit inspect .064 .074 .50 11   0   2.6   - - error 3.5  2.0  47   270 timeout 960   840   22000 3500
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect .046 .046 .42 8.3 0   0     - - timeout 900    890    15000   4800 timeout 960   940   15000 4900
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i true 2 wit inspect .080 .090 .46 11   0   2.6   - - timeout 900    890    20000   3000 timeout 960   940   18000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i true 2 wit inspect .062 .074 .43 11   0   2.6   - - timeout 900    890    21000   5800 timeout 960   830   13000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i true 2 wit inspect .073 .083 .38 11   0   2.6   - - timeout 900    890    19000   3500 timeout 960   940   10000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i true 2 wit inspect .076 .082 .31 9.9 0   1.5   - - out of memory 380    370    7400   7000 timeout 960   940   19000 5300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i true 2 wit inspect .076 .086 .38 11   0   2.6   - - timeout 910    890    14000   6000 error 10   5.5 140 310
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect .077 .087 .38 11   0   2.5   - - timeout 900    890    18000   4300 timeout 960   940   17000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 2 wit inspect .080 .081 .49 8.4 0   .16  - - timeout 900    890    18000   3600 timeout 960   940   14000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i true 2 wit inspect .070 .088 .39 13   0   4.5   - - timeout 910    900    9900   6400 timeout 960   810   23000 2700
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect .052 .052 .32 8.3 0   0     false(unreach-call) 5.6 3.4 110 380 true 7.9 4.2 140 320 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect .049 .059 .50 11   0   2.4   false(unreach-call) 7.0 4.3 140 380 true 10   5.8 120 310 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect .057 .067 .33 11   0   2.3   false(unreach-call) 9.6 6.2 220 450 true 9.0 4.8 130 320 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect .059 .077 .37 13   0   4.6   false(unreach-call) 14   8.9 290 630 true 8.1 4.3 160 330 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect .056 .074 .62 13   0   4.8   false(unreach-call) 19   12   360 720 true 7.3 3.9 150 310 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect .075 .083 .35 10   0   1.6   timeout 98   82   2800 3100 true 9.5 5.0 79 320 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect .028 .028 .13 7.9 0   .11  - - timeout 900    900    20000   1800 true 190   160   5400 1100
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect .029 .030 .11 7.9 0   0     - - timeout 900    890    14000   3400 true 310   270   8600 1600
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect .035 .036 .13 8.0 0   .11  - - timeout 910    900    17000   6600 timeout 960   860   23000 4100
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect .032 .033 .12 7.7 0   .045 - - out of memory 530    520    9000   7000 unknown 220   170   5000 4700
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect .021 .021 .15 7.7 0   0     - - out of memory 400    390    8000   7000 unknown 360   280   8200 5000
reducercommutativity/avg_true-unreach-call.i aborted 0 wit inspect .11  .11  1.3  8.1 0   .23  - - error (invalid witness file) .69 .44 7.9 44 error (invalid witness file) 5.9 3.2 120 290
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect .026 .026 .13 7.8 0   0     - - true 94    84    1500   820 timeout 960   910   26000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect .034 .034 .15 7.7 0   0     - - timeout 900    890    20000   1800 timeout 960   880   12000 2400
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect .018 .019 .14 7.9 0   .11  - - timeout 900    890    16000   1800 timeout 960   810   23000 5200
reducercommutativity/max40_true-unreach-call.i true 2 wit inspect .027 .028 .11 8.0 0   .22  - - timeout 900    890    20000   2100 timeout 960   790   19000 4900
reducercommutativity/max60_true-unreach-call.i true 2 wit inspect .022 .022 .12 7.8 0   0     - - timeout 900    890    25000   3500 timeout 960   800   22000 5100
reducercommutativity/max_true-unreach-call.i aborted 0 wit inspect .11  .11  1.1  7.9 0   .20  - - error (invalid witness file) .49 .31 6.5 40 error (invalid witness file) 6.4 3.4 87 300
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect .029 .029 .13 7.9 0   .11  - - true 170    160    3100   980 true 240   170   4600 2700
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect .021 .021 .16 7.8 0   0     - - timeout 900    890    15000   1300 out of memory 770   650   18000 7000
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect .026 .027 .13 7.9 0   .11  - - timeout 900    890    17000   1200 out of memory 320   220   3000 7000
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect .021 .021 .17 7.8 0   0     - - timeout 900    890    19000   1800 out of memory 800   640   19000 7000
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect .032 .033 .12 7.7 0   0     - - timeout 900    890    14000   3600 timeout 960   820   15000 5600
reducercommutativity/sep_true-unreach-call.i aborted 0 wit inspect .14  .14  1.1  8.0 0   .094 - - error (invalid witness file) .56 .36 9.2 40 error (invalid witness file) 6.1 3.2 120 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect .020 .020 .14 7.9 0   0     - - timeout 900    900    20000   1100 true 36   23   850 720
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect .017 .017 .18 7.9 0   0     - - timeout 900    890    25000   2000 true 90   58   2200 1300
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect .026 .027 .15 7.8 0   .098 - - timeout 900    890    18000   6800 timeout 960   910   18000 5100
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect .048 .048 .13 7.8 0   0     - - out of memory 380    370    4400   7000 timeout 960   800   13000 4800
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect .023 .024 .14 7.9 0   .11  - - out of memory 460    450    8900   7000 timeout 960   840   17000 6300
reducercommutativity/sum_true-unreach-call.i aborted 0 wit inspect .14  .14  1.2  7.9 0   .094 - - error (invalid witness file) .51 .35 7.0 41 error (invalid witness file) 6.1 3.2 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 214 86 87 960 1400 0   250 135 450 340 11000 20000   135 500 340 7900 21000   135 23000 23000 460000 140000   135 74000 64000 1600000 340000  
    correct results 127 214 85 86 960 1300 0   250 5 450 340 11000 20000   38 500 340 7900 21000   3 23000 23000 460000 140000   8 73000 64000 1600000 340000  
        correct true 87 174 31 32 330 840 0   130 0 0 0 0 0   38 0 0 0 0   3 23000 23000 460000 140000   8 73000 64000 1600000 340000  
        correct false 40 40 54 54 630 450 0   120 5 450 340 11000 20000   0 500 340 7900 21000   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) 214
Run set sv-comp17.ReachSafety-Arrays