Tool CPAchecker 1.4-svcomp16c
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-04 06:25:51 CET [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.ArraysReach
Options -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-bam.2016-01-04_0625.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 3.6 1.7 210 wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 3.1 1.4 210 wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 3.1 1.4 210 wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 3.5 1.6 200 wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 3.0 1.4 200 wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 3.5 1.6 200 wit - -
array-examples/standard_copy1_false-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_copy2_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_copy3_false-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_copy4_false-unreach-call_ground.i unknown 3.4 1.6 200 wit - -
array-examples/standard_copy5_false-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_copy6_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_copy7_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_copy8_false-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_copy9_false-unreach-call_ground.i unknown 3.6 1.7 210 wit - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unknown 3.1 1.4 210 wit - -
array-examples/standard_init1_false-unreach-call_ground.i unknown 3.4 1.6 200 wit - -
array-examples/standard_init2_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_init3_false-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_init4_false-unreach-call_ground.i unknown 3.0 1.4 200 wit - -
array-examples/standard_init5_false-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_init6_false-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_init7_false-unreach-call_ground.i unknown 3.4 1.6 210 wit - -
array-examples/standard_init8_false-unreach-call_ground.i unknown 3.6 1.7 210 wit - -
array-examples/standard_init9_false-unreach-call_ground.i unknown 3.5 1.5 210 wit - -
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_partition_false-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_running_false-unreach-call.i unknown 2.9 1.3 210 wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i unknown 3.1 1.4 210 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 3.5 1.7 210 wit - -
array-examples/relax_true-unreach-call.i exception 4.4 1.9 230 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 3.6 1.6 200 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 900   870   850 wit - -
array-examples/sanfoundry_24_true-unreach-call.i unknown 3.4 1.6 200 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 3.3 1.5 210 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i unknown 3.5 1.6 200 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_compare_true-unreach-call_ground.i unknown 3.5 1.7 210 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i unknown 3.5 1.6 200 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i unknown 3.5 1.7 200 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i unknown 2.7 1.3 210 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i unknown 3.4 1.6 210 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i unknown 3.6 1.6 200 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i unknown 3.1 1.4 210 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_find_true-unreach-call_ground.i unknown 3.5 1.6 200 wit - -
array-examples/standard_init1_true-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_init2_true-unreach-call_ground.i unknown 2.9 1.4 210 wit - -
array-examples/standard_init3_true-unreach-call_ground.i unknown 3.2 1.4 210 wit - -
array-examples/standard_init4_true-unreach-call_ground.i unknown 3.5 1.5 210 wit - -
array-examples/standard_init5_true-unreach-call_ground.i unknown 3.4 1.6 210 wit - -
array-examples/standard_init6_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_init7_true-unreach-call_ground.i unknown 3.1 1.4 200 wit - -
array-examples/standard_init8_true-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_init9_true-unreach-call_ground.i unknown 3.4 1.6 210 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i unknown 2.8 1.4 200 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i unknown 3.6 1.6 200 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_partition_true-unreach-call_ground.i unknown 3.6 1.6 210 wit - -
array-examples/standard_password_true-unreach-call_ground.i unknown 3.6 1.6 200 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i unknown 3.0 1.4 210 wit - -
array-examples/standard_running_true-unreach-call.i unknown 3.5 1.6 210 wit - -
array-examples/standard_sentinel_true-unreach-call.i unknown 2.9 1.4 200 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i unknown 2.8 1.3 210 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i unknown 3.6 1.7 210 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i unknown 3.0 1.4 200 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 3.5 1.6 210 wit - -
array-examples/standard_two_index_01_true-unreach-call.i unknown 3.5 1.6 210 wit - -
array-examples/standard_two_index_02_true-unreach-call.i unknown 2.9 1.4 210 wit - -
array-examples/standard_two_index_03_true-unreach-call.i unknown 3.6 1.7 210 wit - -
array-examples/standard_two_index_04_true-unreach-call.i unknown 2.8 1.4 200 wit - -
array-examples/standard_two_index_05_true-unreach-call.i unknown 3.5 1.7 210 wit - -
array-examples/standard_two_index_06_true-unreach-call.i unknown 2.8 1.3 210 wit - -
array-examples/standard_two_index_07_true-unreach-call.i unknown 2.9 1.4 210 wit - -
array-examples/standard_two_index_08_true-unreach-call.i unknown 3.0 1.4 200 wit - -
array-examples/standard_two_index_09_true-unreach-call.i unknown 3.4 1.6 210 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i unknown 2.9 1.3 210 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i unknown 3.4 1.7 210 wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) 8.1 3.5 420 wit false(reach) 25 16 460 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 8.3 3.6 490 wit false(reach) 52 41 550 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 15   8.5 680 wit false(reach) 36 19 640 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 24   15   990 wit false(reach) 48 27 930 -
reducercommutativity/rangesum60_false-unreach-call.i false(reach) 46   37   1200 wit false(reach) 88 53 1500 -
reducercommutativity/rangesum_false-unreach-call.i timeout 900   870   980 wit - -
reducercommutativity/avg05_true-unreach-call.i timeout 900   900   2200 wit - -
reducercommutativity/avg10_true-unreach-call.i timeout 900   900   2000 wit - -
reducercommutativity/avg20_true-unreach-call.i timeout 900   900   2900 wit - -
reducercommutativity/avg40_true-unreach-call.i false(reach) 26   19   1000 wit - -
reducercommutativity/avg60_true-unreach-call.i false(reach) 52   45   1400 wit - -
reducercommutativity/avg_true-unreach-call.i out of memory 850   840   15000 wit - -
reducercommutativity/max05_true-unreach-call.i timeout 900   900   1000 wit - -
reducercommutativity/max10_true-unreach-call.i timeout 900   900   2400 wit - -
reducercommutativity/max20_true-unreach-call.i timeout 900   900   2100 wit - -
reducercommutativity/max40_true-unreach-call.i false(reach) 190   190   1000 wit - -
reducercommutativity/max60_true-unreach-call.i timeout 900   890   1500 wit - -
reducercommutativity/max_true-unreach-call.i timeout 900   870   3600 wit - -
reducercommutativity/sep05_true-unreach-call.i true 63   51   780 wit - -
reducercommutativity/sep10_true-unreach-call.i timeout 900   880   890 wit - -
reducercommutativity/sep20_true-unreach-call.i timeout 900   870   880 wit - -
reducercommutativity/sep40_true-unreach-call.i timeout 900   860   850 wit - -
reducercommutativity/sep60_true-unreach-call.i timeout 900   860   890 wit - -
reducercommutativity/sep_true-unreach-call.i timeout 900   870   890 wit - -
reducercommutativity/sum05_true-unreach-call.i timeout 900   900   1600 wit - -
reducercommutativity/sum10_true-unreach-call.i timeout 900   900   3300 wit - -
reducercommutativity/sum20_true-unreach-call.i timeout 900   900   3000 wit - -
reducercommutativity/sum40_true-unreach-call.i false(reach) 22   15   980 wit - -
reducercommutativity/sum60_true-unreach-call.i false(reach) 45   35   1300 wit - -
reducercommutativity/sum_true-unreach-call.i timeout 900   820   8300 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 19000 18000 84000 118 250   160   4100   118 0  
    correct results 6 170 120 4600 5 250   160   4100   0 0  
        correct true 1 63 51 780 0 0   0   0   0 0  
        correct false 5 100 67 3800 5 250   160   4100   0 0  
    incorrect results 5 340 300 5700 0 0   0   0   0 0  
        incorrect true 0
        incorrect false 5 340 300 5700 0 0   0   0   0 0  
score (118 tasks, max score: 202) -73
Run set sv-comp16.ArraysReach