Tool DepthK ESBMC+DepthK version 2.1
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-22-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-05 14:06:34 CET [[ 2016-01-15 22:17:52 CET ]]
Run set sv-comp16.ArraysReach
Options [[ ../../results-verified/esbmcdepthk.2016-01-05_1406.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 unknown 890    900    380 wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 890    900    350 wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 890    900    450 wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 890    900    850 wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 890    900    850 wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 890    900    4200 wit - -
array-examples/standard_copy1_false-unreach-call_ground.i unknown 220    220    76 wit - -
array-examples/standard_copy2_false-unreach-call_ground.i unknown 680    680    130 wit - -
array-examples/standard_copy3_false-unreach-call_ground.i unknown 890    900    180 wit - -
array-examples/standard_copy4_false-unreach-call_ground.i unknown 890    900    210 wit - -
array-examples/standard_copy5_false-unreach-call_ground.i unknown 890    900    240 wit - -
array-examples/standard_copy6_false-unreach-call_ground.i unknown 890    900    260 wit - -
array-examples/standard_copy7_false-unreach-call_ground.i unknown 890    900    290 wit - -
array-examples/standard_copy8_false-unreach-call_ground.i unknown 890    900    310 wit - -
array-examples/standard_copy9_false-unreach-call_ground.i unknown 890    900    330 wit - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unknown 690    690    180 wit - -
array-examples/standard_init1_false-unreach-call_ground.i unknown 200    200    75 wit - -
array-examples/standard_init2_false-unreach-call_ground.i unknown 510    520    130 wit - -
array-examples/standard_init3_false-unreach-call_ground.i unknown 890    900    180 wit - -
array-examples/standard_init4_false-unreach-call_ground.i unknown 890    900    190 wit - -
array-examples/standard_init5_false-unreach-call_ground.i unknown 890    900    210 wit - -
array-examples/standard_init6_false-unreach-call_ground.i unknown 890    900    220 wit - -
array-examples/standard_init7_false-unreach-call_ground.i unknown 890    900    230 wit - -
array-examples/standard_init8_false-unreach-call_ground.i unknown 890    900    240 wit - -
array-examples/standard_init9_false-unreach-call_ground.i unknown 890    900    250 wit - -
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 51    52    53 wit - -
array-examples/standard_partition_false-unreach-call_ground.i unknown 890    900    190 wit - -
array-examples/standard_running_false-unreach-call.i unknown 890    900    69 wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i true .42 .46 22 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i true .79 .82 36 wit - -
array-examples/relax_true-unreach-call.i true 10    10    63 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i true .92 .95 23 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i true .74 .78 36 wit - -
array-examples/sanfoundry_24_true-unreach-call.i true .38 .41 22 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i true .50 .53 22 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true .39 .42 21 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 890    900    460 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 890    900    840 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i true .39 .42 22 wit - -
array-examples/standard_compare_true-unreach-call_ground.i true .40 .43 22 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i true .38 .40 21 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i true .46 .49 21 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i true .40 .43 21 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i true .42 .44 22 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i true .48 .51 22 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i true .42 .45 22 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i true .49 .52 22 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i true .40 .42 22 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i true .42 .44 22 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true .44 .46 22 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true .43 .46 22 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i true .41 .44 22 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i true .41 .44 21 wit - -
array-examples/standard_find_true-unreach-call_ground.i true .48 .51 23 wit - -
array-examples/standard_init1_true-unreach-call_ground.i true .37 .40 21 wit - -
array-examples/standard_init2_true-unreach-call_ground.i true .39 .42 21 wit - -
array-examples/standard_init3_true-unreach-call_ground.i true .46 .50 22 wit - -
array-examples/standard_init4_true-unreach-call_ground.i true .38 .40 22 wit - -
array-examples/standard_init5_true-unreach-call_ground.i true .46 .50 22 wit - -
array-examples/standard_init6_true-unreach-call_ground.i true .44 .47 22 wit - -
array-examples/standard_init7_true-unreach-call_ground.i true .43 .46 22 wit - -
array-examples/standard_init8_true-unreach-call_ground.i true .47 .50 22 wit - -
array-examples/standard_init9_true-unreach-call_ground.i true .41 .45 22 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i true .47 .51 22 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i true .42 .45 21 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i true .44 .48 21 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i true .40 .42 22 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i true .44 .46 22 wit - -
array-examples/standard_partition_true-unreach-call_ground.i true .34 .36 22 wit - -
array-examples/standard_password_true-unreach-call_ground.i true .47 .50 21 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i unknown 300    300    77 wit - -
array-examples/standard_running_true-unreach-call.i true .46 .49 22 wit - -
array-examples/standard_sentinel_true-unreach-call.i true .62 .65 23 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i true .48 .51 21 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i true .55 .59 23 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i true 5.6  5.6  35 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i true 5.0  5.0  35 wit - -
array-examples/standard_two_index_01_true-unreach-call.i true .44 .47 21 wit - -
array-examples/standard_two_index_02_true-unreach-call.i true .43 .45 21 wit - -
array-examples/standard_two_index_03_true-unreach-call.i true .39 .42 21 wit - -
array-examples/standard_two_index_04_true-unreach-call.i true .44 .47 21 wit - -
array-examples/standard_two_index_05_true-unreach-call.i true .38 .40 21 wit - -
array-examples/standard_two_index_06_true-unreach-call.i true .39 .42 21 wit - -
array-examples/standard_two_index_07_true-unreach-call.i true .49 .51 21 wit - -
array-examples/standard_two_index_08_true-unreach-call.i true .41 .44 21 wit - -
array-examples/standard_two_index_09_true-unreach-call.i true .47 .50 21 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i true .48 .50 22 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i true .39 .42 21 wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) 3.7  2.1  170 wit true 11 6.3 340 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 3.7  2.1  170 wit true 11 6.5 320 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 3.8  2.5  170 wit true 12 6.8 320 -
reducercommutativity/rangesum40_false-unreach-call.i true .40 .43 22 wit - -
reducercommutativity/rangesum60_false-unreach-call.i true .42 .45 22 wit - -
reducercommutativity/rangesum_false-unreach-call.i false(reach) 160    160    170 wit true 12 7.3 330 -
reducercommutativity/avg05_true-unreach-call.i true 2.1  2.2  43 wit - -
reducercommutativity/avg10_true-unreach-call.i true 5.8  5.9  45 wit - -
reducercommutativity/avg20_true-unreach-call.i true 24    24    50 wit - -
reducercommutativity/avg40_true-unreach-call.i unknown 890    900    130 wit - -
reducercommutativity/avg60_true-unreach-call.i unknown 890    900    140 wit - -
reducercommutativity/avg_true-unreach-call.i unknown 890    900    100 wit - -
reducercommutativity/max05_true-unreach-call.i true 6.2  6.2  27 wit - -
reducercommutativity/max10_true-unreach-call.i true 260    260    43 wit - -
reducercommutativity/max20_true-unreach-call.i unknown 890    900    130 wit - -
reducercommutativity/max40_true-unreach-call.i unknown 890    900    330 wit - -
reducercommutativity/max60_true-unreach-call.i unknown 890    900    180 wit - -
reducercommutativity/max_true-unreach-call.i unknown 890    900    76 wit - -
reducercommutativity/sep05_true-unreach-call.i true 2.0  2.0  34 wit - -
reducercommutativity/sep10_true-unreach-call.i true 7.1  7.2  52 wit - -
reducercommutativity/sep20_true-unreach-call.i true 630    630    100 wit - -
reducercommutativity/sep40_true-unreach-call.i unknown 890    900    190 wit - -
reducercommutativity/sep60_true-unreach-call.i unknown 890    900    250 wit - -
reducercommutativity/sep_true-unreach-call.i unknown 900    900    140 wit - -
reducercommutativity/sum05_true-unreach-call.i true 1.5  1.5  22 wit - -
reducercommutativity/sum10_true-unreach-call.i true 3.0  3.1  23 wit - -
reducercommutativity/sum20_true-unreach-call.i true 6.9  7.1  23 wit - -
reducercommutativity/sum40_true-unreach-call.i true 16    17    23 wit - -
reducercommutativity/sum60_true-unreach-call.i true 26    27    24 wit - -
reducercommutativity/sum_true-unreach-call.i unknown 890    900    130 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 35000    35000    17000 118 45   27   1300   118 0  
    correct results 74 1200    1200    2500 4 45   27   1300   0 0  
        correct true 70 1000    1000    1800 4 0   0   0   0 0  
        correct false 4 170    170    670 0 45   27   1300   0 0  
    incorrect results 2 .82 .88 43 0 0   0   0   0 0  
        incorrect true 2 .82 .88 43 0 0   0   0   0 0  
        incorrect false 0
score (118 tasks, max score: 202) 80
Run set sv-comp16.ArraysReach