Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 false(unreach-call) 1 wit inspect 2.5  2.7  28   300   .012 12      unknown 13    7.4  260   970 out of memory 89   60   1500 7000 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout (timeout) 0 wit inspect 900    900    9700   4200   .012 0      error (invalid witness file) .49 .31 12   39 error (invalid witness file) 5.8 3.0 87 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    9300   4200   .012 0      error (invalid witness file) .54 .34 13   40 error (invalid witness file) 5.8 3.1 110 300 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error 0 wit inspect 340    340    3500   71   .012 0      error (invalid witness file) .50 .32 13   40 error (invalid witness file) 5.7 3.0 70 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i error 0 wit inspect 340    340    3300   70   .012 0      error (invalid witness file) .62 .40 6.3 40 error (invalid witness file) 6.0 3.2 92 290 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.0  1.1  13   150   .012 8.1    unknown 3.2  1.8  64   260 true 7.6 4.1 110 330 - -
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.8  1.8  21   230   .012 0      unknown 3.3  1.8  49   270 true 7.9 4.2 100 310 - -
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 4.6  4.6  50   560   .012 0      unknown 23    13    440   1500 timeout 97   66   2100 6300 - -
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.9  5.9  64   840   .012 0      unknown 32    18    530   3100 timeout 97   69   1400 6200 - -
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.4  7.4  84   1100   .012 0      unknown 55    31    650   3000 timeout 98   65   1600 6600 - -
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 8.7  8.7  110   1400   .012 0      unknown 58    34    960   3600 timeout 96   66   1300 6000 - -
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 10    10    130   1700   .012 0      unknown 63    36    1300   4500 timeout 98   68   1300 6600 - -
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 11    11    170   1900   .012 0      timeout 90    52    1300   4700 timeout 98   66   1700 6700 - -
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 13    13    160   2200   .012 0      unknown 83    49    1500   5300 timeout 91   59   1600 7000 - -
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 14    14    160   2500   .012 0      timeout 95    56    1500   5700 timeout 97   65   1500 6700 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.6  2.6  35   560   .012 0      unknown 23    13    370   1600 timeout 97   69   1700 5900 - -
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 1.4  1.4  18   280   .012 0      unknown 13    7.1  310   940 timeout 98   68   1300 5900 - -
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 2.7  2.7  33   560   .012 .32   unknown 24    13    500   1500 timeout 98   70   1300 6100 - -
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 3.9  3.8  49   840   .012 0      unknown 33    19    570   3000 timeout 96   68   960 5800 - -
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.1  5.1  52   1100   .012 0      unknown 55    31    760   3100 timeout 98   66   1600 6600 - -
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.5  6.5  82   1400   .012 0      unknown 68    39    900   4000 timeout 97   67   1300 6000 - -
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.7  7.7  93   1700   .012 0      unknown 69    39    1200   4200 timeout 97   66   1200 6100 - -
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 8.5  8.5  97   1900   .012 0      unknown 84    48    1600   4900 timeout 98   68   2000 6900 - -
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 9.9  9.9  120   2200   .012 .32   timeout 98    56    880   4900 timeout 97   65   1500 6700 - -
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 11    11    130   2500   .012 0      timeout 97    56    2100   5600 timeout 94   60   1300 7000 - -
array-examples/standard_minInArray_false-unreach-call_ground.i error 0 wit inspect .50 .50 5.8 100   .012 0      error (invalid witness file) .56 .36 8.7 40 error (invalid witness file) 5.6 2.9 120 300 - -
array-examples/standard_partition_false-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    8900   12000   .012 0      error (invalid witness file) .58 .38 7.9 41 error (invalid witness file) 5.4 2.9 81 300 - -
array-examples/standard_running_false-unreach-call.i error 0 wit inspect 1.2  1.2  14   160   .012 0      error (invalid witness file) .54 .35 9.0 40 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect .16 .15 1.7 9.6 .012 0      - - error 4.2  2.3  69   280 true 9.4 5.1 170 350
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    10000   1300   .012 0      - - error (invalid witness file) .55 .35 9.1 41 error (invalid witness file) 6.7 3.6 81 300
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 150    150    1600   54   .074 0      - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.4 3.4 120 310
array-examples/sanfoundry_02_true-unreach-call_ground.i error 0 wit inspect 320    320    2300   120   .012 0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.1 3.3 110 300
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    10000   940   .012 0      - - error (invalid witness file) .48 .32 12   41 error (invalid witness file) 5.9 3.1 120 290
array-examples/sanfoundry_24_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    7900   6400   .012 0      - - error (invalid witness file) .52 .34 11   42 error (invalid witness file) 6.6 3.6 77 290
array-examples/sanfoundry_27_true-unreach-call_ground.i error 0 wit inspect .47 .47 5.8 97   .012 0      - - error (invalid witness file) .56 .36 7.1 41 error (invalid witness file) 7.0 3.7 71 300
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect .16 .16 1.5 9.3 .012 0      - - true 3.5  2.0  44   270 true 9.4 4.9 120 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    9200   4200   .012 0      - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.1 3.3 74 300
array-examples/sorting_selectionsort_true-unreach-call_ground.i error 0 wit inspect 330    330    3200   69   .012 0      - - error (invalid witness file) .59 .39 10   41 error (invalid witness file) 7.1 3.7 95 310
array-examples/standard_compareModified_true-unreach-call_ground.i error 0 wit inspect 100    100    680   170   .012 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.0 3.7 67 300
array-examples/standard_compare_true-unreach-call_ground.i error 0 wit inspect 100    100    780   170   .012 0      - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 7.4 3.9 100 310
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 1.1  1.1  16   100   .012 0      - - error 4.5  2.5  40   280 timeout 960   800   19000 3600
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 1.5  1.5  22   120   .012 0      - - error 3.6  2.0  65   270 timeout 960   840   20000 4400
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 1.8  1.8  21   140   .012 0      - - error 3.5  2.0  63   270 timeout 960   850   19000 4700
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 2.2  2.2  29   160   .012 0      - - error 3.7  2.1  54   270 timeout 960   850   21000 4700
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 2.5  2.5  34   180   .012 .32   - - error 4.5  2.5  50   270 timeout 960   870   19000 4700
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 2.8  2.8  35   200   .012 0      - - error 3.9  2.1  67   270 timeout 960   860   22000 4700
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 3.2  3.2  49   230   .012 0      - - error 4.0  2.2  90   270 timeout 960   870   33000 4700
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 3.5  3.5  47   250   .012 0      - - error 3.8  2.1  53   270 timeout 960   870   31000 4800
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect 3.9  3.9  50   270   .012 0      - - error 4.0  2.2  67   270 timeout 960   870   24000 5100
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 1.4  1.4  17   98   .012 0      - - error 4.6  2.5  51   290 timeout 960   850   21000 4500
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 1.8  1.8  29   120   .012 0      - - error 4.1  2.2  38   270 timeout 960   860   20000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 1.5  1.5  19   130   .012 0      - - error 3.5  2.0  61   270 timeout 960   850   23000 4800
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 1.1  1.1  14   79   .012 0      - - error 3.6  2.0  83   270 timeout 960   830   17000 3200
array-examples/standard_find_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    10000   88   .012 0      - - error (invalid witness file) .50 .31 7.5 42 error (invalid witness file) 7.7 4.1 74 290
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect .84 .95 13   67   .012 8.4    - - error 3.6  2.0  67   280 timeout 960   790   18000 3400
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 1.0  1.0  12   77   .012 0      - - error 4.4  2.5  53   270 timeout 960   830   18000 3700
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 1.2  1.2  17   93   .012 0      - - error 3.5  1.9  46   270 timeout 960   850   26000 4000
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 1.4  1.4  17   110   .012 0      - - error 3.6  2.0  34   270 timeout 960   840   16000 4800
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 1.6  1.6  20   130   .012 0      - - error 3.7  2.1  42   290 timeout 960   850   18000 4800
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 1.8  1.8  34   140   .012 0      - - error 4.1  2.3  53   290 timeout 960   860   13000 4700
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 2.1  2.1  28   160   .012 0      - - error 4.9  2.7  45   280 timeout 960   860   18000 4700
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 2.2  2.2  33   180   .012 0      - - error 3.9  2.2  53   280 timeout 960   860   19000 4700
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 2.5  2.5  37   200   .012 0      - - error 4.7  2.6  66   270 timeout 960   860   19000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i error 0 wit inspect .47 .47 5.8 98   .012 0      - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.0 3.2 100 300
array-examples/standard_minInArray_true-unreach-call_ground.i error 0 wit inspect .52 .51 6.9 100   .012 0      - - error (invalid witness file) .62 .38 8.7 40 error (invalid witness file) 5.8 3.1 88 290
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect .67 .67 9.9 57   .012 0      - - error 3.8  2.1  63   270 timeout 960   800   12000 4000
array-examples/standard_partial_init_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    8400   3900   .012 0      - - error (invalid witness file) .53 .33 10   41 error (invalid witness file) 6.7 3.5 91 300
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 0 wit inspect 16    16    170   15000   .012 0      - - error (invalid witness file) .59 .37 12   41 error (invalid witness file) 6.2 3.3 98 290
array-examples/standard_partition_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    10000   12000   .012 8.8    - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.8 3.1 130 300
array-examples/standard_password_true-unreach-call_ground.i error 0 wit inspect 94    94    610   170   .012 0      - - error (invalid witness file) .49 .31 9.3 41 error (invalid witness file) 6.9 3.6 91 300
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect 1.2  1.2  15   100   .012 0      - - error 4.6  2.6  53   270 timeout 960   790   14000 4100
array-examples/standard_running_true-unreach-call.i error 0 wit inspect 1.3  1.3  17   220   .012 0      - - error (invalid witness file) .50 .33 8.7 40 error (invalid witness file) 5.6 3.0 91 290
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9200   460   .012 0      - - error (invalid witness file) .53 .34 11   42 error (invalid witness file) 6.1 3.2 100 300
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect .93 .93 13   61   .012 0      - - error 4.1  2.3  45   270 timeout 960   790   12000 3800
array-examples/standard_strcmp_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    8700   670   .012 0      - - error (invalid witness file) .61 .40 9.1 41 error (invalid witness file) 6.5 3.5 110 300
array-examples/standard_strcpy_original_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    11000   89   .012 0      - - error (invalid witness file) .62 .38 7.4 41 error (invalid witness file) 6.0 3.2 100 310
array-examples/standard_strcpy_true-unreach-call_ground.i timeout (timeout) 0 wit inspect 900    900    12000   88   .012 0      - - error (invalid witness file) .59 .37 8.6 39 error (invalid witness file) 7.2 3.8 71 290
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect .24 .24 3.2 18   .012 0      - - error 4.0  2.2  66   290 timeout 960   810   15000 2600
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect .74 .74 8.6 58   .012 0      - - error 4.5  2.5  52   290 timeout 960   830   13000 3000
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect .20 .20 2.2 12   .012 0      - - error 3.9  2.2  58   280 timeout 960   810   15000 2500
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect .47 .47 6.4 35   .012 0      - - error 3.7  2.0  67   270 timeout 960   820   26000 2700
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect .36 .36 4.6 30   .012 0      - - error 3.4  1.9  66   270 timeout 960   810   22000 2100
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect .18 .18 1.7 11   .012 0      - - error 3.8  2.1  61   270 timeout 960   820   13000 2900
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect .30 .29 3.6 26   .012 0      - - error 4.1  2.3  66   290 timeout 960   820   22000 2800
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect .34 .34 3.7 24   .012 .45   - - error 4.3  2.4  49   280 timeout 960   820   18000 2800
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect .30 .30 4.1 23   .012 0      - - error 3.6  2.0  66   270 timeout 960   810   21000 2700
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   560   .012 0      - - error (invalid witness file) .55 .36 8.4 43 error (invalid witness file) 6.9 3.7 69 290
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 1.7  1.8  26   200   .012 7.9    - - error 3.9  2.2  75   280 timeout 960   780   13000 3600
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect 1.3  1.3  18   280   .012 0      unknown 13    7.3  280   940 timeout 96   65   2400 5900 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i false(unreach-call) 1 wit inspect 1.4  1.4  20   280   .012 0      timeout 97    83    3100   1700 timeout 97   86   1800 4800 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i timeout (timeout) 0 wit inspect 900    900    11000   130   .012 0      error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.1 3.2 82 300 - -
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 1.6  1.6  20   330   .012 0      unknown 18    9.9  320   1200 timeout 97   87   1600 4700 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i timeout (timeout) 0 wit inspect 900    900    11000   4200   .012 0      error (invalid witness file) .49 .31 9.3 40 error (invalid witness file) 7.0 3.7 72 290 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout (timeout) 0 wit inspect 900    900    9000   1300   .012 0      error (invalid witness file) .52 .33 11   42 error (invalid witness file) 6.7 3.5 92 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i out of memory 0 wit inspect 9.6  9.4  120   15000   .012 0      - - error (invalid witness file) .51 .34 5.1 40 error (invalid witness file) 6.2 3.3 95 290
array-industry-pattern/array_mul_init_true-unreach-call.i out of memory 0 wit inspect 15    15    190   15000   .012 0      - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 5.6 3.0 87 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect .81 .81 10   60   .012 0      - - timeout 900    890    15000   5300 timeout 960   940   22000 4800
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    9300   210   .016 0      - - error (invalid witness file) .51 .32 8.6 41 error (invalid witness file) 7.3 3.9 66 290
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i true 2 wit inspect 1.0  1.0  14   74   .012 0      - - timeout 900    890    12000   5800 timeout 960   830   26000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    9600   4100   .012 0      - - error (invalid witness file) .60 .38 9.6 40 error (invalid witness file) 7.2 3.8 86 290
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    12000   7200   .012 .0082 - - error (invalid witness file) .60 .39 9.7 41 error (invalid witness file) 7.3 3.8 110 310
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i true 2 wit inspect 3.0  3.0  41   180   .012 0      - - timeout 910    900    21000   6900 error 12   6.6 160 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect .97 .96 12   67   .012 0      - - timeout 900    890    8900   4300 timeout 960   940   18000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    8500   4300   .012 0      - - error (invalid witness file) .55 .36 11   41 error (invalid witness file) 6.3 3.3 110 300
array-industry-pattern/array_shadowinit_true-unreach-call.i unknown 0 wit inspect .17 .17 1.8 10   .012 0      - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 7.6 4.0 82 300
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .15 1.8 11   .012 0      true 3.8  2.1  63   270 true 9.2 4.9 85 310 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect .18 .18 1.6 11   .012 0      true 4.3  2.4  88   270 true 9.5 5.5 140 310 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect .23 .23 3.1 22   .012 0      true 5.1  2.8  93   280 true 8.3 4.4 160 330 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect .27 .27 2.7 25   .012 0      true 7.8  4.2  76   290 true 8.8 4.7 130 340 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect .30 .30 3.1 29   .012 0      true 7.3  3.9  150   310 true 9.4 5.0 140 320 - -
reducercommutativity/rangesum_false-unreach-call.i timeout (timeout) 0 wit inspect 900    900    7300   210   .012 0      error (invalid witness file) .62 .40 9.3 40 error (invalid witness file) 6.3 3.4 120 310 - -
reducercommutativity/avg05_true-unreach-call.i true 2 wit inspect .15 .15 1.8 9.3 .012 0      - - timeout 900    900    16000   1700 true 180   160   4200 1100
reducercommutativity/avg10_true-unreach-call.i true 2 wit inspect .17 .17 1.8 9.5 .012 0      - - timeout 900    890    11000   3400 true 320   270   7000 1500
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect .17 .17 1.6 9.5 .012 0      - - timeout 900    900    6800   6600 timeout 960   850   17000 3700
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect .17 .17 1.7 9.3 .012 0      - - out of memory 500    490    8200   7000 unknown 220   160   3900 4800
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect .19 .18 1.7 9.5 .012 0      - - out of memory 380    370    8200   7000 unknown 360   270   7600 5100
reducercommutativity/avg_true-unreach-call.i unknown 0 wit inspect .16 .16 1.7 9.9 .012 0      - - error (invalid witness file) .52 .32 12   41 error (invalid witness file) 5.9 3.1 120 300
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 1.6  1.6  18   12   .012 0      - - true 110    99    2100   830 timeout 960   910   16000 1200
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 52    52    530   34   .012 0      - - timeout 900    890    17000   1800 timeout 960   860   15000 2500
reducercommutativity/max20_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    10000   140   .012 0      - - error (invalid witness file) .61 .39 8.8 40 error (invalid witness file) 5.7 3.0 120 290
reducercommutativity/max40_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    11000   260   .012 0      - - error (invalid witness file) .56 .37 9.5 40 error (invalid witness file) 5.3 2.9 89 290
reducercommutativity/max60_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    11000   300   .012 0      - - error (invalid witness file) .62 .40 9.8 43 error (invalid witness file) 7.1 3.7 72 300
reducercommutativity/max_true-unreach-call.i unknown 0 wit inspect .18 .17 1.8 10   .012 0      - - error (invalid witness file) .67 .43 8.2 40 error (invalid witness file) 7.9 4.2 77 300
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect .18 .18 1.6 9.4 .012 0      - - true 130    120    3900   970 true 210   150   1900 3200
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect .16 .15 1.8 9.4 .012 0      - - timeout 900    890    12000   1300 out of memory 740   630   10000 7000
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect .16 .16 1.7 9.4 .012 0      - - timeout 900    890    12000   1300 out of memory 400   270   5800 7000
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect .18 .17 2.2 9.2 .012 0      - - timeout 900    890    17000   1800 timeout 910   740   19000 7000
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect .19 .18 1.9 9.4 .012 0      - - timeout 900    890    12000   3300 timeout 960   820   29000 5500
reducercommutativity/sep_true-unreach-call.i unknown 0 wit inspect .16 .16 2.0 10   .012 0      - - error (invalid witness file) .50 .33 9.7 41 error (invalid witness file) 5.7 3.0 110 290
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect .17 .17 1.6 9.3 .012 0      - - timeout 900    900    16000   1100 true 38   23   380 730
reducercommutativity/sum10_true-unreach-call.i true 2 wit inspect .28 .40 2.3 19   .012 8.8    - - timeout 900    890    17000   2000 true 92   60   1600 1300
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect .18 .18 1.9 9.4 .012 0      - - timeout 900    890    10000   6700 timeout 960   900   15000 5000
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect .17 .17 2.0 9.3 .012 0      - - out of memory 390    380    4500   7000 unknown 350   280   9300 4700
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect .27 .38 1.7 17   .012 7.6    - - out of memory 420    410    6800   7000 timeout 960   850   19000 6300
reducercommutativity/sum_true-unreach-call.i unknown 0 wit inspect .17 .16 2.1 10   .012 0      - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 7.5 4.0 74 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 145 25000 25000 280000 150000 1.7  63 135 1200 740 22000 72000   135 2200 1600 36000 140000   135 16000 15000 240000 95000   135 46000 40000 920000 230000  
    correct results 87 145 260 260 3100 31000 1.1  54 5 1200 740 22000 72000   7 2200 1500 35000 140000   3 16000 15000 240000 93000   7 46000 40000 920000 220000  
        correct true 58 116 110 110 1400 4500 .71 33 5 0 0 0 0   7 0 0 0 0   3 16000 15000 240000 93000   7 46000 40000 920000 220000  
        correct false 29 29 150 150 1800 27000 .36 20 0 1200 740 22000 72000   0 2200 1500 35000 140000   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) 145
Run set sv-comp17.ReachSafety-Arrays