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-57-generic; 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-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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   850   11000 4400 0     0     error 4.4  2.4  35   290 false(unreach-call) 8.0 4.3 140 330 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900   860   11000 2400 0     0     error 4.3  2.4  92   280 timeout 97   63   1100 1500 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2100 0     0     error 3.9  2.2  51   280 timeout 97   63   1300 1600 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900   860   12000 2300 0     0     error 4.6  2.5  57   290 timeout 97   59   850 1200 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900   850   13000 2100 0     0     error 4.5  2.5  77   280 timeout 97   57   1700 1000 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2100 0     0     error 4.1  2.3  90   280 timeout 97   66   1600 2200 - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2200 0     0     error 3.6  2.1  68   270 timeout 96   59   1300 1400 - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2200 0     0     error 4.1  2.3  84   270 timeout 97   62   1700 2000 - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     error 4.3  2.4  50   270 timeout 97   64   1000 2900 - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2300 0     0     error 4.0  2.2  85   270 timeout 96   65   1500 3900 - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2300 0     0     error 4.2  2.3  54   280 timeout 97   61   900 3200 - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2100 0     0     error 4.3  2.4  48   280 timeout 97   64   1400 4000 - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2000 0     0     error 4.4  2.4  95   280 timeout 97   63   1200 3800 - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2300 0     0     error 4.3  2.4  80   280 timeout 96   64   960 4500 - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900   860   15000 2100 0     0     error 4.5  2.4  54   280 timeout 96   66   1300 4500 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 1900 0     .79  error 4.4  2.4  94   290 timeout 97   63   1400 1300 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2100 0     0     error 3.7  2.0  28   270 timeout 97   63   1400 1600 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2100 0     8.9   error 3.9  2.1  44   280 timeout 97   62   910 2000 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2000 0     0     error 4.0  2.2  67   280 timeout 97   63   1200 2300 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     error 4.1  2.3  62   280 timeout 97   64   1400 2900 - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2300 0     0     error 4.3  2.3  77   280 timeout 97   61   1500 2700 - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 1900 0     0     error 4.1  2.3  78   280 timeout 97   62   1600 3300 - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 1800 0     0     error 4.3  2.4  53   280 timeout 97   62   950 3500 - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     error 4.4  2.4  71   280 timeout 97   59   1300 2500 - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2000 0     0     error 4.5  2.5  89   300 timeout 97   64   920 4100 - -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2300 0     0     error 3.9  2.2  45   270 false(unreach-call) 7.7 4.1 150 340 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2300 0     0     error 4.2  2.3  67   270 timeout 97   66   2100 1200 - -
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900   860   12000 2500 0     0     error 4.0  2.2  72   280 timeout 97   62   890 1200 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 3.9 1.2 26 280 0     .012 - - error 6.1  3.4  60   290 false(unreach-call) 7.4 4.0 140 320
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900   870   12000 4000 0     0     - - error 6.0  3.3  61   290 false(unreach-call) 7.8 4.1 150 330
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 950   480   9200 3800 0     0     - - timeout 910    880    23000   6200 timeout 960   910   18000 1400
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2200 0     .79  - - error 4.5  2.5  84   280 false(unreach-call) 7.3 4.0 130 320
array-examples/sanfoundry_10_true-unreach-call_ground.i segmentation fault 0 wit inspect 31   5.9 200 1200 0     .012 - - error (invalid witness file) .69 .44 7.1 41 error (invalid witness file) 5.7 3.0 99 290
array-examples/sanfoundry_24_true-unreach-call.i timeout 0 wit inspect 900   870   11000 3900 0     0     - - error 4.8  2.7  58   280 timeout 960   820   22000 1900
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2200 0     0     - - error 4.7  2.6  54   270 false(unreach-call) 7.3 3.9 150 300
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 2.9 1.0 24 270 0     0     - - true 3.7  2.1  70   270 true 8.2 4.4 98 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2400 0     0     - - error 4.1  2.3  82   280 timeout 960   820   16000 3600
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2100 0     0     - - error 5.7  3.1  70   280 timeout 960   790   16000 3900
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2300 0     0     - - error 5.5  3.1  56   280 timeout 960   820   19000 3700
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 3700 0     0     - - error 4.4  2.4  50   270 timeout 960   810   17000 4700
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2200 0     0     - - error 3.8  2.1  85   270 timeout 960   810   20000 4500
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 3700 0     0     - - error 5.0  2.8  54   270 timeout 960   840   19000 4800
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2200 0     3.1   - - error 4.5  2.5  64   280 timeout 960   850   25000 4700
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2300 0     0     - - error 5.3  2.9  52   270 timeout 960   860   20000 4700
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2200 0     .79  - - error 4.5  2.5  57   280 timeout 960   870   15000 4700
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2400 0     0     - - error 4.4  2.5  74   270 timeout 960   870   21000 4800
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 3700 0     1.6   - - error 5.5  3.0  56   280 timeout 960   870   20000 4800
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2500 0     0     - - error 5.4  2.9  61   270 timeout 960   870   24000 4700
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 1900 0     0     - - error 4.5  2.5  72   280 timeout 960   870   18000 4800
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2000 0     0     - - error 5.2  2.8  62   290 timeout 960   870   20000 2400
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2000 0     4.9   - - error 5.5  3.0  55   280 timeout 960   880   17000 2100
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 3700 0     0     - - error 4.0  2.2  64   270 timeout 960   860   26000 2400
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 1800 0     0     - - error 4.5  2.5  66   280 timeout 960   860   21000 2500
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 1900 0     0     - - error 4.0  2.2  56   280 timeout 960   810   20000 4700
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     - - error 3.8  2.1  62   270 timeout 960   790   12000 4600
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2200 0     0     - - error 4.0  2.2  75   270 timeout 960   840   17000 4500
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 1900 0     0     - - error 5.1  2.8  60   270 timeout 960   850   20000 4800
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2000 0     0     - - error 4.1  2.2  85   270 timeout 960   860   22000 4700
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     - - error 4.1  2.3  79   280 timeout 960   870   16000 4700
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2100 0     .79  - - error 4.6  2.5  60   280 timeout 960   870   28000 4800
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2000 0     0     - - error 5.1  2.8  79   290 timeout 960   860   18000 4800
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2300 0     0     - - error 5.9  3.2  58   290 timeout 960   860   20000 4800
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 3600 0     0     - - error 4.9  2.7  86   280 timeout 960   860   17000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2700 0     0     - - error 3.8  2.1  72   280 false(unreach-call) 7.8 4.2 150 330
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2500 0     0     - - error 4.4  2.5  59   270 false(unreach-call) 9.0 4.8 130 340
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900   860   13000 2100 0     0     - - error 4.0  2.2  77   270 timeout 960   810   23000 4400
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900   860   15000 2500 0     .79  - - error 4.7  2.6  69   270 timeout 960   810   21000 2800
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2600 0     0     - - error 4.6  2.5  68   280 timeout 960   760   13000 2800
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2500 0     0     - - error 5.1  2.8  71   290 timeout 960   810   20000 2900
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 2400 0     0     - - error 4.9  2.7  63   280 timeout 960   810   16000 4600
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900   860   11000 2200 0     0     - - error 4.1  2.3  64   270 timeout 960   810   19000 4500
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2600 0     0     - - error 5.1  2.8  57   280 timeout 960   870   20000 2500
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900   850   12000 3800 0     .025 - - error 4.4  2.5  57   270 timeout 960   830   18000 2100
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   860   14000 3700 0     0     - - error 4.1  2.3  60   270 timeout 960   800   22000 4100
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 3700 0     0     - - error 4.6  2.5  69   280 timeout 960   810   13000 5000
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2000 0     0     - - error 5.2  2.9  57   280 timeout 960   800   15000 3900
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2000 0     0     - - error 3.9  2.2  75   270 timeout 960   800   16000 3800
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900   860   13000 2100 0     0     - - error 4.0  2.2  82   280 timeout 960   810   19000 2200
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2300 0     0     - - error 3.9  2.2  78   270 timeout 960   810   21000 2200
array-examples/standard_two_index_03_true-unreach-call.i error 0 wit inspect 330   280   4700 2700 0     0     - - exception 8.0  4.9  110   290 error 15   9.6 230 370
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900   860   13000 2200 0     0     - - error 4.7  2.6  52   270 timeout 960   810   25000 2200
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900   860   11000 2500 0     0     - - error 4.8  2.6  57   270 timeout 960   810   21000 2200
array-examples/standard_two_index_06_true-unreach-call.i error 0 wit inspect 96   71   1100 3900 0     3.1   - - error 25    14    370   940 error 16   9.1 330 340
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900   860   11000 2000 0     0     - - error 4.9  2.7  43   270 timeout 960   810   17000 2300
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2300 0     .79  - - error 5.0  2.7  55   270 timeout 960   810   22000 2300
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2100 0     0     - - error 4.7  2.6  64   280 timeout 960   810   18000 2300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   860   12000 3000 0     0     - - error 4.2  2.3  73   270 timeout 960   800   18000 2900
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900   860   12000 2100 0     0     - - error 4.9  2.7  57   270 timeout 960   800   16000 3900
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   860   12000 1800 0     0     error 3.9  2.2  82   270 timeout 97   61   930 1300 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   290   7300 3800 0     0     timeout 92    85    1000   2300 timeout 97   89   1700 4600 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900   860   13000 2600 0     0     error 4.0  2.2  45   270 timeout 97   63   2100 2000 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900   860   11000 2200 0     0     error 3.9  2.2  64   270 timeout 97   90   2200 4500 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900   860   14000 2400 0     0     error 4.2  2.3  84   280 timeout 97   65   1500 2200 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 960   350   10000 4200 0     0     timeout 91    75    880   4100 false(unreach-call) 7.7 4.1 160 320 - -
array-industry-pattern/array_monotonic_true-unreach-call.i timeout 0 wit inspect 900   860   13000 2400 0     0     - - error 4.4  2.4  59   270 timeout 960   850   16000 3000
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 900   860   12000 2200 0     0     - - error 5.1  2.8  56   270 false(unreach-call) 7.4 3.9 140 320
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   290   6300 4300 0     0     - - timeout 900    890    17000   4900 timeout 960   940   13000 4700
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   290   5300 3500 0     0     - - timeout 900    890    29000   3200 timeout 960   940   16000 5300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   290   6400 5400 0     0     - - timeout 910    890    17000   5500 timeout 960   820   18000 2800
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   290   5200 3900 0     0     - - timeout 900    890    20000   4000 timeout 960   940   13000 5200
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   290   7100 4600 0     0     - - timeout 910    890    17000   5200 timeout 960   940   16000 5200
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   290   7200 6300 0     0     - - timeout 910    900    21000   6700 error 13   6.7 170 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   290   6700 4100 0     0     - - timeout 900    890    17000   3000 timeout 960   940   17000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   290   5000 5100 0     0     - - timeout 900    890    17000   3800 timeout 960   940   15000 5300
array-industry-pattern/array_shadowinit_true-unreach-call.i segmentation fault 0 wit inspect 340   100   2700 5000 0     0     - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.8 3.6 120 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 47   17   340 1200 .88  0     timeout 92    88    900   1800 false(unreach-call) 11   5.8 170 360 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 120   52   930 1800 5.1   0     timeout 92    87    860   2000 false(unreach-call) 12   6.4 170 390 - -
reducercommutativity/rangesum20_false-unreach-call.i segmentation fault 0 wit inspect 290   140   3100 2000 .041 .012 error (invalid witness file) .52 .34 9.1 43 error (invalid witness file) 5.5 2.9 110 290 - -
reducercommutativity/rangesum40_false-unreach-call.i timeout 0 wit inspect 950   490   11000 8100 .078 0     timeout 92    86    890   1600 false(unreach-call) 38   21   520 740 - -
reducercommutativity/rangesum60_false-unreach-call.i timeout 0 wit inspect 940   480   10000 8000 .11  0     timeout 92    86    1300   1600 false(unreach-call) 50   28   770 1000 - -
reducercommutativity/rangesum_false-unreach-call.i segmentation fault 0 wit inspect 260   80   2200 4600 0     .037 error (invalid witness file) .47 .30 6.7 40 error (invalid witness file) 6.4 3.3 130 300 - -
reducercommutativity/avg05_true-unreach-call.i timeout 0 wit inspect 910   450   5500 3200 .016 0     - - timeout 900    900    22000   1800 true 390   360   11000 1000
reducercommutativity/avg10_true-unreach-call.i timeout 0 wit inspect 910   450   7300 4000 .025 0     - - timeout 900    890    20000   3400 true 870   800   21000 1300
reducercommutativity/avg20_true-unreach-call.i segmentation fault 0 wit inspect 270   130   2700 2300 .045 0     - - error (invalid witness file) .63 .41 7.5 40 error (invalid witness file) 6.3 3.3 100 300
reducercommutativity/avg40_true-unreach-call.i segmentation fault 0 wit inspect 130   60   1200 1900 .086 0     - - error (invalid witness file) .61 .39 6.3 40 error (invalid witness file) 6.7 3.5 110 300
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 960   500   8400 3300 .12  0     - - out of memory 410    400    7100   7000 timeout 960   820   15000 4500
reducercommutativity/avg_true-unreach-call.i segmentation fault 0 wit inspect 95   27   760 2500 0     .012 - - error (invalid witness file) .64 .41 8.3 40 error (invalid witness file) 5.4 2.9 100 300
reducercommutativity/max05_true-unreach-call_true-termination.i segmentation fault 0 wit inspect 82   35   800 1500 .020 0     - - error (invalid witness file) .68 .43 7.4 39 error (invalid witness file) 6.7 3.5 130 310
reducercommutativity/max10_true-unreach-call_true-termination.i segmentation fault 0 wit inspect 56   22   460 1100 .033 0     - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 7.3 3.9 80 300
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   440   7300 3000 .066 0     - - timeout 900    890    20000   1800 timeout 960   810   12000 2300
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 910   450   9600 3700 .12  0     - - timeout 900    890    14000   2100 timeout 960   790   18000 3000
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 910   450   9900 2200 0     0     - - timeout 900    890    20000   3400 timeout 960   800   17000 3700
reducercommutativity/max_true-unreach-call.i segmentation fault 0 wit inspect 41   8.7 270 1400 0     .012 - - error (invalid witness file) .56 .37 13   42 error (invalid witness file) 6.1 3.2 110 300
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 57   15   440 2100 .012 0     - - true 180    170    2700   1000 true 220   150   3800 3300
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900   290   7300 4800 0     0     - - timeout 900    890    16000   1300 out of memory 780   660   19000 7000
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 910   300   7900 5000 0     0     - - timeout 900    890    13000   1200 out of memory 350   230   5800 7000
reducercommutativity/sep40_true-unreach-call.i segmentation fault 0 wit inspect 220   66   2000 3000 0     0     - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.2 3.3 97 310
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 910   300   8600 3500 0     0     - - timeout 900    890    17000   3300 timeout 960   830   21000 5500
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 960   350   9700 5300 0     0     - - timeout 900    890    18000   2300 out of memory 660   540   12000 7000
reducercommutativity/sum05_true-unreach-call_true-termination.i segmentation fault 0 wit inspect 16   4.1 120 610 .016 .012 - - error (invalid witness file) .55 .35 11   39 error (invalid witness file) 6.2 3.3 130 300
reducercommutativity/sum10_true-unreach-call.i timeout 0 wit inspect 910   440   8300 3100 .025 0     - - timeout 900    890    21000   2100 true 670   610   11000 1400
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 910   450   9300 2900 .045 0     - - timeout 900    890    18000   6800 timeout 960   870   21000 1900
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 960   490   9600 7600 .086 0     - - out of memory 410    400    7400   7000 timeout 960   840   16000 2300
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 910   450   8600 2900 .12  0     - - out of memory 450    440    10000   7000 timeout 960   820   17000 4600
reducercommutativity/sum_true-unreach-call.i segmentation fault 0 wit inspect 47   9.8 300 1500 0     0     - - error (invalid witness file) .53 .35 8.5 39 error (invalid witness file) 5.6 3.0 100 300
../../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 8 110000 87000 1300000 370000 7.1   26     135 690 580 8000 22000   135 3100 2100 44000 85000   135 20000 19000 410000 110000   135 68000 59000 1300000 280000  
    correct results 5 8 230 87 1800 5700 6.0   .012 0 180 180 1800 3800   2 22 12 350 750   2 190 180 2900 1600   3 230 160 4100 4000  
        correct true 3 6 64 18 490 2700 .012 .012 0 0 0 0 0   0 0 0 0 0   2 190 180 2900 1600   2 230 160 4100 4000  
        correct false 2 2 170 69 1300 3000 6.0   0     0 180 180 1800 3800   2 22 12 350 750   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) 8
Run set sv-comp17.ReachSafety-Arrays