Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-16 17:45:19 CET [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.ArraysReach
Options [[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i timeout 910     240     12000 wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 87     86     15000 wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 88     87     15000 wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 51     50     15000 wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 51     50     15000 wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 45     45     15000 wit - -
array-examples/standard_copy1_false-unreach-call_ground.i false(reach) 95     63     4000 wit true 13 7.9 330 -
array-examples/standard_copy2_false-unreach-call_ground.i false(reach) 100     63     4100 wit true 11 6.3 340 -
array-examples/standard_copy3_false-unreach-call_ground.i false(reach) 110     64     4200 wit true 14 8.9 340 -
array-examples/standard_copy4_false-unreach-call_ground.i false(reach) 120     74     4200 wit true 13 6.9 330 -
array-examples/standard_copy5_false-unreach-call_ground.i false(reach) 130     75     4200 wit true 15 11   340 -
array-examples/standard_copy6_false-unreach-call_ground.i false(reach) 140     75     4200 wit true 13 7.3 370 -
array-examples/standard_copy7_false-unreach-call_ground.i false(reach) 150     76     4300 wit true 16 9.7 390 -
array-examples/standard_copy8_false-unreach-call_ground.i false(reach) 150     76     4400 wit true 15 9.9 340 -
array-examples/standard_copy9_false-unreach-call_ground.i false(reach) 160     87     4400 wit true 16 10   350 -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(reach) 110     72     3000 wit true 14 7.9 340 -
array-examples/standard_init1_false-unreach-call_ground.i false(reach) 90     61     1600 wit true 12 7.0 340 -
array-examples/standard_init2_false-unreach-call_ground.i false(reach) 100     71     1900 wit true 13 7.5 330 -
array-examples/standard_init3_false-unreach-call_ground.i false(reach) 110     72     3000 wit true 13 9.3 330 -
array-examples/standard_init4_false-unreach-call_ground.i false(reach) 120     72     3100 wit true 14 7.9 350 -
array-examples/standard_init5_false-unreach-call_ground.i false(reach) 120     73     3100 wit true 15 8.6 350 -
array-examples/standard_init6_false-unreach-call_ground.i false(reach) 140     73     4000 wit true 14 8.5 370 -
array-examples/standard_init7_false-unreach-call_ground.i false(reach) 150     84     4000 wit true 12 6.6 400 -
array-examples/standard_init8_false-unreach-call_ground.i false(reach) 150     84     4000 wit true 15 8.4 420 -
array-examples/standard_init9_false-unreach-call_ground.i false(reach) 150     84     3900 wit true 13 7.1 430 -
array-examples/standard_minInArray_false-unreach-call_ground.i false(reach) 97     62     4000 wit true 11 6.0 330 -
array-examples/standard_partition_false-unreach-call_ground.i false(reach) 140     84     4200 wit true 14 7.5 330 -
array-examples/standard_running_false-unreach-call.i false(reach) 97     64     3900 wit true 14 8.0 350 -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i true 31     31     2800 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 900     900     13000 wit - -
array-examples/relax_true-unreach-call.i unknown 890     900     260 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 890     900     460 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i true 610     610     360 wit - -
array-examples/sanfoundry_24_true-unreach-call.i true .32  .34  51 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 890     900     310 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true .15  .16  13 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 88     88     15000 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 51     50     15000 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i true .46  .47  65 wit - -
array-examples/standard_compare_true-unreach-call_ground.i true .30  .31  36 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i true .19  .21  16 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i true .19  .20  18 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i true .23  .24  19 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i true .28  .29  21 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i true .32  .34  22 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i true .38  .40  23 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i true .39  .40  25 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i true .43  .44  26 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i true .49  .51  27 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true .27  .28  19 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true .32  .33  21 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i true .27  .28  19 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i true .19  .20  18 wit - -
array-examples/standard_find_true-unreach-call_ground.i true .77  .78  67 wit - -
array-examples/standard_init1_true-unreach-call_ground.i true .15  .15  16 wit - -
array-examples/standard_init2_true-unreach-call_ground.i true .17  .18  17 wit - -
array-examples/standard_init3_true-unreach-call_ground.i true .17  .18  19 wit - -
array-examples/standard_init4_true-unreach-call_ground.i true .18  .19  20 wit - -
array-examples/standard_init5_true-unreach-call_ground.i true .23  .24  21 wit - -
array-examples/standard_init6_true-unreach-call_ground.i true .26  .27  22 wit - -
array-examples/standard_init7_true-unreach-call_ground.i true .27  .28  24 wit - -
array-examples/standard_init8_true-unreach-call_ground.i true .29  .31  25 wit - -
array-examples/standard_init9_true-unreach-call_ground.i true .25  .26  26 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i unknown 890     900     280 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i unknown 890     900     250 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i true .26  .27  17 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i unknown 890     900     420 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i unknown 890     900     860 wit - -
array-examples/standard_partition_true-unreach-call_ground.i unknown 890     900     560 wit - -
array-examples/standard_password_true-unreach-call_ground.i true .30  .31  36 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i false(reach) 93     63     4000 wit - -
array-examples/standard_running_true-unreach-call.i unknown 890     900     320 wit - -
array-examples/standard_sentinel_true-unreach-call.i true 1.7   1.8   17 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i true .19  .20  17 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i true .33  .34  21 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i true 180     180     48 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i true 180     180     50 wit - -
array-examples/standard_two_index_01_true-unreach-call.i true .16  .17  18 wit - -
array-examples/standard_two_index_02_true-unreach-call.i true .19  .20  18 wit - -
array-examples/standard_two_index_03_true-unreach-call.i true .17  .17  18 wit - -
array-examples/standard_two_index_04_true-unreach-call.i true .20  .22  18 wit - -
array-examples/standard_two_index_05_true-unreach-call.i true .20  .21  18 wit - -
array-examples/standard_two_index_06_true-unreach-call.i true .18  .20  18 wit - -
array-examples/standard_two_index_07_true-unreach-call.i true .22  .23  18 wit - -
array-examples/standard_two_index_08_true-unreach-call.i true .18  .19  18 wit - -
array-examples/standard_two_index_09_true-unreach-call.i true .17  .18  18 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i true .26  .27  28 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i true .18  .20  17 wit - -
reducercommutativity/rangesum05_false-unreach-call.i error (1) 120     60     4300 wit - -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 49     30     3100 wit true 12 8.5 320 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 820     530     7800 wit true 11 6.6 340 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 820     470     7100 wit true 14 8.0 330 -
reducercommutativity/rangesum60_false-unreach-call.i timeout 910     450     8400 wit - -
reducercommutativity/rangesum_false-unreach-call.i error (1) 150     110     3200 wit - -
reducercommutativity/avg05_true-unreach-call.i unknown 890     900     150 wit - -
reducercommutativity/avg10_true-unreach-call.i unknown 890     900     190 wit - -
reducercommutativity/avg20_true-unreach-call.i unknown 890     900     250 wit - -
reducercommutativity/avg40_true-unreach-call.i unknown 890     900     310 wit - -
reducercommutativity/avg60_true-unreach-call.i unknown 890     900     290 wit - -
reducercommutativity/avg_true-unreach-call.i unknown 890     900     320 wit - -
reducercommutativity/max05_true-unreach-call.i true 1.7   1.7   16 wit - -
reducercommutativity/max10_true-unreach-call.i true 55     55     40 wit - -
reducercommutativity/max20_true-unreach-call.i unknown 890     900     110 wit - -
reducercommutativity/max40_true-unreach-call.i unknown 890     900     170 wit - -
reducercommutativity/max60_true-unreach-call.i unknown 890     900     240 wit - -
reducercommutativity/max_true-unreach-call.i unknown 890     900     180 wit - -
reducercommutativity/sep05_true-unreach-call.i true .20  .21  13 wit - -
reducercommutativity/sep10_true-unreach-call.i true .25  .26  13 wit - -
reducercommutativity/sep20_true-unreach-call.i true .37  .38  13 wit - -
reducercommutativity/sep40_true-unreach-call.i true .57  .58  13 wit - -
reducercommutativity/sep60_true-unreach-call.i true .79  .80  13 wit - -
reducercommutativity/sep_true-unreach-call.i error (1) 460     410     4000 wit - -
reducercommutativity/sum05_true-unreach-call.i true .076 .084 13 wit - -
reducercommutativity/sum10_true-unreach-call.i true .092 .10  13 wit - -
reducercommutativity/sum20_true-unreach-call.i true .096 .10  13 wit - -
reducercommutativity/sum40_true-unreach-call.i true .14  .15  13 wit - -
reducercommutativity/sum60_true-unreach-call.i true .17  .18  13 wit - -
reducercommutativity/sum_true-unreach-call.i unknown 890     900     200 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
total tasks 118 27000 24000 260000 118 340   200   8800   118 0  
    correct results 84 5500 3700 100000 25 340   200   8800   0 0  
        correct true 59 1100 1100 4500 25 0   0   0   0 0  
        correct false 25 4400 2600 100000 0 340   200   8800   0 0  
    incorrect results 1 93 63 4000 0 0   0   0   0 0  
        incorrect true 0
        incorrect false 1 93 63 4000 0 0   0   0   0 0  
score (118 tasks, max score: 202) 127
Run set sv-comp16.ArraysReach