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