Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 22:41:15 CET ]]
Run set sv-comp16.ArraysReach
Options [[ ../../results-verified/uautomizer.2016-01-14_2351.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   740   1700 wit - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 900   750   1400 wit - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 900   750   1400 wit - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 900   750   1900 wit - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 900   750   2100 wit - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 900   750   2100 wit - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 900   740   1300 wit - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 900   760   960 wit - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 900   780   1700 wit - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 900   780   1000 wit - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 900   780   1200 wit - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 900   790   2000 wit - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 900   790   1900 wit - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 900   790   1800 wit - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 900   790   2000 wit - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 900   770   1000 wit - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 900   750   1000 wit - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 900   760   1600 wit - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 900   770   1100 wit - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 900   780   1700 wit - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 900   780   1600 wit - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 900   790   2600 wit - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 900   780   1500 wit - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 900   780   1300 wit - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 900   790   1600 wit - -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 900   750   1100 wit - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 900   770   1500 wit - -
array-examples/standard_running_false-unreach-call.i timeout 900   780   1400 wit - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i true 12   3.8 340 wit - -
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 900   740   2100 wit - -
array-examples/relax_true-unreach-call.i timeout 900   780   1100 wit - -
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 900   770   1800 wit - -
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 900   710   1200 wit - -
array-examples/sanfoundry_24_true-unreach-call.i true 10   4.0 320 wit - -
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 900   750   1400 wit - -
array-examples/sanfoundry_43_true-unreach-call_ground.i true 8.3 2.4 330 wit - -
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 900   750   1600 wit - -
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 900   750   1700 wit - -
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 900   750   1400 wit - -
array-examples/standard_compare_true-unreach-call_ground.i timeout 900   740   1200 wit - -
array-examples/standard_copy1_true-unreach-call_ground.i timeout 900   750   2800 wit - -
array-examples/standard_copy2_true-unreach-call_ground.i timeout 900   770   2500 wit - -
array-examples/standard_copy3_true-unreach-call_ground.i timeout 900   780   900 wit - -
array-examples/standard_copy4_true-unreach-call_ground.i timeout 900   780   1200 wit - -
array-examples/standard_copy5_true-unreach-call_ground.i timeout 900   780   2600 wit - -
array-examples/standard_copy6_true-unreach-call_ground.i timeout 900   780   1300 wit - -
array-examples/standard_copy7_true-unreach-call_ground.i timeout 900   780   1400 wit - -
array-examples/standard_copy8_true-unreach-call_ground.i timeout 900   790   2900 wit - -
array-examples/standard_copy9_true-unreach-call_ground.i timeout 900   790   1600 wit - -
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 900   770   1400 wit - -
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 900   780   1800 wit - -
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 900   780   1600 wit - -
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 900   770   1400 wit - -
array-examples/standard_find_true-unreach-call_ground.i timeout 900   730   1200 wit - -
array-examples/standard_init1_true-unreach-call_ground.i timeout 900   740   1100 wit - -
array-examples/standard_init2_true-unreach-call_ground.i timeout 900   760   1300 wit - -
array-examples/standard_init3_true-unreach-call_ground.i timeout 900   770   1100 wit - -
array-examples/standard_init4_true-unreach-call_ground.i timeout 900   780   2000 wit - -
array-examples/standard_init5_true-unreach-call_ground.i timeout 900   780   1200 wit - -
array-examples/standard_init6_true-unreach-call_ground.i timeout 900   780   1100 wit - -
array-examples/standard_init7_true-unreach-call_ground.i timeout 900   780   1100 wit - -
array-examples/standard_init8_true-unreach-call_ground.i timeout 900   780   1200 wit - -
array-examples/standard_init9_true-unreach-call_ground.i timeout 900   790   1400 wit - -
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 900   750   1500 wit - -
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 900   750   1300 wit - -
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 900   740   1200 wit - -
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 900   750   1200 wit - -
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 900   760   2300 wit - -
array-examples/standard_partition_true-unreach-call_ground.i timeout 900   780   2500 wit - -
array-examples/standard_password_true-unreach-call_ground.i timeout 900   740   940 wit - -
array-examples/standard_reverse_true-unreach-call_ground.i timeout 900   750   1900 wit - -
array-examples/standard_running_true-unreach-call.i timeout 900   780   1300 wit - -
array-examples/standard_sentinel_true-unreach-call.i timeout 900   800   5200 wit - -
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 900   750   1100 wit - -
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 900   740   1600 wit - -
array-examples/standard_strcpy_original_true-unreach-call.i timeout 900   750   2000 wit - -
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 900   740   1500 wit - -
array-examples/standard_two_index_01_true-unreach-call.i timeout 900   750   1500 wit - -
array-examples/standard_two_index_02_true-unreach-call.i timeout 900   750   1300 wit - -
array-examples/standard_two_index_03_true-unreach-call.i timeout 900   750   1400 wit - -
array-examples/standard_two_index_04_true-unreach-call.i timeout 900   760   2300 wit - -
array-examples/standard_two_index_05_true-unreach-call.i timeout 900   750   1100 wit - -
array-examples/standard_two_index_06_true-unreach-call.i timeout 900   750   980 wit - -
array-examples/standard_two_index_07_true-unreach-call.i timeout 900   750   1200 wit - -
array-examples/standard_two_index_08_true-unreach-call.i timeout 900   760   1700 wit - -
array-examples/standard_two_index_09_true-unreach-call.i timeout 900   750   1200 wit - -
array-examples/standard_vararg_true-unreach-call_ground.i timeout 900   740   1500 wit - -
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 900   750   1500 wit - -
reducercommutativity/rangesum05_false-unreach-call.i false(reach) 13   4.1 330 wit false(reach) 22 12   420 -
reducercommutativity/rangesum10_false-unreach-call.i false(reach) 41   26   440 wit false(reach) 51 38   520 -
reducercommutativity/rangesum20_false-unreach-call.i false(reach) 40   14   680 wit false(reach) 33 17   560 -
reducercommutativity/rangesum40_false-unreach-call.i false(reach) 92   50   1400 wit false(reach) 47 27   670 -
reducercommutativity/rangesum60_false-unreach-call.i false(reach) 200   140   2000 wit false(reach) 68 45   890 -
reducercommutativity/rangesum_false-unreach-call.i false(reach) 18   5.9 480 wit false(reach) 18 9.9 400 -
reducercommutativity/avg05_true-unreach-call.i error 350   330   1400 wit - -
reducercommutativity/avg10_true-unreach-call.i error 420   380   2100 wit - -
reducercommutativity/avg20_true-unreach-call.i timeout 900   800   1600 wit - -
reducercommutativity/avg40_true-unreach-call.i timeout 900   730   2600 wit - -
reducercommutativity/avg60_true-unreach-call.i timeout 900   730   3300 wit - -
reducercommutativity/avg_true-unreach-call.i timeout 900   880   1000 wit - -
reducercommutativity/max05_true-unreach-call.i error 56   30   930 wit - -
reducercommutativity/max10_true-unreach-call.i error 120   77   1000 wit - -
reducercommutativity/max20_true-unreach-call.i error 860   720   2000 wit - -
reducercommutativity/max40_true-unreach-call.i timeout 900   750   2000 wit - -
reducercommutativity/max60_true-unreach-call.i timeout 900   750   2300 wit - -
reducercommutativity/max_true-unreach-call.i error 37   22   510 wit - -
reducercommutativity/sep05_true-unreach-call.i true 93   42   1500 wit - -
reducercommutativity/sep10_true-unreach-call.i timeout 900   450   7200 wit - -
reducercommutativity/sep20_true-unreach-call.i timeout 910   500   8400 wit - -
reducercommutativity/sep40_true-unreach-call.i timeout 900   510   8400 wit - -
reducercommutativity/sep60_true-unreach-call.i timeout 900   670   5400 wit - -
reducercommutativity/sep_true-unreach-call.i timeout 900   650   5900 wit - -
reducercommutativity/sum05_true-unreach-call.i true 32   18   460 wit - -
reducercommutativity/sum10_true-unreach-call.i true 78   57   1000 wit - -
reducercommutativity/sum20_true-unreach-call.i true 300   250   1800 wit - -
reducercommutativity/sum40_true-unreach-call.i timeout 900   740   1900 wit - -
reducercommutativity/sum60_true-unreach-call.i timeout 900   730   2200 wit - -
reducercommutativity/sum_true-unreach-call.i timeout 900   800   910 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 92000 77000 210000 118 240   150   3500   118 0  
    correct results 13 940 620 11000 6 240   150   3500   0 0  
        correct true 7 530 380 5700 0 0   0   0   0 0  
        correct false 6 410 240 5300 6 240   150   3500   0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (118 tasks, max score: 202) 20
Run set sv-comp16.ArraysReach