Tool SMACK+Corral 1.5.2
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:05:16 CET [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.ArraysReach
Options -w error-witness.graphml [[ ../../results-verified/smack.2016-01-07_0905.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 false(reach) 5.0 4.9 86 wit timeout 91 52   1500 -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i false(reach) 3.9 3.8 99 wit true 14 8.1 340 -
array-examples/sorting_bubblesort_false-unreach-call_ground.i false(reach) 3.8 3.8 99 wit true 14 8.4 320 -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i false(reach) 28   27   830 wit timeout 91 60   1600 -
array-examples/sorting_selectionsort_false-unreach-call_ground.i false(reach) 320   320   1100 wit true 12 7.4 340 -
array-examples/standard_allDiff2_false-unreach-call_ground.i false(reach) 8.9 8.7 99 wit timeout 91 55   1800 -
array-examples/standard_copy1_false-unreach-call_ground.i false(reach) 3.1 3.1 79 wit true 17 9.6 420 -
array-examples/standard_copy2_false-unreach-call_ground.i false(reach) 3.4 3.4 75 wit true 19 10   420 -
array-examples/standard_copy3_false-unreach-call_ground.i false(reach) 3.7 3.6 79 wit true 19 11   430 -
array-examples/standard_copy4_false-unreach-call_ground.i false(reach) 3.7 3.7 83 wit true 18 10   420 -
array-examples/standard_copy5_false-unreach-call_ground.i false(reach) 3.8 3.7 87 wit true 21 13   500 -
array-examples/standard_copy6_false-unreach-call_ground.i false(reach) 4.1 4.1 89 wit true 24 20   490 -
array-examples/standard_copy7_false-unreach-call_ground.i false(reach) 4.0 3.9 87 wit true 26 14   510 -
array-examples/standard_copy8_false-unreach-call_ground.i false(reach) 3.9 3.8 92 wit true 25 14   530 -
array-examples/standard_copy9_false-unreach-call_ground.i false(reach) 4.4 4.3 86 wit true 26 17   530 -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(reach) 3.4 3.3 81 wit true 21 13   440 -
array-examples/standard_init1_false-unreach-call_ground.i false(reach) 3.1 3.1 79 wit true 20 13   420 -
array-examples/standard_init2_false-unreach-call_ground.i false(reach) 3.4 3.3 77 wit true 17 9.8 370 -
array-examples/standard_init3_false-unreach-call_ground.i false(reach) 3.4 3.4 80 wit true 17 11   360 -
array-examples/standard_init4_false-unreach-call_ground.i false(reach) 3.5 3.4 75 wit true 17 10   360 -
array-examples/standard_init5_false-unreach-call_ground.i false(reach) 3.6 3.6 79 wit true 17 9.1 350 -
array-examples/standard_init6_false-unreach-call_ground.i false(reach) 3.6 3.6 79 wit true 18 10   370 -
array-examples/standard_init7_false-unreach-call_ground.i false(reach) 3.8 3.7 84 wit true 19 12   400 -
array-examples/standard_init8_false-unreach-call_ground.i false(reach) 3.9 3.9 83 wit true 21 11   390 -
array-examples/standard_init9_false-unreach-call_ground.i false(reach) 3.9 3.8 90 wit true 19 11   390 -
array-examples/standard_minInArray_false-unreach-call_ground.i false(reach) 3.6 3.6 78 wit true 16 10   360 -
array-examples/standard_partition_false-unreach-call_ground.i false(reach) 3.9 3.9 93 wit true 29 17   500 -
array-examples/standard_running_false-unreach-call.i false(reach) 3.4 3.4 81 wit timeout 90 56   1700 -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i true 4.0 3.9 93 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i true 880   880   200 wit - -
array-examples/relax_true-unreach-call.i true 880   880   300 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i true 3.1 3.1 70 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i true 6.9 6.8 90 wit - -
array-examples/sanfoundry_24_true-unreach-call.i true 2.6 2.6 73 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i true 3.8 3.8 78 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2.5 2.5 64 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i true 28   28   140 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 880   930   1000 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i true 3.0 3.0 74 wit - -
array-examples/standard_compare_true-unreach-call_ground.i true 3.3 3.2 79 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i true 3.4 3.4 77 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i true 3.5 3.5 87 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i true 3.6 3.5 80 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i true 3.7 3.7 88 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i true 3.8 3.7 91 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i true 4.0 3.9 90 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i true 4.2 4.2 93 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i true 4.4 4.4 97 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i true 4.6 4.5 90 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 4.0 4.0 82 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 4.9 4.8 91 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 3.8 3.8 81 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i true 3.5 3.5 75 wit - -
array-examples/standard_find_true-unreach-call_ground.i true 3.5 3.5 78 wit - -
array-examples/standard_init1_true-unreach-call_ground.i true 3.2 3.2 79 wit - -
array-examples/standard_init2_true-unreach-call_ground.i true 3.2 3.2 77 wit - -
array-examples/standard_init3_true-unreach-call_ground.i true 3.3 3.3 76 wit - -
array-examples/standard_init4_true-unreach-call_ground.i true 3.4 3.3 74 wit - -
array-examples/standard_init5_true-unreach-call_ground.i true 3.2 3.2 79 wit - -
array-examples/standard_init6_true-unreach-call_ground.i true 3.8 3.8 88 wit - -
array-examples/standard_init7_true-unreach-call_ground.i true 4.0 3.9 85 wit - -
array-examples/standard_init8_true-unreach-call_ground.i true 3.9 3.8 86 wit - -
array-examples/standard_init9_true-unreach-call_ground.i true 3.8 3.8 94 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i true 3.7 3.7 78 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i true 3.6 3.6 82 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i true 3.1 3.1 71 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i true 150   150   100 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i true 84   84   98 wit - -
array-examples/standard_partition_true-unreach-call_ground.i true 27   27   92 wit - -
array-examples/standard_password_true-unreach-call_ground.i true 3.3 3.3 80 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i true 3.3 3.3 78 wit - -
array-examples/standard_running_true-unreach-call.i true 3.2 3.2 72 wit - -
array-examples/standard_sentinel_true-unreach-call.i true 3.2 3.2 69 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i true 3.3 3.3 76 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i true 3.3 3.3 76 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i true 880   880   310 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i true 880   880   320 wit - -
array-examples/standard_two_index_01_true-unreach-call.i error (1) 130   130   9800 wit - -
array-examples/standard_two_index_02_true-unreach-call.i true 2.7 2.7 71 wit - -
array-examples/standard_two_index_03_true-unreach-call.i timeout 900   880   4000 wit - -
array-examples/standard_two_index_04_true-unreach-call.i true 3.0 3.0 73 wit - -
array-examples/standard_two_index_05_true-unreach-call.i true 2.9 2.9 73 wit - -
array-examples/standard_two_index_06_true-unreach-call.i true 900   880   1200 wit - -
array-examples/standard_two_index_07_true-unreach-call.i true 2.2 2.2 72 wit - -
array-examples/standard_two_index_08_true-unreach-call.i true 3.0 3.1 71 wit - -
array-examples/standard_two_index_09_true-unreach-call.i true 2.9 2.9 77 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i true 880   880   410 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i true 3.5 3.5 79 wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) 3.4 3.4 69 wit false(reach) 23 14   380 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 3.6 3.5 74 wit true 30 17   430 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 3.3 3.2 91 wit true 33 19   530 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 4.3 4.2 110 wit true 43 23   590 -
reducercommutativity/rangesum60_false-unreach-call.i false(reach) 4.9 4.8 140 wit true 46 24   790 -
reducercommutativity/rangesum_false-unreach-call.i false(reach) 3.7 3.6 85 wit false(reach) 21 12   400 -
reducercommutativity/avg05_true-unreach-call.i true 2.8 2.8 65 wit - -
reducercommutativity/avg10_true-unreach-call.i true 2.7 2.7 67 wit - -
reducercommutativity/avg20_true-unreach-call.i true 2.9 2.9 75 wit - -
reducercommutativity/avg40_true-unreach-call.i true 3.2 3.2 90 wit - -
reducercommutativity/avg60_true-unreach-call.i true 3.3 3.3 110 wit - -
reducercommutativity/avg_true-unreach-call.i timeout 880   930   1200 wit - -
reducercommutativity/max05_true-unreach-call.i true 2.9 2.9 68 wit - -
reducercommutativity/max10_true-unreach-call.i true 3.1 3.1 73 wit - -
reducercommutativity/max20_true-unreach-call.i true 3.6 3.6 80 wit - -
reducercommutativity/max40_true-unreach-call.i true 7.5 7.5 120 wit - -
reducercommutativity/max60_true-unreach-call.i true 12   12   170 wit - -
reducercommutativity/max_true-unreach-call.i true 880   880   370 wit - -
reducercommutativity/sep05_true-unreach-call.i true 2.8 2.8 66 wit - -
reducercommutativity/sep10_true-unreach-call.i true 3.8 3.8 70 wit - -
reducercommutativity/sep20_true-unreach-call.i timeout 880   930   90 wit - -
reducercommutativity/sep40_true-unreach-call.i timeout 880   930   130 wit - -
reducercommutativity/sep60_true-unreach-call.i timeout 880   930   180 wit - -
reducercommutativity/sep_true-unreach-call.i true 880   880   180 wit - -
reducercommutativity/sum05_true-unreach-call.i true 2.8 2.8 69 wit - -
reducercommutativity/sum10_true-unreach-call.i true 2.8 2.8 71 wit - -
reducercommutativity/sum20_true-unreach-call.i true 2.8 2.8 72 wit - -
reducercommutativity/sum40_true-unreach-call.i true 3.1 3.2 90 wit - -
reducercommutativity/sum60_true-unreach-call.i true 3.4 3.3 120 wit - -
reducercommutativity/sum_true-unreach-call.i true 880   880   380 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 14000 15000 30000 118 1000   610   20000   118 0  
    correct results 111 9000 8900 14000 30 1000   610   20000   0 0  
        correct true 77 8500 8500 9300 28 0   0   0   0 0  
        correct false 34 470 470 4700 2 1000   610   20000   0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (118 tasks, max score: 202) 188
Run set sv-comp16.ArraysReach