Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i timeout 0 wit inspect 900 840 12000 4300 0      0    error 4.7 2.6 95 280 false(unreach-call) 7.8 4.2 110 320 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900 860 13000 1400 0      0    error 4.2 2.3 52 280 timeout 97   57   1300 1100 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900 860 14000 1400 0      0    error 4.3 2.4 86 290 timeout 97   62   2400 1500 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    error 4.9 2.7 110 280 timeout 96   58   1400 1100 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900 860 10000 2200 0      0    error 5.3 2.9 100 290 timeout 97   58   1100 1100 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 0      0    error 4.8 2.7 77 280 timeout 96   61   1500 1700 - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    error 4.1 2.3 81 270 timeout 97   61   1900 1600 - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 2200 0      0    error 4.1 2.3 83 280 timeout 97   60   1600 1800 - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2400 0      0    error 4.0 2.2 88 280 timeout 97   60   1300 2100 - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2400 0      0    error 4.6 2.5 76 270 timeout 97   60   2100 2700 - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2400 0      0    error 4.2 2.3 72 270 timeout 96   56   1300 1700 - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    error 4.7 2.6 75 280 timeout 96   57   1200 2500 - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 3500 0      0    error 4.9 2.7 72 280 timeout 97   63   1900 3700 - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    error 5.0 2.8 67 280 timeout 97   60   1600 3500 - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 3500 0      0    error 4.6 2.5 76 280 timeout 97   65   1900 4400 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 730 0      .15 error 4.2 2.3 84 290 timeout 96   61   1900 1300 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 740 0      0    error 4.0 2.2 65 280 timeout 97   59   970 1100 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 720 0      0    error 3.9 2.2 82 270 timeout 97   62   2000 1800 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 760 0      0    error 4.1 2.2 71 270 timeout 97   56   1100 1300 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 780 0      0    error 4.6 2.6 57 280 timeout 97   60   1700 2000 - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 730 0      0    error 4.3 2.3 88 270 timeout 97   60   1500 2500 - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 850 0      0    error 4.4 2.4 88 280 timeout 97   61   1000 2500 - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900 870 14000 800 0      0    error 4.2 2.3 47 280 timeout 96   58   1200 2300 - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 760 0      0    error 5.0 2.8 88 300 timeout 97   64   2100 3400 - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 760 0      0    error 4.6 2.5 90 280 timeout 97   62   2400 3800 - -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    error 4.5 2.5 62 280 false(unreach-call) 8.1 4.4 160 340 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    error 4.6 2.5 110 290 timeout 97   65   1200 1100 - -
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900 860 12000 2200 0      0    error 4.2 2.3 79 290 timeout 97   60   1300 1200 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 160 140 1900 2200 0      0    - - error 5.0  2.8  77   280 false(unreach-call) 7.7 4.2 130 330
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 3700 0      0    - - error 4.6  2.5  92   290 false(unreach-call) 7.7 4.1 110 320
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900 480 8000 4900 .053  0    - - timeout 900    870    26000   6000 timeout 960   900   21000 1400
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 4.7  2.6  85   300 false(unreach-call) 7.8 4.2 150 320
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900 600 11000 5700 0      0    - - timeout 900    890    27000   3900 false(unreach-call) 7.1 3.8 83 320
array-examples/sanfoundry_24_true-unreach-call.i timeout 0 wit inspect 900 860 13000 3900 .0082 0    - - error 4.7  2.6  54   270 timeout 960   820   16000 1900
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 4.0  2.2  81   270 false(unreach-call) 7.5 4.0 130 310
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 93 88 1200 2300 0      0    - - true 4.1  2.3  60   270 true 8.0 4.2 140 330
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    - - error 4.3  2.4  88   290 timeout 960   820   14000 3400
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 0      0    - - error 4.6  2.5  88   280 timeout 960   800   23000 4000
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    - - error 4.5  2.5  91   270 timeout 960   830   13000 4300
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2400 0      0    - - error 5.4  3.0  58   280 timeout 960   810   19000 4800
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900 870 14000 2400 0      0    - - error 3.9  2.2  58   270 timeout 960   810   17000 4300
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 0      0    - - error 4.2  2.3  83   270 timeout 960   840   14000 4800
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 2200 0      0    - - error 4.2  2.3  94   270 timeout 960   860   18000 4700
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 3500 0      0    - - error 4.2  2.3  92   270 timeout 960   870   14000 4700
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 5.0  2.7  63   280 timeout 960   870   24000 4700
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2400 0      0    - - error 4.5  2.5  66   280 timeout 960   870   23000 4800
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 2200 0      0    - - error 4.7  2.6  85   280 timeout 960   860   16000 4800
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900 860 14000 2200 0      0    - - error 4.7  2.6  98   280 timeout 960   870   17000 5200
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900 860 10000 2200 0      0    - - error 5.3  2.9  72   280 timeout 960   870   14000 5300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900 870 14000 690 0      0    - - error 3.9  2.2  76   280 timeout 960   870   14000 2500
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 780 0      0    - - error 4.5  2.5  78   270 timeout 960   870   15000 2300
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 780 0      0    - - error 4.3  2.4  78   280 timeout 960   860   18000 2500
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 750 0      0    - - error 3.8  2.1  86   270 timeout 960   860   15000 2600
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2400 0      0    - - error 4.1  2.2  82   280 timeout 960   800   25000 4500
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 820 0      0    - - error 4.0  2.2  67   270 timeout 960   800   18000 3900
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900 870 10000 690 0      0    - - error 4.8  2.7  58   270 timeout 960   840   17000 4000
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 710 0      0    - - error 5.3  2.9  51   280 timeout 960   850   15000 4800
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 900 0      0    - - error 4.3  2.4  80   270 timeout 960   860   21000 4700
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 720 0      0    - - error 4.4  2.4  98   280 timeout 960   860   14000 4700
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 770 0      0    - - error 4.6  2.5  91   290 timeout 960   860   12000 4800
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900 870 13000 730 0      0    - - error 4.3  2.4  69   270 timeout 960   860   18000 4700
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 740 0      0    - - error 4.5  2.5  76   280 timeout 960   860   15000 4800
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 740 0      0    - - error 4.4  2.4  84   280 timeout 960   860   14000 4900
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 0      0    - - error 4.9  2.7  70   290 false(unreach-call) 8.5 4.5 93 360
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900 860 14000 2200 0      0    - - error 4.0  2.2  71   280 false(unreach-call) 7.9 4.3 160 340
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 2200 0      0    - - error 4.1  2.3  78   280 timeout 960   810   15000 4400
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900 860 13000 1400 0      0    - - error 5.3  2.9  57   280 timeout 960   810   12000 2800
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 2200 0      0    - - error 4.4  2.4  89   290 timeout 960   770   12000 2600
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 2200 0      0    - - error 4.3  2.4  85   290 timeout 960   810   12000 2700
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900 860 9900 2200 0      0    - - error 5.1  2.8  67   290 timeout 960   810   16000 4700
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900 870 11000 2200 0      0    - - error 4.0  2.2  79   270 timeout 960   810   14000 4400
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 3.8  2.1  68   270 timeout 960   870   19000 2500
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900 860 13000 2400 .0082 0    - - error 4.4  2.4  60   280 timeout 960   830   16000 2100
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900 870 12000 800 0      0    - - error 5.3  2.8  59   280 timeout 960   800   22000 3800
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900 860 11000 3500 0      0    - - error 5.0  2.8  52   270 timeout 960   810   17000 5200
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900 860 9900 2400 0      0    - - error 4.0  2.2  75   270 timeout 960   800   17000 4200
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 5.1  2.8  65   280 timeout 960   800   23000 4200
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900 860 11000 2200 4.9    0    - - error 4.0  2.2  69   270 timeout 960   810   18000 2200
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900 870 12000 2200 0      0    - - error 5.1  2.8  55   290 timeout 960   810   16000 2300
array-examples/standard_two_index_03_true-unreach-call.i unknown 0 wit inspect 360 310 4100 3300 3.2    0    - - error 61    38    650   2800 error 16   10   320 380
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900 870 14000 2200 0      0    - - error 4.8  2.7  63   280 timeout 960   810   17000 2500
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900 870 13000 2400 0      0    - - error 3.8  2.1  57   270 timeout 960   810   11000 2200
array-examples/standard_two_index_06_true-unreach-call.i unknown 0 wit inspect 98 71 1200 4000 1.6    0    - - error 24    13    380   930 error 17   9.3 340 350
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900 870 14000 2200 0      0    - - error 4.1  2.3  84   270 timeout 960   810   14000 2300
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900 860 11000 2200 6.2    0    - - error 4.8  2.6  66   290 timeout 960   810   13000 2100
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900 860 11000 2100 5.5    0    - - error 4.1  2.3  66   280 timeout 960   810   14000 2100
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900 860 12000 2500 .0082 0    - - error 4.0  2.2  76   270 timeout 960   800   21000 2800
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900 860 12000 2200 0      0    - - error 3.8  2.1  53   270 timeout 960   800   17000 3800
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i timeout 0 wit inspect 900 870 14000 860 0      0    error 4.1 2.3 95 270 timeout 98   59   940 1100 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900 610 11000 4200 0      0    timeout 93   86   1400 1300 timeout 97   88   1400 4600 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900 860 9900 2200 0      0    error 4.3 2.4 79 290 timeout 97   61   1600 1700 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900 870 12000 750 0      0    error 4.0 2.2 74 280 timeout 97   89   1600 4500 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900 860 13000 2300 0      0    error 4.2 2.3 81 290 timeout 97   63   1700 2000 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900 590 9800 5900 0      0    timeout 94   75   1700 3800 false(unreach-call) 10   5.5 100 330 - -
array-industry-pattern/array_monotonic_true-unreach-call.i timeout 0 wit inspect 900 860 11000 1800 0      0    - - error 4.6  2.6  62   270 timeout 960   850   21000 3200
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 900 870 10000 810 0      0    - - error 4.1  2.3  79   270 false(unreach-call) 8.3 4.3 110 330
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900 610 8300 3000 0      0    - - timeout 900    890    17000   4900 timeout 960   940   16000 5000
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900 610 8200 3700 0      0    - - timeout 900    890    14000   3100 timeout 960   940   15000 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900 600 8400 4700 0      0    - - timeout 910    890    21000   5400 timeout 960   820   15000 2800
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900 610 7900 4100 0      0    - - timeout 900    890    19000   3800 timeout 960   940   15000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900 610 7800 4000 0      0    - - timeout 910    890    16000   5900 timeout 960   940   14000 5300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900 600 8300 4800 0      0    - - timeout 910    900    25000   6900 error 10   5.6 230 290
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900 610 8900 3700 0      0    - - timeout 900    890    18000   4100 timeout 960   940   9800 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900 610 7800 4400 0      0    - - timeout 900    890    22000   3800 timeout 960   940   11000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900 540 9200 3800 .0082 0    - - timeout 900    890    17000   5300 timeout 960   830   14000 2100
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 35 29 460 560 .041  0    false(unreach-call) 7.6 4.5 94 380 false(unreach-call) 36   23   450 560 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 110 100 1500 730 .061  0    false(unreach-call) 7.2 4.2 140 400 false(unreach-call) 49   33   580 1500 - -
reducercommutativity/rangesum20_false-unreach-call.i timeout 0 wit inspect 900 880 8800 5300 .082  0    timeout 93   86   2100 1800 false(unreach-call) 24   13   320 530 - -
reducercommutativity/rangesum40_false-unreach-call.i timeout 0 wit inspect 900 880 8400 4000 .16   0    timeout 92   86   1800 1600 false(unreach-call) 42   23   660 740 - -
reducercommutativity/rangesum60_false-unreach-call.i timeout 0 wit inspect 900 880 11000 4000 .23   0    timeout 92   86   3000 1600 false(unreach-call) 65   37   850 900 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 170 160 1800 2200 .0082 0    false(unreach-call) 5.7 3.4 110 370 false(unreach-call) 20   11   230 450 - -
reducercommutativity/avg05_true-unreach-call.i timeout 0 wit inspect 900 890 10000 1700 .033  0    - - timeout 900    900    22000   1800 true 360   320   5300 1000
reducercommutativity/avg10_true-unreach-call.i timeout 0 wit inspect 900 890 8900 3300 .049  0    - - timeout 900    890    22000   3500 timeout 960   890   20000 1500
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900 880 9300 4400 .090  0    - - timeout 900    890    19000   6500 timeout 960   860   12000 1900
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 910 880 9200 5900 .17   0    - - out of memory 510    500    9700   7000 timeout 960   830   17000 2300
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900 870 12000 4700 .25   0    - - out of memory 380    370    9100   7000 timeout 960   810   14000 4800
reducercommutativity/avg_true-unreach-call.i timeout 0 wit inspect 900 580 7200 4400 .0082 0    - - timeout 900    890    19000   2700 timeout 960   900   19000 1500
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 910 910 11000 1500 .041  0    - - error (invalid witness file) .56 .36 11   40 error (invalid witness file) 5.8 3.1 97 300
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880 8100 2600 .070  0    - - timeout 900    890    19000   1800 timeout 960   810   19000 2600
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900 880 8300 2800 .13   0    - - timeout 900    890    17000   1800 timeout 960   810   18000 2200
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900 870 9100 2500 .25   0    - - timeout 900    890    32000   2100 timeout 960   800   14000 3100
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900 860 9600 4000 .36   0    - - timeout 900    890    16000   3800 timeout 960   800   14000 3400
reducercommutativity/max_true-unreach-call.i segmentation fault 0 wit inspect 120 110 1300 2200 .0082 0    - - error (invalid witness file) .51 .32 4.6 41 error (invalid witness file) 5.7 3.0 68 300
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 840 790 10000 1500 .066  0    - - true 160    150    3800   1000 true 200   140   2000 2800
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900 530 8300 4800 .074  0    - - timeout 900    890    18000   1300 out of memory 840   720   12000 7000
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 900 600 8800 3700 0      0    - - timeout 900    890    14000   1200 out of memory 310   210   5000 7000
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900 600 8600 3900 0      0    - - timeout 900    890    15000   1800 out of memory 770   620   13000 7000
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900 590 9100 4300 0      0    - - timeout 900    890    19000   3300 timeout 960   820   12000 5300
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 900 600 9600 2700 0      0    - - timeout 900    890    16000   2300 out of memory 720   590   20000 7000
reducercommutativity/sum05_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890 13000 3800 .033  0    - - timeout 900    890    20000   1100 timeout 960   930   13000 5000
reducercommutativity/sum10_true-unreach-call.i timeout 0 wit inspect 900 890 10000 2000 .049  0    - - timeout 900    890    22000   2100 timeout 960   900   14000 4800
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 910 880 8600 6600 .090  0    - - timeout 900    890    16000   6800 timeout 960   860   13000 1800
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 910 870 11000 7400 .17   0    - - out of memory 440    420    7100   7000 timeout 960   840   18000 2200
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 910 860 10000 6500 .25   0    - - out of memory 450    430    7400   7000 timeout 960   830   13000 4800
reducercommutativity/sum_true-unreach-call.i timeout 0 wit inspect 900 580 9100 4300 .0082 0    - - timeout 900    890    23000   3900 false(unreach-call) 8.8 4.7 130 350
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 135 9 120000 110000 1400000 340000 24     .15 135 630 510 13000 20000   135 3300 2100 51000 74000   135 28000 27000 590000 150000   135 74000 65000 1200000 310000  
    correct results 6 9 1400 1300 17000 9600 .18  0    3 20 12 340 1200   3 100 67 1300 2500   2 170 150 3900 1600   3 220 150 2300 3500  
        correct true 3 6 1100 1000 14000 6100 .066 0    0 0 0 0 0   0 0 0 0 0   2 170 150 3900 1600   2 220 150 2300 3500  
        correct false 3 3 320 300 3700 3500 .11  0    3 20 12 340 1200   3 100 67 1300 2500   0 0 0 0 0   1 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (135 tasks, max score: 230) 9
Run set sv-comp17.ReachSafety-Arrays