Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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     900     11000    1100 .84 0   error (invalid witness file) .55 .33 9.8 42 error (invalid witness file) 5.6 3.0 98 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900     900     9000    500 .84 0   error (invalid witness file) .60 .39 6.8 40 error (invalid witness file) 5.9 3.1 120 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900     900     7700    450 .84 0   error (invalid witness file) .52 .35 10   40 error (invalid witness file) 5.8 3.1 100 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900     900     8600    400 .84 0   error (invalid witness file) .48 .32 6.9 39 error (invalid witness file) 6.2 3.3 140 310 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900     900     7600    430 .84 0   error (invalid witness file) .50 .34 6.8 40 error (invalid witness file) 5.7 3.1 120 290 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    5900 .84 0   error (invalid witness file) .50 .32 9.3 41 error (invalid witness file) 7.2 3.7 140 310 - -
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 0 wit inspect 280     280     3300    15000 .84 0   error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.1 3.2 120 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900     900     2100    330 .94 0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.9 3.1 130 290 - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    680 .84 0   error (invalid witness file) .48 .30 8.8 40 error (invalid witness file) 6.0 3.2 130 300 - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    660 .84 0   error (invalid witness file) .50 .32 7.1 39 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8300    830 .84 0   error (invalid witness file) .53 .33 13   40 error (invalid witness file) 5.8 3.1 100 300 - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900     900     9700    730 .84 0   error (invalid witness file) .53 .34 6.2 40 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    750 .98 0   error (invalid witness file) .51 .32 9.3 40 error (invalid witness file) 5.9 3.1 110 300 - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900     900     12000    840 .84 0   error (invalid witness file) .47 .31 6.4 40 error (invalid witness file) 6.5 3.4 110 320 - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8700    820 .84 0   error (invalid witness file) .52 .35 4.6 39 error (invalid witness file) 5.3 2.9 87 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8600    670 .84 0   error (invalid witness file) .49 .32 9.5 41 error (invalid witness file) 6.1 3.2 120 300 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    560 .99 0   error (invalid witness file) .59 .37 7.3 40 error (invalid witness file) 5.7 3.0 110 300 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    660 .84 0   error (invalid witness file) .48 .30 7.4 39 error (invalid witness file) 6.1 3.2 130 290 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900     900     9900    540 .84 0   error (invalid witness file) .51 .35 3.7 40 error (invalid witness file) 5.8 3.1 120 290 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900     900     9300    690 .84 0   error (invalid witness file) .49 .32 7.0 39 error (invalid witness file) 6.4 3.4 120 300 - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900     900     9000    650 .84 0   error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.1 3.2 120 300 - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8200    770 .84 0   error (invalid witness file) .52 .33 8.9 41 error (invalid witness file) 6.2 3.3 93 290 - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900     900     1900    450 .84 0   error (invalid witness file) .49 .33 13   39 error (invalid witness file) 5.4 2.9 92 290 - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900     900     11000    890 .84 0   error (invalid witness file) .49 .32 3.5 41 error (invalid witness file) 6.1 3.2 120 300 - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8900    740 .84 0   error (invalid witness file) .67 .41 7.4 40 error (invalid witness file) 6.4 3.3 130 300 - -
array-examples/standard_minInArray_false-unreach-call_ground.i out of memory 0 wit inspect 660     660     8100    15000 .84 0   error (invalid witness file) .47 .31 6.8 40 error (invalid witness file) 5.9 3.1 120 290 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900     900     8800    630 .84 0   error (invalid witness file) .49 .32 11   43 error (invalid witness file) 5.6 3.0 110 290 - -
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900     900     9500    730 .84 0   error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900     900     8800    1200 .99 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.0 3.1 110 300
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9800    1300 .95 0   - - error (invalid witness file) .66 .42 8.8 41 error (invalid witness file) 6.0 3.2 110 300
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900     900     7700    490 .99 0   - - error (invalid witness file) .49 .33 7.5 40 error (invalid witness file) 5.9 3.1 91 300
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900     900     11000    6400 .99 0   - - error (invalid witness file) .53 .35 13   39 error (invalid witness file) 6.1 3.2 110 300
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    1000 .99 0   - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.1 3.2 130 300
array-examples/sanfoundry_24_true-unreach-call.i true 2 wit inspect .081 .082 .99 23 .84 0   - - error 3.7  2.0  48   270 true 9.2 5.0 110 340
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900     900     12000    14000 .84 0   - - error (invalid witness file) .51 .33 9.9 41 error (invalid witness file) 6.0 3.2 130 310
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect .090 .089 1.0  23 .84 0   - - true 3.8  2.1  77   270 true 6.9 3.7 130 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9700    490 .84 0   - - error (invalid witness file) .53 .34 8.0 44 error (invalid witness file) 6.7 3.5 130 310
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8300    410 .84 0   - - error (invalid witness file) .49 .32 3.5 39 error (invalid witness file) 5.6 3.0 96 310
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    780 .84 0   - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.0 3.2 120 290
array-examples/standard_compare_true-unreach-call_ground.i out of memory 0 wit inspect 350     350     4600    15000 .84 0   - - error (invalid witness file) .58 .37 7.6 40 error (invalid witness file) 5.9 3.1 120 290
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9500    650 .84 0   - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 7.9 4.1 140 340
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    630 .84 0   - - error (invalid witness file) .71 .44 9.0 42 error (invalid witness file) 5.3 2.9 120 290
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    640 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.6 3.0 120 290
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900     900     1600    370 .84 0   - - error (invalid witness file) .57 .37 12   42 error (invalid witness file) 5.7 3.0 100 300
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9000    660 .84 0   - - error (invalid witness file) .48 .31 8.9 39 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9000    640 .84 0   - - error (invalid witness file) .52 .34 11   42 error (invalid witness file) 6.5 3.4 120 320
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9100    680 .84 0   - - error (invalid witness file) .50 .32 7.0 41 error (invalid witness file) 5.8 3.1 120 290
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9800    730 .84 0   - - error (invalid witness file) .48 .31 9.4 39 error (invalid witness file) 7.2 3.8 150 330
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8200    680 .84 0   - - error (invalid witness file) .54 .35 8.1 40 error (invalid witness file) 6.0 3.1 100 290
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900     900     2400    310 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.7 3.0 110 300
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9800    580 .84 0   - - error (invalid witness file) .52 .33 7.5 42 error (invalid witness file) 5.6 2.9 110 290
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8300    500 .84 0   - - error (invalid witness file) .55 .36 9.8 40 error (invalid witness file) 6.4 3.3 130 300
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9800    550 .84 0   - - error (invalid witness file) .54 .35 5.7 40 error (invalid witness file) 6.2 3.3 120 300
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    600 .84 0   - - error (invalid witness file) .53 .36 9.4 42 error (invalid witness file) 6.4 3.3 97 310
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9700    520 .84 0   - - error (invalid witness file) .50 .33 6.5 40 error (invalid witness file) 5.7 3.1 110 300
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9700    560 .84 0   - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.4 3.4 110 310
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8900    620 .84 0   - - error (invalid witness file) .49 .34 3.8 40 error (invalid witness file) 6.7 3.5 130 320
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900     900     1900    410 .84 0   - - error (invalid witness file) .46 .30 8.2 40 error (invalid witness file) 5.7 3.0 100 300
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900     900     11000    790 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.7 3.0 120 290
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8400    790 .84 0   - - error (invalid witness file) .48 .32 8.8 40 error (invalid witness file) 6.0 3.2 100 300
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900     900     12000    750 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.2 2.8 100 290
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    770 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.5 2.9 110 280
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900     900     2300    480 .84 0   - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900     900     1800    5000 .84 0   - - error (invalid witness file) .48 .32 6.3 41 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_minInArray_true-unreach-call_ground.i out of memory 0 wit inspect 720     710     10000    15000 .99 0   - - error (invalid witness file) .58 .36 8.4 41 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8600    510 .84 0   - - error (invalid witness file) .52 .35 12   42 error (invalid witness file) 6.0 3.2 110 290
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900     900     2600    330 .86 0   - - error (invalid witness file) .54 .35 13   43 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900     900     12000    600 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900     900     8500    760 .98 0   - - error (invalid witness file) .50 .33 4.3 41 error (invalid witness file) 5.7 3.1 110 300
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900     890     1700    10000 .84 0   - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.7 3.6 130 310
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    700 .84 0   - - error (invalid witness file) .47 .32 9.9 39 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900     900     10000    730 .99 0   - - error (invalid witness file) .49 .31 9.2 40 error (invalid witness file) 6.3 3.3 120 310
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    6200 .84 0   - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.2 3.3 110 300
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900     900     9700    560 .84 0   - - error (invalid witness file) .64 .41 7.7 40 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900     900     13000    7400 .84 0   - - error (invalid witness file) .50 .33 7.7 41 error (invalid witness file) 5.9 3.1 130 290
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900     900     8600    450 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900     900     13000    490 .84 0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900     900     9600    670 .84 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900     900     11000    830 .84 0   - - error (invalid witness file) .54 .35 13   43 error (invalid witness file) 5.9 3.1 130 290
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900     900     10000    700 .84 0   - - error (invalid witness file) .53 .36 11   41 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900     900     9200    710 .84 0   - - error (invalid witness file) .56 .36 12   43 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900     900     7900    610 .84 0   - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900     900     8700    690 .99 0   - - error (invalid witness file) .47 .32 11   40 error (invalid witness file) 5.7 3.1 100 290
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900     900     9600    610 .84 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.7 3.1 93 300
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900     900     13000    690 .84 0   - - error (invalid witness file) .52 .32 9.8 39 error (invalid witness file) 6.0 3.2 130 300
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900     900     8500    640 .99 0   - - error (invalid witness file) .59 .40 6.4 40 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 350     340     5100    15000 .84 0   - - error (invalid witness file) .51 .32 8.8 40 error (invalid witness file) 6.6 3.5 130 320
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900     900     10000    500 .84 0   - - error (invalid witness file) .47 .31 6.6 39 error (invalid witness file) 5.9 3.1 100 300
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i timeout 0 wit inspect 900     900     2100    700 .84 0   error (invalid witness file) .50 .33 10   40 error (invalid witness file) 6.0 3.2 110 300 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900     900     8500    1400 .84 0   error (invalid witness file) .65 .42 7.9 40 error (invalid witness file) 5.5 3.0 91 290 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900     900     10000    550 .84 0   error (invalid witness file) .53 .34 13   41 error (invalid witness file) 5.6 3.0 110 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900     900     9600    490 .84 0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.2 3.7 120 300 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900     900     13000    540 .84 0   error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.0 3.2 110 300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900     900     7600    940 .84 0   error (invalid witness file) .51 .32 9.2 40 error (invalid witness file) 6.1 3.2 110 290 - -
array-industry-pattern/array_monotonic_true-unreach-call.i timeout 0 wit inspect 900     900     9200    600 .84 0   - - error (invalid witness file) .53 .33 12   41 error (invalid witness file) 6.7 3.5 140 320
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 900     900     8600    730 .84 0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.1 3.2 110 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900     900     9600    740 .84 0   - - error (invalid witness file) .53 .35 8.0 41 error (invalid witness file) 6.4 3.4 110 290
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i true 2 wit inspect .32  .32  .64 23 .84 0   - - timeout 900    890    12000   3100 timeout 960   940   12000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i out of memory 0 wit inspect 810     810     9400    15000 .84 0   - - error (invalid witness file) .47 .30 7.9 39 error (invalid witness file) 5.9 3.1 120 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i true 2 wit inspect .32  .32  .81 23 .84 0   - - timeout 900    890    11000   3600 timeout 960   940   20000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900     900     8900    840 .84 0   - - error (invalid witness file) .58 .37 11   39 error (invalid witness file) 6.5 3.5 77 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900     900     8500    900 .84 0   - - error (invalid witness file) .53 .36 9.4 41 error (invalid witness file) 5.4 2.9 110 290
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900     900     10000    1000 .84 0   - - error (invalid witness file) .52 .33 8.5 44 error (invalid witness file) 5.9 3.2 130 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900     900     8800    1400 .93 0   - - error (invalid witness file) .49 .32 7.6 39 error (invalid witness file) 5.7 3.0 130 300
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900     900     9200    880 .84 0   - - error (invalid witness file) .50 .33 7.7 39 error (invalid witness file) 5.9 3.1 110 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 2.0   2.0   23    120 .84 0   false(unreach-call) 7.8  4.9  86   370 true 9.5 5.1 130 350 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 12     12     150    250 .84 0   false(unreach-call) 7.1  4.5  160   390 true 11   6.2 140 360 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 120     120     1200    600 .84 0   false(unreach-call) 8.9  5.8  96   450 true 11   5.6 110 420 - -
reducercommutativity/rangesum40_false-unreach-call.i timeout 0 wit inspect 900     900     9000    1100 .84 0   error (invalid witness file) .51 .34 8.7 39 error (invalid witness file) 6.1 3.2 120 300 - -
reducercommutativity/rangesum60_false-unreach-call.i timeout 0 wit inspect 900     900     2200    820 .99 0   error (invalid witness file) .57 .35 9.8 44 error (invalid witness file) 6.1 3.2 130 300 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 1.5   1.5   16    160 .84 0   false(unreach-call) 5.9  3.6  100   380 true 9.7 5.4 150 360 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect 1.9   1.9   21    95 .84 0   - - timeout 900    900    8700   1800 true 160   140   3000 1000
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect 16     16     180    190 .84 0   - - timeout 900    890    13000   3500 true 350   310   5700 1400
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900     900     2400    490 .84 0   - - error (invalid witness file) .58 .39 8.7 40 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900     900     8500    660 .84 0   - - error (invalid witness file) .63 .40 7.7 39 error (invalid witness file) 6.0 3.2 120 300
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900     900     11000    660 .84 0   - - error (invalid witness file) .50 .33 10   43 error (invalid witness file) 6.2 3.3 120 300
reducercommutativity/avg_true-unreach-call.i timeout 0 wit inspect 900     900     9500    300 .84 0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.5 3.0 93 300
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 5.4   5.4   72    34 .84 0   - - true 93    83    1300   840 timeout 960   910   16000 1400
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 240     240     3000    90 .84 0   - - timeout 900    890    12000   2000 timeout 960   890   15000 2400
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900     900     13000    330 .84 0   - - error (invalid witness file) .63 .40 9.5 40 error (invalid witness file) 5.7 3.1 79 280
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900     900     8800    580 .84 0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.2 3.3 110 310
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900     900     11000    630 .84 0   - - error (invalid witness file) .66 .42 8.3 40 error (invalid witness file) 5.6 3.0 100 300
reducercommutativity/max_true-unreach-call.i timeout 0 wit inspect 900     900     1800    110 .84 0   - - error (invalid witness file) .62 .39 9.2 44 error (invalid witness file) 6.2 3.3 89 300
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect .80  .79  10    36 .84 0   - - true 160    150    1600   990 true 210   150   2200 2600
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 11     11     140    100 .84 0   - - timeout 900    890    9800   1300 out of memory 740   630   8700 7000
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 900     900     13000    370 .84 0   - - error (invalid witness file) .50 .31 9.4 39 error (invalid witness file) 6.5 3.5 130 320
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900     900     2600    520 .99 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.3 3.3 140 300
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900     900     11000    880 .84 0   - - error (invalid witness file) .59 .36 8.7 45 error (invalid witness file) 6.1 3.2 110 300
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 900     900     12000    390 .84 0   - - error (invalid witness file) .51 .33 10   43 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 1.4   1.4   2.7  31 .84 0   - - timeout 900    900    12000   1000 true 36   22   610 740
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect 4.0   3.9   51    74 .84 0   - - timeout 900    890    12000   2300 true 89   59   930 1200
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect 240     240     2200    310 .84 0   - - timeout 900    890    8900   6700 timeout 960   910   8100 5100
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900     900     8100    490 .84 0   - - error (invalid witness file) .56 .36 7.7 41 error (invalid witness file) 6.2 3.3 120 310
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900     900     6800    500 .99 0   - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.1 3.2 120 310
reducercommutativity/sum_true-unreach-call.i timeout 0 wit inspect 900     900     11000    200 .84 0   - - error (invalid witness file) .65 .41 8.7 40 error (invalid witness file) 6.9 3.7 95 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 135 30 100000 100000 1000000 220000 120   0   135 48 31 770 3000   135 260 140 4700 12000   135 8400 8300 100000 31000   135 6900 6200 100000 58000  
    correct results 17 30 660 660 7000 2200 14   0   4 30 19 450 1600   4 41 22 540 1500   3 8400 8300 100000 28000   7 6400 5900 93000 34000  
        correct true 13 26 520 520 5700 1100 11   0   0 0 0 0 0   4 0 0 0 0   3 8400 8300 100000 28000   7 6400 5900 93000 34000  
        correct false 4 4 140 140 1400 1100 3.4 0   4 30 19 450 1600   0 41 22 540 1500   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (135 tasks, max score: 230) 30
Run set sv-comp17.ReachSafety-Arrays