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-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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    12000   230 .84 0   error (invalid witness file) .56 .37 7.7 39 error (invalid witness file) 6.9 3.6 140 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900    890    11000   970 .84 0   error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.3 3.4 130 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900    890    10000   970 .84 0   error (invalid witness file) .61 .39 8.6 39 error (invalid witness file) 5.6 3.0 46 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900    890    11000   530 .84 0   error (invalid witness file) .51 .33 9.2 40 error (invalid witness file) 6.4 3.4 99 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   530 .84 0   error (invalid witness file) .50 .33 8.8 41 error (invalid witness file) 5.5 2.9 72 300 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900    900    11000   4500 .84 0   error (invalid witness file) .51 .34 14   40 error (invalid witness file) 5.9 3.1 110 300 - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900    800    1600   1300 .84 0   error (invalid witness file) .51 .34 10   41 error (invalid witness file) 7.3 3.8 82 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900    810    12000   5300 .84 0   error (invalid witness file) .49 .32 8.6 39 error (invalid witness file) 5.8 3.1 83 300 - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5200 .84 0   error (invalid witness file) .54 .35 11   41 error (invalid witness file) 6.7 3.6 63 300 - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900    800    12000   5300 .84 0   error (invalid witness file) .53 .33 8.8 40 error (invalid witness file) 6.0 3.2 49 290 - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900    810    11000   5300 .84 0   error (invalid witness file) .49 .31 10   40 error (invalid witness file) 5.5 3.0 93 300 - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900    810    12000   5300 .84 0   error (invalid witness file) .52 .34 10   40 error (invalid witness file) 4.8 2.7 49 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900    810    14000   5300 .84 0   error (invalid witness file) .56 .37 5.8 40 error (invalid witness file) 6.7 3.5 120 310 - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900    800    13000   5300 .84 0   error (invalid witness file) .64 .40 7.3 41 error (invalid witness file) 6.3 3.3 100 300 - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900    810    12000   5300 .84 0   error (invalid witness file) .67 .43 4.8 43 error (invalid witness file) 5.9 3.1 83 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900    800    12000   5900 .84 0   error (invalid witness file) .68 .44 7.2 41 error (invalid witness file) 8.0 4.2 75 300 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .84 0   error (invalid witness file) .51 .33 8.8 41 error (invalid witness file) 5.9 3.1 95 300 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5900 .84 0   error (invalid witness file) .76 .48 8.6 43 error (invalid witness file) 6.0 3.2 98 290 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900    790    12000   5900 .84 0   error (invalid witness file) .54 .35 9.1 39 error (invalid witness file) 7.5 3.9 120 330 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .84 0   error (invalid witness file) .47 .31 4.5 39 error (invalid witness file) 5.1 2.8 84 300 - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900    790    12000   5900 .84 0   error (invalid witness file) .50 .32 9.2 40 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .84 0   error (invalid witness file) .63 .40 6.6 39 error (invalid witness file) 6.6 3.5 110 300 - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900    790    12000   5900 .84 0   error (invalid witness file) .49 .31 11   39 error (invalid witness file) 5.7 3.1 83 300 - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900    790    14000   6000 .84 0   error (invalid witness file) .65 .41 5.5 40 error (invalid witness file) 6.3 3.3 120 300 - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5900 .84 0   error (invalid witness file) .57 .37 8.7 43 error (invalid witness file) 5.7 3.0 90 290 - -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900    890    9500   530 .84 0   error (invalid witness file) .67 .42 8.8 40 error (invalid witness file) 6.1 3.3 120 310 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   1100 .84 0   error (invalid witness file) .53 .34 9.9 42 error (invalid witness file) 6.4 3.4 91 290 - -
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 470    450    6200   15000 .84 0   error (invalid witness file) .69 .43 8.0 41 error (invalid witness file) 6.6 3.5 100 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900    870    13000   11000 .84 0   - - error (invalid witness file) .55 .35 13   42 error (invalid witness file) 5.4 2.9 100 290
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900    900    12000   230 .84 0   - - error (invalid witness file) .50 .32 12   41 error (invalid witness file) 6.9 3.6 140 320
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900    900    7200   540 .84 0   - - error (invalid witness file) .54 .36 7.1 43 error (invalid witness file) 5.9 3.1 110 300
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   740 .84 0   - - error (invalid witness file) .50 .33 8.2 40 error (invalid witness file) 7.1 3.7 91 300
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900    900    8600   10000 .84 0   - - error (invalid witness file) .64 .41 7.0 40 error (invalid witness file) 5.9 3.2 120 300
array-examples/sanfoundry_24_true-unreach-call.i out of memory 0 wit inspect 900    890    12000   15000 .84 0   - - error (invalid witness file) .51 .34 9.3 40 error (invalid witness file) 5.7 3.1 110 300
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900    890    10000   530 .84 0   - - error (invalid witness file) .49 .33 9.3 44 error (invalid witness file) 5.6 3.0 110 300
array-examples/sanfoundry_43_true-unreach-call_ground.i timeout 0 wit inspect 900    840    11000   4300 .84 0   - - error (invalid witness file) .59 .38 9.2 43 error (invalid witness file) 5.9 3.1 120 290
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900    890    10000   970 .84 0   - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 5.9 3.1 110 310
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   530 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.7 3.0 110 300
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   490 .84 0   - - error (invalid witness file) .58 .37 6.2 40 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900    890    9900   530 .84 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 5.5 3.0 96 290
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900    800    12000   5200 .84 0   - - error (invalid witness file) .49 .31 9.1 39 error (invalid witness file) 6.2 3.3 130 300
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5200 .84 0   - - error (invalid witness file) .68 .42 7.7 41 error (invalid witness file) 6.0 3.2 97 300
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900    800    12000   5200 .84 0   - - error (invalid witness file) .51 .33 7.8 42 error (invalid witness file) 6.9 3.6 120 310
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5300 .84 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.4 3.3 100 300
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900    810    12000   5300 .99 0   - - error (invalid witness file) .56 .36 11   43 error (invalid witness file) 5.9 3.2 110 300
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900    800    13000   5300 .84 0   - - error (invalid witness file) .71 .44 6.8 42 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5300 .84 0   - - error (invalid witness file) .50 .31 9.1 39 error (invalid witness file) 6.3 3.3 120 310
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900    800    13000   5200 .84 0   - - error (invalid witness file) .55 .36 12   44 error (invalid witness file) 6.1 3.2 130 300
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900    810    12000   5300 .84 0   - - error (invalid witness file) .52 .33 10   44 error (invalid witness file) 5.5 3.0 91 290
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5900 .84 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.9 3.1 110 290
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900    790    9400   4800 .84 0   - - error (invalid witness file) .51 .32 8.9 40 error (invalid witness file) 5.5 3.0 89 290
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900    800    11000   5800 .84 0   - - error (invalid witness file) .47 .31 7.2 40 error (invalid witness file) 5.8 3.1 120 300
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5900 .84 0   - - error (invalid witness file) .56 .36 9.8 39 error (invalid witness file) 5.5 3.0 91 280
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900    820    10000   9400 .84 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900    790    13000   5800 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.6 3.0 110 300
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .99 0   - - error (invalid witness file) .58 .37 15   43 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900    790    12000   5800 .84 0   - - error (invalid witness file) .60 .39 9.9 39 error (invalid witness file) 5.0 2.8 110 290
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .84 0   - - error (invalid witness file) .52 .33 9.5 42 error (invalid witness file) 6.0 3.2 100 300
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900    790    12000   5700 .84 0   - - error (invalid witness file) .55 .36 8.2 40 error (invalid witness file) 6.4 3.4 110 310
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5800 .84 0   - - error (invalid witness file) .47 .31 9.3 40 error (invalid witness file) 5.8 3.1 130 300
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900    790    11000   5700 .84 0   - - error (invalid witness file) .53 .35 9.8 41 error (invalid witness file) 5.9 3.1 110 290
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900    790    13000   5800 .84 0   - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900    800    12000   5800 .84 0   - - error (invalid witness file) .50 .32 9.4 39 error (invalid witness file) 5.8 3.1 72 310
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900    890    10000   530 .84 0   - - error (invalid witness file) .49 .33 4.9 40 error (invalid witness file) 5.9 3.2 120 300
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900    890    11000   540 .84 0   - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900    820    11000   4400 .84 0   - - error (invalid witness file) .49 .31 8.1 39 error (invalid witness file) 6.1 3.2 120 300
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900    890    9600   1100 .84 0   - - error (invalid witness file) .46 .30 6.3 39 error (invalid witness file) 5.9 3.2 130 300
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 0 wit inspect 500    470    6500   15000 .84 0   - - error (invalid witness file) .60 .40 9.0 40 error (invalid witness file) 5.8 3.1 110 290
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900    890    9900   1100 .84 0   - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 5.3 2.9 110 280
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900    890    9300   540 .84 0   - - error (invalid witness file) .51 .34 12   39 error (invalid witness file) 5.7 3.0 83 300
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900    820    13000   4600 .84 0   - - error (invalid witness file) .50 .31 12   40 error (invalid witness file) 5.8 3.1 120 300
array-examples/standard_running_true-unreach-call.i out of memory 0 wit inspect 460    450    6200   15000 .84 0   - - error (invalid witness file) .49 .33 6.2 40 error (invalid witness file) 6.0 3.2 100 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    12000   2400 .84 0   - - error (invalid witness file) .47 .31 6.6 39 error (invalid witness file) 5.8 3.1 110 310
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900    820    15000   4300 .84 0   - - error (invalid witness file) .65 .42 7.9 40 error (invalid witness file) 5.4 2.9 77 290
array-examples/standard_strcmp_true-unreach-call_ground.i out of memory 0 wit inspect 710    700    11000   15000 .84 0   - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 5.7 3.1 96 300
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900    810    10000   9700 .84 0   - - error (invalid witness file) .63 .40 8.8 39 error (invalid witness file) 5.6 3.0 100 290
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900    820    9600   9600 .84 0   - - error (invalid witness file) .51 .33 4.7 40 error (invalid witness file) 5.9 3.2 100 310
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900    820    11000   4200 .84 0   - - error (invalid witness file) .64 .41 7.6 39 error (invalid witness file) 6.0 3.2 130 290
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900    810    2300   1000 .84 0   - - error (invalid witness file) .48 .32 8.7 39 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_two_index_03_true-unreach-call.i out of memory 0 wit inspect 490    480    6500   15000 .84 0   - - error (invalid witness file) .60 .37 5.1 44 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900    820    11000   4200 .84 0   - - error (invalid witness file) .52 .34 9.7 41 error (invalid witness file) 6.1 3.2 120 310
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900    820    12000   4200 .84 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.7 3.1 120 300
array-examples/standard_two_index_06_true-unreach-call.i out of memory 0 wit inspect 480    470    6200   15000 .84 0   - - error (invalid witness file) .52 .35 4.1 40 error (invalid witness file) 5.9 3.1 93 310
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900    820    15000   4200 .84 0   - - error (invalid witness file) .49 .32 6.2 40 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900    820    11000   4200 .85 0   - - error (invalid witness file) .51 .32 7.4 40 error (invalid witness file) 5.2 2.8 81 290
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900    820    12000   4200 .84 0   - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 6.6 3.5 100 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 860    860    12000   15000 .84 0   - - error (invalid witness file) .55 .35 13   42 error (invalid witness file) 5.9 3.2 100 310
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900    820    11000   4400 .84 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.0 3.2 98 300
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i timeout 0 wit inspect 900    790    11000   6000 .84 0   error (invalid witness file) .50 .32 8.1 40 error (invalid witness file) 6.5 3.4 130 320 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900    800    11000   5300 .84 0   error (invalid witness file) .55 .35 11   42 error (invalid witness file) 5.8 3.1 90 290 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900    900    11000   1500 .84 0   error (invalid witness file) .62 .39 7.1 40 error (invalid witness file) 7.1 3.7 93 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900    830    12000   3700 .84 0   error (invalid witness file) .61 .39 7.8 39 error (invalid witness file) 6.4 3.4 87 310 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900    900    10000   1500 .84 0   error (invalid witness file) .51 .33 9.1 40 error (invalid witness file) 5.7 3.1 110 300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900    900    12000   230 .84 0   error (invalid witness file) .50 .32 6.3 40 error (invalid witness file) 6.2 3.3 75 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i timeout 0 wit inspect 900    890    9300   1000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 120 300
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 900    820    13000   3900 .84 0   - - error (invalid witness file) .47 .30 7.7 39 error (invalid witness file) 5.8 3.1 120 290
array-industry-pattern/array_of_struct_break_true-unreach-call.i out of memory 0 wit inspect 880    880    12000   15000 .84 0   - - error (invalid witness file) .51 .33 7.4 39 error (invalid witness file) 5.8 3.1 100 290
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900    890    9900   5200 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.9 3.1 110 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900    870    8000   3900 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 130 300
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900    900    9700   2100 .84 0   - - error (invalid witness file) .57 .36 9.0 43 error (invalid witness file) 7.6 4.0 130 340
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900    860    11000   2400 .84 0   - - error (invalid witness file) .49 .32 9.7 39 error (invalid witness file) 6.1 3.2 110 310
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900    880    11000   1400 .84 0   - - error (invalid witness file) .48 .31 6.8 40 error (invalid witness file) 7.0 3.6 130 310
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900    780    11000   6300 .84 0   - - error (invalid witness file) .52 .34 6.2 40 error (invalid witness file) 6.1 3.2 120 300
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900    900    9000   2400 .84 0   - - error (invalid witness file) .56 .35 13   42 error (invalid witness file) 5.7 3.0 120 290
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900    900    11000   430 .84 0   - - error (invalid witness file) .54 .33 12   41 error (invalid witness file) 6.2 3.3 120 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect .24 .24 2.9 37 .84 0   false(unreach-call) 6.3  3.9  100   380 true 12   6.2 130 340 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect .29 .29 3.3 38 .84 0   false(unreach-call) 7.1  4.5  150   390 true 11   6.1 150 350 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 1.0  1.0  13   40 .84 0   false(unreach-call) 9.6  6.3  130   450 true 11   5.8 170 420 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 2.7  2.7  30   45 .93 0   false(unreach-call) 12    7.9  190   630 true 13   6.9 220 540 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 2.6  2.6  30   48 .84 0   false(unreach-call) 18    13    290   710 true 15   7.9 230 540 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect .65 .65 6.9 92 .84 0   false(unreach-call) 5.8  3.6  140   370 true 11   6.0 160 360 - -
reducercommutativity/avg05_true-unreach-call.i out of memory 0 wit inspect 160    160    2100   15000 .84 0   - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 5.6 3.0 92 300
reducercommutativity/avg10_true-unreach-call.i out of memory 0 wit inspect 220    210    3300   15000 .84 0   - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.2 3.3 110 300
reducercommutativity/avg20_true-unreach-call.i out of memory 0 wit inspect 280    250    3800   15000 .84 0   - - error (invalid witness file) .48 .31 8.4 40 error (invalid witness file) 5.3 2.9 96 290
reducercommutativity/avg40_true-unreach-call.i out of memory 0 wit inspect 340    310    3800   15000 .84 0   - - error (invalid witness file) .51 .32 7.6 40 error (invalid witness file) 5.6 3.1 120 300
reducercommutativity/avg60_true-unreach-call.i out of memory 0 wit inspect 410    380    5300   15000 .84 0   - - error (invalid witness file) .49 .32 4.0 43 error (invalid witness file) 6.0 3.2 100 290
reducercommutativity/avg_true-unreach-call.i timeout 0 wit inspect 900    900    13000   170 .84 0   - - error (invalid witness file) .49 .31 12   40 error (invalid witness file) 5.7 3.0 110 290
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    12000   1000 .94 0   - - error (invalid witness file) .49 .32 10   42 error (invalid witness file) 5.6 3.0 98 290
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    10000   120 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.6 3.0 110 290
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900    900    12000   140 .84 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 5.6 3.0 100 290
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900    900    9400   170 .84 0   - - error (invalid witness file) .73 .45 8.2 44 error (invalid witness file) 6.1 3.2 110 300
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900    900    10000   200 .84 0   - - error (invalid witness file) .53 .34 12   43 error (invalid witness file) 5.4 2.9 110 280
reducercommutativity/max_true-unreach-call.i timeout 0 wit inspect 900    900    13000   120 .84 0   - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.9 3.6 100 300
reducercommutativity/sep05_true-unreach-call.i timeout 0 wit inspect 900    900    13000   8000 .84 0   - - error (invalid witness file) .56 .36 11   41 error (invalid witness file) 6.5 3.4 130 310
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900    900    13000   1400 .84 0   - - error (invalid witness file) .54 .35 14   40 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 900    900    10000   64 .84 0   - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 5.8 3.1 110 300
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900    900    10000   92 .84 0   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.9 3.1 120 300
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900    900    9400   130 .84 0   - - error (invalid witness file) .52 .34 14   41 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 900    900    10000   170 .84 0   - - error (invalid witness file) .46 .32 4.1 40 error (invalid witness file) 6.0 3.2 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i out of memory 0 wit inspect 180    170    2700   15000 .84 0   - - error (invalid witness file) .60 .39 7.0 39 error (invalid witness file) 6.1 3.2 120 300
reducercommutativity/sum10_true-unreach-call.i timeout 0 wit inspect 900    810    2300   13000 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.9 3.2 120 290
reducercommutativity/sum20_true-unreach-call.i out of memory 0 wit inspect 280    260    3600   15000 .84 0   - - error (invalid witness file) .48 .31 13   40 error (invalid witness file) 5.9 3.1 110 300
reducercommutativity/sum40_true-unreach-call.i out of memory 0 wit inspect 340    310    4300   15000 .84 0   - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 5.8 3.1 110 300
reducercommutativity/sum60_true-unreach-call.i out of memory 0 wit inspect 410    380    4700   15000 .84 0   - - error (invalid witness file) .47 .32 8.6 39 error (invalid witness file) 6.8 3.6 120 310
reducercommutativity/sum_true-unreach-call.i timeout 0 wit inspect 900    900    11000   190 .84 0   - - error (invalid witness file) .49 .32 7.5 41 error (invalid witness file) 6.3 3.3 120 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 6 110000   100000   1300000 680000 110   0   135 78 51 1300 4300 135 280 150 4300 13000 135 50 32 910 3800   135 560 300 10000 28000  
    correct results 6 6 7.5 7.5 86 300 5.1 0   6 59 39 1000 2900 6 73 39 1100 2600 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 6 6 7.5 7.5 86 300 5.1 0   6 59 39 1000 2900 0 73 39 1100 2600 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