Tool ULTIMATE Automizer f7c3ed31
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-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.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   770   12000 5600 2.3 0      error (invalid witness file) .54 .35 12   41 error (invalid witness file) 6.4 3.4 130 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900   760   13000 2500 2.3 0      error (invalid witness file) .49 .32 12   40 error (invalid witness file) 5.8 3.0 91 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900   760   14000 2300 2.3 0      error (invalid witness file) .55 .36 7.1 42 error (invalid witness file) 5.7 3.1 110 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900   730   13000 2400 2.3 0      error (invalid witness file) .51 .33 8.4 39 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900   730   13000 3000 2.3 0      error (invalid witness file) .49 .32 7.1 39 error (invalid witness file) 5.5 2.9 93 290 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900   740   15000 5700 2.3 0      error (invalid witness file) .60 .37 7.9 42 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   730   14000 2300 2.3 0      error (invalid witness file) .62 .40 11   46 error (invalid witness file) 5.6 3.0 120 290 - -
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900   780   13000 3300 2.3 0      error (invalid witness file) .60 .39 9.6 43 error (invalid witness file) 6.0 3.2 99 310 - -
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900   800   12000 4200 2.3 0      error (invalid witness file) .63 .40 8.3 39 error (invalid witness file) 6.1 3.2 110 290 - -
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900   810   15000 4900 2.3 0      error (invalid witness file) .54 .36 11   39 error (invalid witness file) 5.7 3.0 100 300 - -
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5000 2.3 0      error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.9 3.7 58 290 - -
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 5100 2.3 0      error (invalid witness file) .64 .41 6.7 39 error (invalid witness file) 5.9 3.1 110 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5200 2.3 0      error (invalid witness file) .50 .32 10   39 error (invalid witness file) 7.1 3.7 130 320 - -
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900   810   12000 5100 2.3 0      error (invalid witness file) .48 .32 6.0 39 error (invalid witness file) 6.2 3.3 130 300 - -
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900   810   12000 5100 2.3 0      error (invalid witness file) .53 .34 10   39 error (invalid witness file) 6.2 3.3 95 300 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 4100 2.3 0      error (invalid witness file) .64 .40 6.1 40 error (invalid witness file) 5.7 3.1 130 290 - -
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   720   15000 2400 2.3 0      error (invalid witness file) .52 .36 7.3 41 error (invalid witness file) 5.9 3.1 130 300 - -
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900   770   13000 2500 2.3 0      error (invalid witness file) .54 .35 14   41 error (invalid witness file) 5.8 3.1 100 300 - -
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900   790   13000 2700 2.3 0      error (invalid witness file) .49 .33 7.2 42 error (invalid witness file) 5.7 3.1 110 290 - -
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 3500 2.3 0      error (invalid witness file) .51 .34 9.9 40 error (invalid witness file) 5.8 3.1 84 300 - -
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 3800 2.3 0      error (invalid witness file) .65 .41 7.5 40 error (invalid witness file) 5.8 3.0 74 290 - -
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 5100 2.3 0      error (invalid witness file) .51 .33 9.3 41 error (invalid witness file) 6.5 3.4 86 300 - -
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900   810   12000 5100 2.3 0      error (invalid witness file) .53 .33 12   42 error (invalid witness file) 6.7 3.5 120 290 - -
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 5100 2.3 0      error (invalid witness file) .50 .32 9.0 42 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900   800   11000 5300 2.3 0      error (invalid witness file) .58 .38 10   44 error (invalid witness file) 6.3 3.3 120 300 - -
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900   760   12000 2300 2.3 0      error (invalid witness file) .65 .43 6.2 41 error (invalid witness file) 5.8 3.1 120 300 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   800   12000 3000 2.3 0      error (invalid witness file) .53 .35 9.0 41 error (invalid witness file) 6.0 3.1 97 300 - -
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900   800   15000 3300 2.3 0      error (invalid witness file) .54 .34 12   40 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 7.1 2.2 57 340 2.6 0      - - error 4.9  2.7  84   280 true 8.9 4.8 150 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900   790   14000 5300 2.3 0      - - error (invalid witness file) .54 .33 11   40 error (invalid witness file) 5.7 3.0 110 300
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900   850   13000 1100 2.3 0      - - error (invalid witness file) .53 .34 8.9 39 error (invalid witness file) 6.4 3.4 120 300
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900   790   15000 2200 2.3 0      - - error (invalid witness file) .59 .39 8.7 39 error (invalid witness file) 6.4 3.4 110 300
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   840   12000 1400 2.3 0      - - error (invalid witness file) .63 .41 7.1 40 error (invalid witness file) 6.2 3.2 110 300
array-examples/sanfoundry_24_true-unreach-call.i true 2 wit inspect 8.0 2.3 67 370 2.5 0      - - error 4.3  2.3  60   280 true 9.5 5.1 120 350
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900   760   13000 2300 2.3 0      - - error (invalid witness file) .66 .40 8.1 39 error (invalid witness file) 6.0 3.2 110 300
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 5.6 1.8 43 320 2.5 0      - - true 3.6  2.0  80   270 true 7.4 4.0 140 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900   760   12000 2400 2.3 0      - - error (invalid witness file) .64 .40 8.4 42 error (invalid witness file) 6.4 3.3 110 310
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900   730   13000 3200 2.3 0      - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900   760   13000 2600 2.3 0      - - error (invalid witness file) .60 .39 11   42 error (invalid witness file) 5.5 2.9 89 290
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900   740   12000 2700 2.3 0      - - error (invalid witness file) .60 .38 8.9 40 error (invalid witness file) 5.7 3.0 93 290
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900   730   14000 3700 2.3 0      - - error (invalid witness file) .57 .37 12   45 error (invalid witness file) 6.0 3.2 130 290
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900   780   12000 3400 2.3 0      - - error (invalid witness file) .61 .38 7.7 41 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 3800 2.3 0      - - error (invalid witness file) .68 .44 8.1 42 error (invalid witness file) 5.9 3.1 120 300
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 4400 2.3 0      - - error (invalid witness file) .66 .42 8.5 39 error (invalid witness file) 7.2 3.7 130 310
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900   810   14000 4900 2.3 0      - - error (invalid witness file) .47 .30 8.9 39 error (invalid witness file) 6.0 3.2 91 300
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5100 2.3 0      - - error (invalid witness file) .51 .32 6.5 40 error (invalid witness file) 5.9 3.1 120 290
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900   810   14000 5200 2.3 0      - - error (invalid witness file) .68 .43 8.7 42 error (invalid witness file) 5.7 3.0 130 300
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900   810   12000 5000 2.3 0      - - error (invalid witness file) .58 .37 9.0 40 error (invalid witness file) 5.6 3.1 120 290
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900   810   13000 5100 2.3 0      - - error (invalid witness file) .68 .43 8.0 41 error (invalid witness file) 5.8 3.1 110 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900   800   12000 3500 2.3 0      - - error (invalid witness file) .59 .37 11   42 error (invalid witness file) 5.9 3.1 110 300
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900   810   12000 4400 2.3 0      - - error (invalid witness file) .59 .38 9.0 40 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900   800   11000 3300 2.3 0      - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.0 3.2 93 300
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900   780   13000 2900 2.3 0      - - error (invalid witness file) .59 .38 9.8 41 error (invalid witness file) 5.2 2.8 92 290
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   730   13000 2900 2.3 0      - - error (invalid witness file) .53 .34 10   40 error (invalid witness file) 6.5 3.4 120 310
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   730   12000 3400 2.3 0      - - error (invalid witness file) .55 .36 7.1 39 error (invalid witness file) 5.7 3.0 110 290
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900   770   13000 2400 2.3 0      - - error (invalid witness file) .59 .38 6.5 41 error (invalid witness file) 6.3 3.3 110 310
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900   790   11000 2800 2.3 0      - - error (invalid witness file) .59 .38 10   42 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900   790   13000 3700 2.3 0      - - error (invalid witness file) .57 .36 9.2 42 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 4100 2.3 0      - - error (invalid witness file) .62 .40 10   40 error (invalid witness file) 6.0 3.2 120 290
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5000 2.3 0      - - error (invalid witness file) .64 .40 6.8 40 error (invalid witness file) 6.7 3.6 100 300
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5000 2.3 0      - - error (invalid witness file) .57 .37 8.8 39 error (invalid witness file) 6.2 3.3 120 300
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900   800   13000 5300 2.3 0      - - error (invalid witness file) .51 .32 9.4 42 error (invalid witness file) 6.7 3.5 95 320
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900   810   14000 5100 2.3 0      - - error (invalid witness file) .62 .39 8.7 40 error (invalid witness file) 6.2 3.2 89 310
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   760   13000 2400 2.3 0      - - error (invalid witness file) .50 .34 12   41 error (invalid witness file) 6.6 3.5 140 310
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   760   12000 2200 2.3 0      - - error (invalid witness file) .62 .41 8.2 39 error (invalid witness file) 6.5 3.5 84 300
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900   740   13000 2600 2.3 0      - - error (invalid witness file) .64 .42 5.8 40 error (invalid witness file) 5.7 3.1 74 300
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900   760   14000 2700 2.3 0      - - error (invalid witness file) .65 .41 8.7 42 error (invalid witness file) 6.2 3.3 140 300
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900   760   12000 2300 2.3 0      - - error (invalid witness file) .53 .34 13   43 error (invalid witness file) 5.6 3.0 110 290
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900   800   14000 3100 2.3 0      - - error (invalid witness file) .68 .43 8.7 43 error (invalid witness file) 5.5 2.9 90 290
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900   740   13000 2700 2.3 0      - - error (invalid witness file) .69 .43 7.9 40 error (invalid witness file) 6.1 3.2 120 290
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900   730   14000 2600 2.3 0      - - error (invalid witness file) .59 .38 7.5 39 error (invalid witness file) 5.9 3.1 83 310
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900   800   13000 3100 2.3 0      - - error (invalid witness file) .62 .40 9.1 40 error (invalid witness file) 5.9 3.1 91 310
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 8.3 2.5 64 420 2.5 0      - - error 4.0  2.2  64   270 true 7.5 4.1 150 320
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   730   14000 2100 2.3 0      - - error (invalid witness file) .62 .39 8.2 39 error (invalid witness file) 5.4 2.9 98 290
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900   740   11000 5300 2.3 0      - - error (invalid witness file) .49 .32 6.7 40 error (invalid witness file) 5.8 3.1 130 300
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900   730   12000 2800 2.3 .0041 - - error (invalid witness file) .55 .35 9.0 39 error (invalid witness file) 5.7 3.1 110 290
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900   730   13000 2700 2.3 0      - - error (invalid witness file) .57 .37 12   42 error (invalid witness file) 5.8 3.1 120 300
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900   760   12000 1500 2.3 0      - - error (invalid witness file) .67 .41 7.8 41 error (invalid witness file) 5.6 3.0 100 290
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900   760   11000 1500 2.3 0      - - error (invalid witness file) .53 .35 10   40 error (invalid witness file) 6.5 3.4 120 310
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900   760   12000 1600 2.3 0      - - error (invalid witness file) .63 .39 10   40 error (invalid witness file) 5.8 3.1 84 300
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900   770   13000 1500 2.3 .0041 - - error (invalid witness file) .62 .39 4.8 41 error (invalid witness file) 6.1 3.2 110 300
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900   760   12000 1600 2.3 0      - - error (invalid witness file) .69 .43 9.0 41 error (invalid witness file) 5.9 3.1 89 300
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900   760   12000 1400 2.3 0      - - error (invalid witness file) .64 .41 8.6 42 error (invalid witness file) 5.6 3.0 60 300
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900   770   12000 1500 2.3 0      - - error (invalid witness file) .49 .33 8.9 39 error (invalid witness file) 6.2 3.3 120 310
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900   760   12000 1500 2.3 0      - - error (invalid witness file) .66 .42 7.6 40 error (invalid witness file) 6.0 3.2 110 310
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900   760   14000 1500 2.3 0      - - error (invalid witness file) .64 .41 8.4 39 error (invalid witness file) 6.0 3.2 120 300
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   750   13000 2900 2.3 0      - - error (invalid witness file) .69 .43 9.6 45 error (invalid witness file) 5.4 2.9 96 290
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900   730   12000 4400 2.3 0      - - error (invalid witness file) .65 .42 9.0 40 error (invalid witness file) 6.0 3.2 88 310
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   770   11000 1800 2.3 0      error (invalid witness file) .61 .39 8.1 43 error (invalid witness file) 6.1 3.2 120 300 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   860   9000 5200 2.3 0      error (invalid witness file) .57 .37 12   43 error (invalid witness file) 7.0 3.8 92 290 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900   790   11000 3100 2.3 0      error (invalid witness file) .53 .34 9.5 40 error (invalid witness file) 5.9 3.1 110 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900   850   8500 4900 2.3 0      error (invalid witness file) .56 .36 12   40 error (invalid witness file) 6.2 3.3 120 290 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout 0 wit inspect 900   800   12000 3200 2.3 0      error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.2 3.3 110 290 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   770   13000 4000 2.3 0      error (invalid witness file) .52 .34 13   42 error (invalid witness file) 6.5 3.4 110 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i timeout 0 wit inspect 900   790   12000 1700 2.3 0      - - error (invalid witness file) .60 .38 7.8 40 error (invalid witness file) 6.2 3.3 110 300
array-industry-pattern/array_mul_init_true-unreach-call.i timeout 0 wit inspect 900   780   14000 2400 2.3 0      - - error (invalid witness file) .63 .39 7.7 39 error (invalid witness file) 6.1 3.3 110 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   860   8400 4900 2.3 0      - - error (invalid witness file) .57 .37 10   39 error (invalid witness file) 5.7 3.0 72 300
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   870   8800 5400 2.3 0      - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 5.7 3.0 120 300
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   760   13000 4200 2.3 0      - - error (invalid witness file) .53 .34 13   39 error (invalid witness file) 6.2 3.3 120 310
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   880   8000 5500 2.3 0      - - error (invalid witness file) .63 .40 8.6 40 error (invalid witness file) 5.9 3.1 98 300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   870   8400 5200 2.3 0      - - error (invalid witness file) .59 .38 11   41 error (invalid witness file) 5.9 3.2 100 310
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i error 0 wit inspect 8.0 2.6 60 310 2.6 0      - - error (invalid witness file) .50 .32 5.8 40 error (invalid witness file) 5.8 3.1 120 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   880   7000 5500 2.3 0      - - error (invalid witness file) .59 .38 7.2 40 error (invalid witness file) 6.1 3.2 110 290
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   870   8600 5400 2.3 0      - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.7 3.0 94 300
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 0 wit inspect 900   750   14000 1700 2.3 0      - - error (invalid witness file) .56 .36 13   44 error (invalid witness file) 6.6 3.5 120 320
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 18   11   200 490 2.6 0      timeout 91    87    1200   680 false(unreach-call) 16   9.9 230 430 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 32   21   440 550 2.6 0      timeout 91    89    1200   410 false(unreach-call) 16   8.8 180 540 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 74   51   730 840 2.6 0      timeout 91    88    990   760 out of memory 76   49   570 7000 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 150   110   1600 2700 2.7 0      false(unreach-call) 13    8.0  150   640 timeout 94   57   650 7000 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 270   220   3100 4400 2.8 0      true 19    11    280   740 out of memory 80   50   580 7000 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 14   4.7 100 530 2.6 0      false(unreach-call) 9.1  6.0  120   400 false(unreach-call) 11   6.0 170 390 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect 210   190   2600 1200 2.6 0      - - exception 4.0  2.2  64   260 false(unreach-call) 7.3 3.9 150 320
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect 390   340   4500 1600 2.7 0      - - exception 5.0  2.7  61   270 false(unreach-call) 8.1 4.3 150 320
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   810   11000 3700 2.3 0      - - error (invalid witness file) .63 .39 8.2 40 error (invalid witness file) 5.8 3.1 95 300
reducercommutativity/avg40_true-unreach-call.i unknown 0 wit inspect 170   110   2000 4600 2.5 0      - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 130 290
reducercommutativity/avg60_true-unreach-call.i unknown 0 wit inspect 280   190   3700 4900 2.5 0      - - error (invalid witness file) .59 .37 12   43 error (invalid witness file) 5.8 3.1 100 300
reducercommutativity/avg_true-unreach-call.i timeout 0 wit inspect 900   850   13000 770 2.3 0      - - error (invalid witness file) .50 .32 5.8 40 error (invalid witness file) 6.1 3.2 120 290
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   850   11000 1200 2.3 0      - - error (invalid witness file) .51 .32 9.4 39 error (invalid witness file) 6.2 3.2 96 300
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   11000 2200 2.3 0      - - error (invalid witness file) .60 .39 9.6 39 error (invalid witness file) 5.5 3.0 72 300
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   750   13000 5300 2.3 0      - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.8 3.5 140 320
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900   740   12000 4800 2.3 0      - - error (invalid witness file) .49 .33 9.6 42 error (invalid witness file) 5.9 3.2 110 310
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   740   12000 5000 2.3 0      - - error (invalid witness file) .63 .40 8.0 39 error (invalid witness file) 5.9 3.1 110 300
reducercommutativity/max_true-unreach-call.i timeout 0 wit inspect 900   850   10000 2200 2.3 0      - - error (invalid witness file) .63 .40 9.6 43 error (invalid witness file) 7.3 3.8 110 320
reducercommutativity/sep05_true-unreach-call.i timeout 0 wit inspect 900   780   14000 4800 2.3 0      - - error (invalid witness file) .61 .39 10   40 error (invalid witness file) 6.8 3.5 120 310
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 910   680   9200 8700 2.3 0      - - error (invalid witness file) .65 .42 6.9 40 error (invalid witness file) 5.5 3.0 110 290
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 910   430   7000 13000 2.3 0      - - error (invalid witness file) .57 .37 11   43 error (invalid witness file) 5.7 3.1 90 310
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900   620   11000 9500 2.3 0      - - error (invalid witness file) .56 .35 10   40 error (invalid witness file) 5.5 3.0 96 310
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900   750   13000 6000 2.3 0      - - error (invalid witness file) .67 .42 9.0 40 error (invalid witness file) 5.0 2.7 88 290
reducercommutativity/sep_true-unreach-call.i timeout 0 wit inspect 900   780   11000 5100 2.3 0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 5.8 3.1 110 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 26   11   230 850 2.6 0      - - exception 3.5  2.0  73   260 false(unreach-call) 7.8 4.2 150 320
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect 77   42   750 1400 2.6 0      - - exception 4.7  2.6  48   270 false(unreach-call) 7.8 4.1 130 320
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900   820   6600 4800 2.3 0      - - error (invalid witness file) .53 .34 9.7 39 error (invalid witness file) 6.5 3.5 130 320
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900   760   12000 4600 2.3 0      - - error (invalid witness file) .63 .41 7.4 40 error (invalid witness file) 5.4 2.9 85 300
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900   740   8200 6400 2.3 0      - - error (invalid witness file) .49 .32 11   43 error (invalid witness file) 6.0 3.2 120 300
reducercommutativity/sum_true-unreach-call.i timeout 0 wit inspect 900   850   6300 4700 2.3 0      - - error (invalid witness file) .69 .43 9.8 43 error (invalid witness file) 5.8 3.1 110 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 22 110000 93000 1500000 470000 320 .0082 135 330 300 4200 5000   135 500 290 6100 32000   135 85 52 1300 5700   135 590 310 11000 29000  
    correct results 14 22 1300 1000 14000 16000 36 0      3 320 290 3900 3600   3 290 180 2400 22000   1 34 19 530 2200   8 64 35 1100 2600  
        correct true 8 16 730 590 8300 6600 21 0      1 0 0 0 0   0 0 0 0 0   1 34 19 530 2200   4 64 35 1100 2600  
        correct false 6 6 550 420 6200 9600 16 0      2 320 290 3900 3600   3 290 180 2400 22000   0 0 0 0 0   4 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) 22
Run set sv-comp17.ReachSafety-Arrays