Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.ArraysReach
Options -svcomp [[ ../../results-verified/forest.2016-01-09_2349.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 24     20     920   wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i true 21     21     130   wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i false(valid-free) 330     330     130   wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i false(reach) 29     24     970   wit true 11   7.1 320 -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 24     24     130   wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 20     19     140   wit - -
array-examples/standard_copy1_false-unreach-call_ground.i false(reach) 4.2   4.3   130   wit true 11   6.9 330 -
array-examples/standard_copy2_false-unreach-call_ground.i unknown 5.6   5.7   120   wit - -
array-examples/standard_copy3_false-unreach-call_ground.i error (134) 110     110     270   wit - -
array-examples/standard_copy4_false-unreach-call_ground.i true 160     160     340   wit - -
array-examples/standard_copy5_false-unreach-call_ground.i unknown 10     10     140   wit - -
array-examples/standard_copy6_false-unreach-call_ground.i unknown 12     12     140   wit - -
array-examples/standard_copy7_false-unreach-call_ground.i true 13     13     150   wit - -
array-examples/standard_copy8_false-unreach-call_ground.i unknown 14     14     130   wit - -
array-examples/standard_copy9_false-unreach-call_ground.i error (139) 170     170     670   wit - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(reach) 5.0   5.1   120   wit true 10   6.9 320 -
array-examples/standard_init1_false-unreach-call_ground.i false(reach) 2.6   2.7   130   wit true 10   6.4 340 -
array-examples/standard_init2_false-unreach-call_ground.i false(reach) 3.0   3.0   130   wit true 11   6.5 320 -
array-examples/standard_init3_false-unreach-call_ground.i false(reach) 4.1   4.2   130   wit true 9.7 6.5 330 -
array-examples/standard_init4_false-unreach-call_ground.i false(reach) 4.7   4.8   130   wit true 11   7.6 320 -
array-examples/standard_init5_false-unreach-call_ground.i false(reach) 5.6   5.6   120   wit true 10   7.0 330 -
array-examples/standard_init6_false-unreach-call_ground.i unknown 6.1   6.2   130   wit - -
array-examples/standard_init7_false-unreach-call_ground.i false(reach) 7.2   7.3   130   wit true 12   7.1 350 -
array-examples/standard_init8_false-unreach-call_ground.i false(reach) 7.3   7.4   130   wit true 13   8.3 340 -
array-examples/standard_init9_false-unreach-call_ground.i false(reach) 8.6   8.6   130   wit true 11   7.5 320 -
array-examples/standard_minInArray_false-unreach-call_ground.i false(reach) 3.4   3.4   130   wit true 11   7.2 330 -
array-examples/standard_partition_false-unreach-call_ground.i false(reach) 6.8   6.9   120   wit true 10   5.7 330 -
array-examples/standard_running_false-unreach-call.i unknown 6.0   6.1   130   wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i unknown 7.0   7.1   120   wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 5.5   5.6   130   wit - -
array-examples/relax_true-unreach-call.i error (139) .059 .066 4.0 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 7.2   7.3   130   wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i true .60  .68  38   wit - -
array-examples/sanfoundry_24_true-unreach-call.i unknown 3.7   3.7   120   wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 3.8   3.9   130   wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true 43     44     130   wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 22     22     130   wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i error (134) 15     15     9.4 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i unknown 7.0   7.1   120   wit - -
array-examples/standard_compare_true-unreach-call_ground.i unknown 3.8   3.9   120   wit - -
array-examples/standard_copy1_true-unreach-call_ground.i unknown 3.5   3.5   120   wit - -
array-examples/standard_copy2_true-unreach-call_ground.i unknown 5.7   5.8   130   wit - -
array-examples/standard_copy3_true-unreach-call_ground.i true 6.9   7.0   130   wit - -
array-examples/standard_copy4_true-unreach-call_ground.i unknown 7.8   7.9   120   wit - -
array-examples/standard_copy5_true-unreach-call_ground.i unknown 10     10     140   wit - -
array-examples/standard_copy6_true-unreach-call_ground.i unknown 11     11     120   wit - -
array-examples/standard_copy7_true-unreach-call_ground.i unknown 13     13     120   wit - -
array-examples/standard_copy8_true-unreach-call_ground.i unknown 14     14     120   wit - -
array-examples/standard_copy9_true-unreach-call_ground.i unknown 17     17     130   wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 490     490     150   wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unknown 7.3   7.4   120   wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i unknown 5.1   5.2   120   wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i true 3.5   3.7   120   wit - -
array-examples/standard_find_true-unreach-call_ground.i true 2.7   2.8   130   wit - -
array-examples/standard_init1_true-unreach-call_ground.i true 2.2   2.3   130   wit - -
array-examples/standard_init2_true-unreach-call_ground.i true 2.8   2.9   120   wit - -
array-examples/standard_init3_true-unreach-call_ground.i unknown 4.0   4.1   130   wit - -
array-examples/standard_init4_true-unreach-call_ground.i error (134) 110     110     130   wit - -
array-examples/standard_init5_true-unreach-call_ground.i true 17     17     130   wit - -
array-examples/standard_init6_true-unreach-call_ground.i unknown 6.0   6.0   130   wit - -
array-examples/standard_init7_true-unreach-call_ground.i true 78     79     130   wit - -
array-examples/standard_init8_true-unreach-call_ground.i unknown 7.2   7.3   120   wit - -
array-examples/standard_init9_true-unreach-call_ground.i unknown 8.1   8.2   120   wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i true 840     840     130   wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i true 3.1   3.2   130   wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i true 4.1   4.2   120   wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i true 850     850     210   wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i unknown 6.5   6.6   120   wit - -
array-examples/standard_partition_true-unreach-call_ground.i true 13     13     210   wit - -
array-examples/standard_password_true-unreach-call_ground.i true 4.2   4.3   120   wit - -
array-examples/standard_reverse_true-unreach-call_ground.i unknown 3.6   3.7   120   wit - -
array-examples/standard_running_true-unreach-call.i unknown 6.1   6.1   120   wit - -
array-examples/standard_sentinel_true-unreach-call.i false(valid-free) 8.7   8.8   130   wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i unknown 4.6   4.6   120   wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i unknown 2.4   2.5   120   wit - -
array-examples/standard_strcpy_original_true-unreach-call.i true 490     490     150   wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 4.5   4.6   120   wit - -
array-examples/standard_two_index_01_true-unreach-call.i unknown .95  1.0   40   wit - -
array-examples/standard_two_index_02_true-unreach-call.i unknown 3.4   3.5   120   wit - -
array-examples/standard_two_index_03_true-unreach-call.i true .63  .72  14   wit - -
array-examples/standard_two_index_04_true-unreach-call.i true 570     570     150   wit - -
array-examples/standard_two_index_05_true-unreach-call.i error (134) 35     35     130   wit - -
array-examples/standard_two_index_06_true-unreach-call.i true .73  .84  14   wit - -
array-examples/standard_two_index_07_true-unreach-call.i error (134) 50     50     130   wit - -
array-examples/standard_two_index_08_true-unreach-call.i unknown 4.3   4.3   130   wit - -
array-examples/standard_two_index_09_true-unreach-call.i true 3.5   3.6   120   wit - -
array-examples/standard_vararg_true-unreach-call_ground.i true 1.0   1.2   39   wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i unknown 5.4   5.4   130   wit - -
reducercommutativity/rangesum05_false-unreach-call.i error (139) .023 .031 3.3 wit - -
reducercommutativity/rangesum10_false-unreach-call.i error (139) .025 .032 3.3 wit - -
reducercommutativity/rangesum20_false-unreach-call.i error (139) .025 .034 3.3 wit - -
reducercommutativity/rangesum40_false-unreach-call.i error (139) .017 .024 3.2 wit - -
reducercommutativity/rangesum60_false-unreach-call.i error (139) .021 .030 3.5 wit - -
reducercommutativity/rangesum_false-unreach-call.i error (139) .016 .023 3.4 wit - -
reducercommutativity/avg05_true-unreach-call.i error (139) .027 .033 3.4 wit - -
reducercommutativity/avg10_true-unreach-call.i error (139) .024 .031 3.3 wit - -
reducercommutativity/avg20_true-unreach-call.i error (139) .022 .030 3.4 wit - -
reducercommutativity/avg40_true-unreach-call.i error (139) .021 .030 3.3 wit - -
reducercommutativity/avg60_true-unreach-call.i error (139) .022 .030 3.3 wit - -
reducercommutativity/avg_true-unreach-call.i error (139) .025 .030 3.4 wit - -
reducercommutativity/max05_true-unreach-call.i error (139) .021 .028 3.2 wit - -
reducercommutativity/max10_true-unreach-call.i error (139) .021 .029 3.3 wit - -
reducercommutativity/max20_true-unreach-call.i error (139) .015 .019 3.2 wit - -
reducercommutativity/max40_true-unreach-call.i error (139) .024 .031 3.3 wit - -
reducercommutativity/max60_true-unreach-call.i error (139) .020 .024 3.2 wit - -
reducercommutativity/max_true-unreach-call.i error (139) .020 .029 3.2 wit - -
reducercommutativity/sep05_true-unreach-call.i error (139) .012 .020 3.5 wit - -
reducercommutativity/sep10_true-unreach-call.i error (139) .018 .026 3.3 wit - -
reducercommutativity/sep20_true-unreach-call.i error (139) .011 .019 3.2 wit - -
reducercommutativity/sep40_true-unreach-call.i error (139) .023 .031 3.3 wit - -
reducercommutativity/sep60_true-unreach-call.i error (139) .020 .027 3.4 wit - -
reducercommutativity/sep_true-unreach-call.i error (139) .023 .028 3.6 wit - -
reducercommutativity/sum05_true-unreach-call.i error (139) .020 .028 3.3 wit - -
reducercommutativity/sum10_true-unreach-call.i error (139) .024 .029 3.5 wit - -
reducercommutativity/sum20_true-unreach-call.i error (139) .023 .029 3.4 wit - -
reducercommutativity/sum40_true-unreach-call.i error (139) .017 .024 3.4 wit - -
reducercommutativity/sum60_true-unreach-call.i error (139) .018 .021 3.4 wit - -
reducercommutativity/sum_true-unreach-call.i error (139) .027 .033 3.3 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 4900 4900 13000 118 140   91   4300   118 0  
    correct results 35 3500 3500 5200 13 140   91   4300   0 0  
        correct true 22 3400 3400 2600 13 0   0   0   0 0  
        correct false 13 91 88 2500 0 140   91   4300   0 0  
    incorrect results 5 540 540 880 0 0   0   0   0 0  
        incorrect true 3 200 200 620 0 0   0   0   0 0  
        incorrect false 2 340 340 260 0 0   0   0   0 0  
score (118 tasks, max score: 202) -71
Run set sv-comp16.ArraysReach