Tool CBMC
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-03 00:42:25 CET [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.ArraysReach
Options --graphml-cex error-witness.graphml [[ ../../results-verified/cbmc.2016-01-03_0042.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 true 850    850    13000 wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 22    22    15000 wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 22    22    15000 wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i true 77    77    13000 wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i true 78    78    13000 wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i true 850    850    1800 wit - -
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 34    34    15000 wit - -
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 30    30    15000 wit - -
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 38    38    15000 wit - -
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 44    44    15000 wit - -
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 49    49    15000 wit - -
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 56    56    15000 wit - -
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 46    46    15000 wit - -
array-examples/standard_copy8_false-unreach-call_ground.i out of memory 51    51    15000 wit - -
array-examples/standard_copy9_false-unreach-call_ground.i out of memory 55    55    15000 wit - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_init1_false-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_init2_false-unreach-call_ground.i out of memory 26    26    15000 wit - -
array-examples/standard_init3_false-unreach-call_ground.i out of memory 30    30    15000 wit - -
array-examples/standard_init4_false-unreach-call_ground.i out of memory 35    35    15000 wit - -
array-examples/standard_init5_false-unreach-call_ground.i out of memory 40    40    15000 wit - -
array-examples/standard_init6_false-unreach-call_ground.i out of memory 45    45    15000 wit - -
array-examples/standard_init7_false-unreach-call_ground.i out of memory 49    49    15000 wit - -
array-examples/standard_init8_false-unreach-call_ground.i out of memory 39    39    15000 wit - -
array-examples/standard_init9_false-unreach-call_ground.i out of memory 40    40    15000 wit - -
array-examples/standard_minInArray_false-unreach-call_ground.i true 5.1  5.2  420 wit - -
array-examples/standard_partition_false-unreach-call_ground.i true 110    110    14000 wit - -
array-examples/standard_running_false-unreach-call.i out of memory 37    37    15000 wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i true 1.9  2.0  25 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i true 850    850    9900 wit - -
array-examples/relax_true-unreach-call.i true 510    510    14000 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i true 5.6  5.6  470 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i true 130    130    13000 wit - -
array-examples/sanfoundry_24_true-unreach-call.i true 26    26    780 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i true 5.2  5.2  420 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true 1.3  1.4  26 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 23    22    15000 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i true 77    77    13000 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i out of memory 37    36    15000 wit - -
array-examples/standard_compare_true-unreach-call_ground.i true 7.0  7.1  760 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i out of memory 34    34    15000 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 30    30    15000 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 36    36    15000 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 43    43    15000 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 50    50    15000 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 56    56    15000 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 47    47    15000 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i out of memory 51    51    15000 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 55    54    15000 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 37    37    15000 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 33    33    15000 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 28    28    15000 wit - -
array-examples/standard_find_true-unreach-call_ground.i true 8.4  8.5  440 wit - -
array-examples/standard_init1_true-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_init2_true-unreach-call_ground.i out of memory 26    26    15000 wit - -
array-examples/standard_init3_true-unreach-call_ground.i out of memory 31    31    15000 wit - -
array-examples/standard_init4_true-unreach-call_ground.i out of memory 35    35    15000 wit - -
array-examples/standard_init5_true-unreach-call_ground.i out of memory 39    39    15000 wit - -
array-examples/standard_init6_true-unreach-call_ground.i out of memory 45    45    15000 wit - -
array-examples/standard_init7_true-unreach-call_ground.i out of memory 49    49    15000 wit - -
array-examples/standard_init8_true-unreach-call_ground.i out of memory 38    38    15000 wit - -
array-examples/standard_init9_true-unreach-call_ground.i out of memory 41    40    15000 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i true 4.8  4.8  410 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i true 4.9  4.9  410 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i true 80    80    14000 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i true 68    68    14000 wit - -
array-examples/standard_partition_true-unreach-call_ground.i true 110    110    14000 wit - -
array-examples/standard_password_true-unreach-call_ground.i true 7.0  7.0  760 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i out of memory 34    34    15000 wit - -
array-examples/standard_running_true-unreach-call.i out of memory 37    37    15000 wit - -
array-examples/standard_sentinel_true-unreach-call.i true 850    850    2500 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 32    32    15000 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i true 12    12    860 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 39    39    15000 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 39    39    15000 wit - -
array-examples/standard_two_index_01_true-unreach-call.i true 5.8  5.9  2200 wit - -
array-examples/standard_two_index_02_true-unreach-call.i out of memory 34    34    15000 wit - -
array-examples/standard_two_index_03_true-unreach-call.i true 5.9  5.9  2200 wit - -
array-examples/standard_two_index_04_true-unreach-call.i out of memory 34    34    15000 wit - -
array-examples/standard_two_index_05_true-unreach-call.i out of memory 33    33    15000 wit - -
array-examples/standard_two_index_06_true-unreach-call.i true 5.9  6.0  2200 wit - -
array-examples/standard_two_index_07_true-unreach-call.i out of memory 35    34    15000 wit - -
array-examples/standard_two_index_08_true-unreach-call.i out of memory 34    34    15000 wit - -
array-examples/standard_two_index_09_true-unreach-call.i out of memory 35    35    15000 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i true 8.5  8.5  430 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i out of memory 36    36    15000 wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) .34 .35 25 wit false(reach) 20 12 400 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) .48 .51 30 wit false(reach) 47 35 480 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) .64 .66 27 wit false(reach) 33 18 560 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 5.1  5.2  47 wit false(reach) 45 26 660 -
reducercommutativity/rangesum60_false-unreach-call.i false(reach) 12    12    62 wit false(reach) 78 54 910 -
reducercommutativity/rangesum_false-unreach-call.i false(reach) .55 .56 40 wit false(reach) 19 11 400 -
reducercommutativity/avg05_true-unreach-call.i true 850    850    200 wit - -
reducercommutativity/avg10_true-unreach-call.i true 850    850    310 wit - -
reducercommutativity/avg20_true-unreach-call.i true 850    850    410 wit - -
reducercommutativity/avg40_true-unreach-call.i true 850    850    560 wit - -
reducercommutativity/avg60_true-unreach-call.i true 850    850    690 wit - -
reducercommutativity/avg_true-unreach-call.i true 850    850    350 wit - -
reducercommutativity/max05_true-unreach-call.i true 12    12    28 wit - -
reducercommutativity/max10_true-unreach-call.i true 690    690    68 wit - -
reducercommutativity/max20_true-unreach-call.i true 850    850    220 wit - -
reducercommutativity/max40_true-unreach-call.i true 850    850    420 wit - -
reducercommutativity/max60_true-unreach-call.i true 850    850    650 wit - -
reducercommutativity/max_true-unreach-call.i true 850    850    350 wit - -
reducercommutativity/sep05_true-unreach-call.i true 1.2  1.2  29 wit - -
reducercommutativity/sep10_true-unreach-call.i true 2.3  2.4  32 wit - -
reducercommutativity/sep20_true-unreach-call.i true 6.1  6.1  39 wit - -
reducercommutativity/sep40_true-unreach-call.i true 38    39    99 wit - -
reducercommutativity/sep60_true-unreach-call.i true 230    230    180 wit - -
reducercommutativity/sep_true-unreach-call.i true 850    850    930 wit - -
reducercommutativity/sum05_true-unreach-call.i true 180    180    41 wit - -
reducercommutativity/sum10_true-unreach-call.i true 850    850    250 wit - -
reducercommutativity/sum20_true-unreach-call.i true 850    850    480 wit - -
reducercommutativity/sum40_true-unreach-call.i true 850    850    570 wit - -
reducercommutativity/sum60_true-unreach-call.i true 850    850    610 wit - -
reducercommutativity/sum_true-unreach-call.i true 850    850    390 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 22000 22000 1100000 118 240   160   3400   118 0  
    correct results 53 18000 18000 120000 6 240   160   3400   0 0  
        correct true 47 18000 18000 110000 0 0   0   0   0 0  
        correct false 6 19 19 230 6 240   160   3400   0 0  
    incorrect results 6 2000 2000 55000 0 0   0   0   0 0  
        incorrect true 6 2000 2000 55000 0 0   0   0   0 0  
        incorrect false 0
score (118 tasks, max score: 202) -92
Run set sv-comp16.ArraysReach