Tool SeaHorn-F16 0.1.0
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-13 15:22:34 CET [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.ArraysReach
Options --cex=error-witness.graphml [[ ../../results-verified/seahorn.2016-01-11_2135.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 900    450     850
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 900    450     520
array-examples/sorting_bubblesort_false-unreach-call_ground.i 900    450     520
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 900    450     1000
array-examples/sorting_selectionsort_false-unreach-call_ground.i 900    450     970
array-examples/standard_allDiff2_false-unreach-call_ground.i .30 .18  42 11   7.8 330
array-examples/standard_copy1_false-unreach-call_ground.i .26 .15  28 12   7.6 320
array-examples/standard_copy2_false-unreach-call_ground.i .40 .24  40 10   6.5 330
array-examples/standard_copy3_false-unreach-call_ground.i .28 .17  40 12   6.6 350
array-examples/standard_copy4_false-unreach-call_ground.i .30 .17  40 11   6.6 320
array-examples/standard_copy5_false-unreach-call_ground.i .29 .17  40 11   6.9 330
array-examples/standard_copy6_false-unreach-call_ground.i .28 .17  40 12   7.9 330
array-examples/standard_copy7_false-unreach-call_ground.i .31 .19  40 11   6.4 330
array-examples/standard_copy8_false-unreach-call_ground.i .30 .18  40 12   6.8 330
array-examples/standard_copy9_false-unreach-call_ground.i .36 .22  40 11   8.9 330
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 900    450     430
array-examples/standard_init1_false-unreach-call_ground.i 900    450     410
array-examples/standard_init2_false-unreach-call_ground.i 900    450     460
array-examples/standard_init3_false-unreach-call_ground.i 900    450     450
array-examples/standard_init4_false-unreach-call_ground.i 900    450     460
array-examples/standard_init5_false-unreach-call_ground.i 900    450     450
array-examples/standard_init6_false-unreach-call_ground.i 900    450     460
array-examples/standard_init7_false-unreach-call_ground.i 900    450     450
array-examples/standard_init8_false-unreach-call_ground.i 900    450     460
array-examples/standard_init9_false-unreach-call_ground.i 900    450     460
array-examples/standard_minInArray_false-unreach-call_ground.i 900    450     400
array-examples/standard_partition_false-unreach-call_ground.i 900    450     540
array-examples/standard_running_false-unreach-call.i 900    450     310
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i .27 .17  25
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 900    450     500
array-examples/relax_true-unreach-call.i .56 .31  54
array-examples/sanfoundry_02_true-unreach-call_ground.i 900    450     510
array-examples/sanfoundry_10_true-unreach-call_ground.i 900    450     500
array-examples/sanfoundry_24_true-unreach-call.i .27 .16  36
array-examples/sanfoundry_27_true-unreach-call_ground.i 900    450     400
array-examples/sanfoundry_43_true-unreach-call_ground.i .16 .098 24
array-examples/sorting_bubblesort_true-unreach-call_ground.i 900    450     520
array-examples/sorting_selectionsort_true-unreach-call_ground.i 900    450     960
array-examples/standard_compareModified_true-unreach-call_ground.i 900    450     520
array-examples/standard_compare_true-unreach-call_ground.i 900    450     390
array-examples/standard_copy1_true-unreach-call_ground.i .39 .23  40
array-examples/standard_copy2_true-unreach-call_ground.i .30 .19  40
array-examples/standard_copy3_true-unreach-call_ground.i .29 .18  40
array-examples/standard_copy4_true-unreach-call_ground.i .33 .20  40
array-examples/standard_copy5_true-unreach-call_ground.i .30 .19  40
array-examples/standard_copy6_true-unreach-call_ground.i .30 .19  40
array-examples/standard_copy7_true-unreach-call_ground.i .25 .14  40
array-examples/standard_copy8_true-unreach-call_ground.i .31 .19  40
array-examples/standard_copy9_true-unreach-call_ground.i .31 .20  40
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 900    450     470
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 900    450     450
array-examples/standard_copyInitSum_true-unreach-call_ground.i 900    450     460
array-examples/standard_copyInit_true-unreach-call_ground.i 900    450     410
array-examples/standard_find_true-unreach-call_ground.i .33 .20  43
array-examples/standard_init1_true-unreach-call_ground.i 900    450     450
array-examples/standard_init2_true-unreach-call_ground.i 900    450     460
array-examples/standard_init3_true-unreach-call_ground.i 900    450     450
array-examples/standard_init4_true-unreach-call_ground.i 900    450     450
array-examples/standard_init5_true-unreach-call_ground.i 900    450     450
array-examples/standard_init6_true-unreach-call_ground.i 900    450     450
array-examples/standard_init7_true-unreach-call_ground.i 900    450     450
array-examples/standard_init8_true-unreach-call_ground.i 900    450     460
array-examples/standard_init9_true-unreach-call_ground.i 900    450     460
array-examples/standard_maxInArray_true-unreach-call_ground.i 900    450     400
array-examples/standard_minInArray_true-unreach-call_ground.i 900    450     390
array-examples/standard_palindrome_true-unreach-call_ground.i 900    450     410
array-examples/standard_partial_init_true-unreach-call_ground.i 900    450     680
array-examples/standard_partition_original_true-unreach-call_ground.i 900    450     240
array-examples/standard_partition_true-unreach-call_ground.i 900    450     410
array-examples/standard_password_true-unreach-call_ground.i 900    450     390
array-examples/standard_reverse_true-unreach-call_ground.i 900    450     480
array-examples/standard_running_true-unreach-call.i 900    450     320
array-examples/standard_sentinel_true-unreach-call.i .24 .14  40
array-examples/standard_seq_init_true-unreach-call_ground.i 900    450     450
array-examples/standard_strcmp_true-unreach-call_ground.i 900    450     400
array-examples/standard_strcpy_original_true-unreach-call.i .23 .14  42
array-examples/standard_strcpy_true-unreach-call_ground.i .35 .21  42
array-examples/standard_two_index_01_true-unreach-call.i .29 .18  40
array-examples/standard_two_index_02_true-unreach-call.i 900    450     400
array-examples/standard_two_index_03_true-unreach-call.i 900    450     610
array-examples/standard_two_index_04_true-unreach-call.i 900    450     400
array-examples/standard_two_index_05_true-unreach-call.i 900    450     420
array-examples/standard_two_index_06_true-unreach-call.i 900    450     560
array-examples/standard_two_index_07_true-unreach-call.i 900    450     400
array-examples/standard_two_index_08_true-unreach-call.i 900    450     400
array-examples/standard_two_index_09_true-unreach-call.i 900    450     400
array-examples/standard_vararg_true-unreach-call_ground.i .26 .15  42
array-examples/standard_vector_difference_true-unreach-call_ground.i 900    450     400
reducercommutativity/rangesum05_false-unreach-call.i .25 .16  30
reducercommutativity/rangesum10_false-unreach-call.i .20 .13  30
reducercommutativity/rangesum20_false-unreach-call.i 75    38     95 12   7.3 330
reducercommutativity/rangesum40_false-unreach-call.i 200    100     330 14   7.7 360
reducercommutativity/rangesum60_false-unreach-call.i 780    390     730 14   7.8 350
reducercommutativity/rangesum_false-unreach-call.i 4.3  2.2   84 12   7.5 340
reducercommutativity/avg05_true-unreach-call.i .21 .14  30
reducercommutativity/avg10_true-unreach-call.i .21 .14  30
reducercommutativity/avg20_true-unreach-call.i .23 .15  30
reducercommutativity/avg40_true-unreach-call.i 370    190     350
reducercommutativity/avg60_true-unreach-call.i 900    450     430
reducercommutativity/avg_true-unreach-call.i .70 .38  58
reducercommutativity/max05_true-unreach-call.i .21 .14  30
reducercommutativity/max10_true-unreach-call.i .23 .15  30
reducercommutativity/max20_true-unreach-call.i .22 .14  31
reducercommutativity/max40_true-unreach-call.i 430    220     400
reducercommutativity/max60_true-unreach-call.i 900    450     420
reducercommutativity/max_true-unreach-call.i .87 .46  64
reducercommutativity/sep05_true-unreach-call.i .18 .12  30
reducercommutativity/sep10_true-unreach-call.i .21 .14  30
reducercommutativity/sep20_true-unreach-call.i .19 .13  30
reducercommutativity/sep40_true-unreach-call.i 900    450     390
reducercommutativity/sep60_true-unreach-call.i 900    450     290
reducercommutativity/sep_true-unreach-call.i 1.3  .69  71
reducercommutativity/sum05_true-unreach-call.i .25 .16  30
reducercommutativity/sum10_true-unreach-call.i .21 .14  30
reducercommutativity/sum20_true-unreach-call.i .20 .13  30
reducercommutativity/sum40_true-unreach-call.i 370    180     340
reducercommutativity/sum60_true-unreach-call.i 900    450     430
reducercommutativity/sum_true-unreach-call.i .72 .38  59
../../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 60000    30000    34000 118 160   100   4700   118 0  
    correct results 29 1100    540    2100 14 160   100   4700   0 0  
        correct true 15 3.2  2.1  450 14 0   0   0   0 0  
        correct false 14 1100    530    1600 0 160   100   4700   0 0  
    incorrect results 25 1200    590    2100 0 0   0   0   0 0  
        incorrect true 2 .44 .29 60 0 0   0   0   0 0  
        incorrect false 23 1200    590    2000 0 0   0   0   0 0  
score (118 tasks, max score: 202) -388
Run set sv-comp16.ArraysReach