Tool symbiotic 3.0.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-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-07 09:04:54 CET [[ 2016-01-15 22:39:28 CET ]]
Run set sv-comp16.ArraysReach
Options [[ ../../results-verified/symbiotic3.2016-01-07_0904.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 900     900    4300   wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 900     900    5300   wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 900     900    5300   wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 900     900    810   wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 900     900    870   wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 900     910    650   wit - -
array-examples/standard_copy1_false-unreach-call_ground.i false(reach) 1.2   1.2  12   wit unknown 9.4 5.4 320 -
array-examples/standard_copy2_false-unreach-call_ground.i false(reach) 20     20    93   wit unknown 8.8 5.1 320 -
array-examples/standard_copy3_false-unreach-call_ground.i false(reach) 22     22    160   wit unknown 8.5 5.5 320 -
array-examples/standard_copy4_false-unreach-call_ground.i false(reach) 22     22    180   wit unknown 8.9 5.4 300 -
array-examples/standard_copy5_false-unreach-call_ground.i false(reach) 23     23    200   wit unknown 9.3 5.3 310 -
array-examples/standard_copy6_false-unreach-call_ground.i false(reach) 24     24    230   wit unknown 8.8 5.3 300 -
array-examples/standard_copy7_false-unreach-call_ground.i false(reach) 24     25    250   wit unknown 8.7 5.0 320 -
array-examples/standard_copy8_false-unreach-call_ground.i false(reach) 26     26    280   wit unknown 9.2 5.4 310 -
array-examples/standard_copy9_false-unreach-call_ground.i false(reach) 26     26    300   wit unknown 8.5 5.2 310 -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(reach) 19     19    49   wit unknown 10   6.0 320 -
array-examples/standard_init1_false-unreach-call_ground.i false(reach) 18     19    27   wit unknown 9.5 5.4 320 -
array-examples/standard_init2_false-unreach-call_ground.i false(reach) 19     19    46   wit unknown 9.4 6.1 320 -
array-examples/standard_init3_false-unreach-call_ground.i false(reach) 19     19    65   wit unknown 10   5.8 320 -
array-examples/standard_init4_false-unreach-call_ground.i false(reach) 20     20    84   wit unknown 9.1 5.2 310 -
array-examples/standard_init5_false-unreach-call_ground.i false(reach) 20     20    100   wit unknown 11   7.4 340 -
array-examples/standard_init6_false-unreach-call_ground.i false(reach) 21     21    120   wit unknown 9.4 7.0 320 -
array-examples/standard_init7_false-unreach-call_ground.i false(reach) 21     21    140   wit unknown 8.6 4.9 300 -
array-examples/standard_init8_false-unreach-call_ground.i false(reach) 22     22    160   wit unknown 9.4 5.4 320 -
array-examples/standard_init9_false-unreach-call_ground.i false(reach) 22     22    180   wit unknown 8.4 5.2 300 -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 900     900    840   wit - -
array-examples/standard_partition_false-unreach-call_ground.i out of memory 16     16    15000   wit - -
array-examples/standard_running_false-unreach-call.i timeout 900     900    2800   wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i timeout 900     900    54   wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 900     900    1800   wit - -
array-examples/relax_true-unreach-call.i unknown .12  .13 7.0 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 900     900    830   wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i unknown .19  .21 6.5 wit - -
array-examples/sanfoundry_24_true-unreach-call.i timeout 900     900    1700   wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 900     900    730   wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true .091 .12 5.9 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 900     900    5200   wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 900     900    880   wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i true 75     75    11000   wit - -
array-examples/standard_compare_true-unreach-call_ground.i timeout 900     900    2700   wit - -
array-examples/standard_copy1_true-unreach-call_ground.i true 19     19    110   wit - -
array-examples/standard_copy2_true-unreach-call_ground.i true 20     20    130   wit - -
array-examples/standard_copy3_true-unreach-call_ground.i true 21     21    160   wit - -
array-examples/standard_copy4_true-unreach-call_ground.i true 21     21    180   wit - -
array-examples/standard_copy5_true-unreach-call_ground.i true 22     22    200   wit - -
array-examples/standard_copy6_true-unreach-call_ground.i true 23     23    230   wit - -
array-examples/standard_copy7_true-unreach-call_ground.i true 23     23    260   wit - -
array-examples/standard_copy8_true-unreach-call_ground.i true 24     24    280   wit - -
array-examples/standard_copy9_true-unreach-call_ground.i true 25     25    300   wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 20     20    110   wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 21     21    130   wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 21     21    150   wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i true 20     20    86   wit - -
array-examples/standard_find_true-unreach-call_ground.i timeout 900     900    68   wit - -
array-examples/standard_init1_true-unreach-call_ground.i true 19     19    65   wit - -
array-examples/standard_init2_true-unreach-call_ground.i true 20     20    83   wit - -
array-examples/standard_init3_true-unreach-call_ground.i true 19     19    100   wit - -
array-examples/standard_init4_true-unreach-call_ground.i true 20     20    120   wit - -
array-examples/standard_init5_true-unreach-call_ground.i true 21     21    140   wit - -
array-examples/standard_init6_true-unreach-call_ground.i true 22     22    160   wit - -
array-examples/standard_init7_true-unreach-call_ground.i true 22     22    180   wit - -
array-examples/standard_init8_true-unreach-call_ground.i true 23     23    200   wit - -
array-examples/standard_init9_true-unreach-call_ground.i true 23     23    220   wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 900     900    810   wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 900     900    810   wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i true 18     18    61   wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 900     900    2700   wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 15     15    15000   wit - -
array-examples/standard_partition_true-unreach-call_ground.i out of memory 17     17    15000   wit - -
array-examples/standard_password_true-unreach-call_ground.i timeout 900     900    2700   wit - -
array-examples/standard_reverse_true-unreach-call_ground.i true 20     20    110   wit - -
array-examples/standard_running_true-unreach-call.i timeout 900     900    2900   wit - -
array-examples/standard_sentinel_true-unreach-call.i timeout 900     900    730   wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i true 20     20    65   wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 900     900    1500   wit - -
array-examples/standard_strcpy_original_true-unreach-call.i timeout 900     900    200   wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 900     900    180   wit - -
array-examples/standard_two_index_01_true-unreach-call.i true 18     18    16   wit - -
array-examples/standard_two_index_02_true-unreach-call.i true 19     19    61   wit - -
array-examples/standard_two_index_03_true-unreach-call.i true 18     18    9.6 wit - -
array-examples/standard_two_index_04_true-unreach-call.i true 18     18    37   wit - -
array-examples/standard_two_index_05_true-unreach-call.i true 19     19    35   wit - -
array-examples/standard_two_index_06_true-unreach-call.i true 18     18    7.9 wit - -
array-examples/standard_two_index_07_true-unreach-call.i true 18     18    27   wit - -
array-examples/standard_two_index_08_true-unreach-call.i true 18     18    25   wit - -
array-examples/standard_two_index_09_true-unreach-call.i true 18     18    24   wit - -
array-examples/standard_vararg_true-unreach-call_ground.i timeout 900     900    69   wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i true 20     20    200   wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) 36     36    7.8 wit unknown 9.2 5.3 320 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 18     18    8.6 wit unknown 9.2 5.9 310 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 18     18    19   wit unknown 9.2 5.2 310 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 35     35    24   wit unknown 9.2 5.4 300 -
reducercommutativity/rangesum60_false-unreach-call.i false(reach) 18     18    25   wit unknown 10   6.0 310 -
reducercommutativity/rangesum_false-unreach-call.i unknown .12  .14 7.0 wit - -
reducercommutativity/avg05_true-unreach-call.i true 18     18    5.9 wit - -
reducercommutativity/avg10_true-unreach-call.i true 18     18    5.9 wit - -
reducercommutativity/avg20_true-unreach-call.i true 18     18    6.2 wit - -
reducercommutativity/avg40_true-unreach-call.i true 18     18    6.5 wit - -
reducercommutativity/avg60_true-unreach-call.i true 18     18    6.7 wit - -
reducercommutativity/avg_true-unreach-call.i unknown .11  .13 7.1 wit - -
reducercommutativity/max05_true-unreach-call.i true 640     640    10   wit - -
reducercommutativity/max10_true-unreach-call.i timeout 900     910    84   wit - -
reducercommutativity/max20_true-unreach-call.i timeout 890     930    210   wit - -
reducercommutativity/max40_true-unreach-call.i timeout 880     930    200   wit - -
reducercommutativity/max60_true-unreach-call.i timeout 890     930    200   wit - -
reducercommutativity/max_true-unreach-call.i unknown .23  .26 7.1 wit - -
reducercommutativity/sep05_true-unreach-call.i true 18     18    6.1 wit - -
reducercommutativity/sep10_true-unreach-call.i true 18     18    6.1 wit - -
reducercommutativity/sep20_true-unreach-call.i true 18     18    6.1 wit - -
reducercommutativity/sep40_true-unreach-call.i true 18     18    6.4 wit - -
reducercommutativity/sep60_true-unreach-call.i true 18     18    7.0 wit - -
reducercommutativity/sep_true-unreach-call.i unknown .15  .17 7.5 wit - -
reducercommutativity/sum05_true-unreach-call.i true 18     18    5.8 wit - -
reducercommutativity/sum10_true-unreach-call.i true 18     18    6.1 wit - -
reducercommutativity/sum20_true-unreach-call.i true 18     18    6.2 wit - -
reducercommutativity/sum40_true-unreach-call.i true 18     18    6.4 wit - -
reducercommutativity/sum60_true-unreach-call.i true 18     18    6.6 wit - -
reducercommutativity/sum_true-unreach-call.i unknown .22  .24 7.2 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 30000 30000 110000 118 220   130   7500   118 0  
    correct results 77 2200 2200 18000 0 220   130   7500   0 0  
        correct true 53 1700 1700 15000 0 0   0   0   0 0  
        correct false 24 510 520 2800 0 220   130   7500   0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (118 tasks, max score: 202) 130
Run set sv-comp16.ArraysReach