Tool VeriAbs
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-14 09:46:18 CET [[ 2017-01-15 04:55:34 CET ]] [[ 2017-01-15 05:46:09 CET ]] [[ 2017-01-15 05:17:25 CET ]] [[ 2017-01-15 05:48:02 CET ]]
Run set sv-comp17.ReachSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.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 out of memory 0 wit inspect 43   40   530 15000 .037 0      error (invalid witness file) .56 .35 9.2 39 error (invalid witness file) 6.2 3.2 95 290 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 0 wit inspect 440   430   5700 15000 12     0      error (invalid witness file) .51 .32 6.9 39 error (invalid witness file) 5.8 3.1 110 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 0 wit inspect 430   430   4900 15000 8.1   0      error (invalid witness file) .50 .33 3.8 42 error (invalid witness file) 6.0 3.2 120 310 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 0 wit inspect 110   110   1100 15000 .074 0      error (invalid witness file) .47 .30 9.9 39 error (invalid witness file) 6.0 3.2 120 300 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 0 wit inspect 110   110   1200 15000 .074 0      error (invalid witness file) .48 .33 14   40 error (invalid witness file) 5.9 3.2 120 290 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 0 wit inspect 170   160   1900 15000 .090 0      error (invalid witness file) .48 .31 7.1 40 error (invalid witness file) 6.2 3.2 120 300 - -
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.5 2.3 44 220 .045 0      error (invalid witness file) .53 .34 13   40 error (invalid witness file) 5.7 3.0 80 300 - -
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.8 2.4 43 220 .045 0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.4 2.9 120 290 - -
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.0 2.5 46 220 .045 0      error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.6 3.1 98 290 - -
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.0 2.6 60 220 .045 0      error (invalid witness file) .53 .34 13   41 error (invalid witness file) 5.6 3.0 120 290 - -
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.2 2.8 48 230 .045 .098  error (invalid witness file) .49 .33 4.9 42 error (invalid witness file) 6.0 3.2 110 300 - -
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.3 3.0 49 220 .045 0      error (invalid witness file) .50 .33 10   41 error (invalid witness file) 6.0 3.1 110 300 - -
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.9 3.2 50 220 .045 0      error (invalid witness file) .48 .32 11   39 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.1 3.3 59 220 .045 0      error (invalid witness file) .55 .36 9.7 44 error (invalid witness file) 6.1 3.2 110 300 - -
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.1 3.6 60 220 .045 0      error (invalid witness file) .50 .33 8.8 43 error (invalid witness file) 6.7 3.6 130 310 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.0 2.5 46 220 .045 0      error (invalid witness file) .52 .33 9.2 39 error (invalid witness file) 6.1 3.2 110 300 - -
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.6 2.2 43 220 .045 0      error (invalid witness file) .54 .34 13   42 error (invalid witness file) 5.3 2.8 100 290 - -
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.6 2.3 49 220 .045 0      error (invalid witness file) .64 .43 7.6 41 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.6 2.4 44 230 .045 0      error (invalid witness file) .49 .31 9.4 41 error (invalid witness file) 5.8 3.1 82 300 - -
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.1 2.7 43 220 .045 0      error (invalid witness file) .49 .31 11   39 error (invalid witness file) 5.7 3.0 110 290 - -
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.3 2.8 48 220 .045 0      error (invalid witness file) .48 .31 8.8 39 error (invalid witness file) 7.1 3.7 130 320 - -
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.4 2.9 47 220 .045 0      error (invalid witness file) .51 .33 8.5 41 error (invalid witness file) 5.7 3.0 110 300 - -
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.6 3.1 49 220 .045 0      error (invalid witness file) .52 .34 3.7 40 error (invalid witness file) 6.7 3.5 130 310 - -
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.9 3.2 52 220 .045 .59   error (invalid witness file) .48 .32 9.4 40 error (invalid witness file) 5.7 3.0 110 290 - -
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.8 3.3 61 220 .045 0      error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.1 3.2 130 300 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 0 wit inspect 270   260   2800 1100 41     .098  error (invalid witness file) .52 .34 10   42 error (invalid witness file) 6.0 3.2 130 300 - -
array-examples/standard_partition_false-unreach-call_ground.i out of memory 0 wit inspect 35   30   450 15000 .078 0      error (invalid witness file) .50 .33 12   41 error (invalid witness file) 5.9 3.1 120 300 - -
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 99   94   1000 15000 .082 0      error (invalid witness file) .50 .33 7.1 40 error (invalid witness file) 5.7 3.1 110 300 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 43   40   560 15000 .037 0      - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.5 2.9 100 290
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i out of memory 0 wit inspect 41   39   510 15000 .037 0      - - error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 6.0 3.2 130 300
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 570   560   5300 13000 .37  0      - - error (invalid witness file) .49 .33 9.7 40 error (invalid witness file) 6.0 3.2 110 300
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 0 wit inspect 800   790   8200 6700 33     0      - - error (invalid witness file) .51 .35 8.0 40 error (invalid witness file) 6.9 3.7 140 320
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 wit inspect 650   310   7000 880 .17  0      - - out of memory 580    550    11000   7000 timeout 960   790   12000 3100
array-examples/sanfoundry_24_true-unreach-call.i true 2 wit inspect 650   300   6200 880 .17  0      - - error 3.8  2.1  66   280 true 10   5.6 160 340
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect 650   310   6900 920 .17  0      - - error 3.9  2.2  84   280 timeout 960   820   16000 4100
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 6.4 2.2 43 280 .041 0      - - true 3.7  2.0  67   270 true 8.0 4.2 130 320
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 0 wit inspect 370   370   4400 15000 25     0      - - error (invalid witness file) .51 .33 9.3 41 error (invalid witness file) 6.1 3.2 120 310
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 0 wit inspect 110   110   1100 15000 .074 0      - - error (invalid witness file) .49 .33 5.2 40 error (invalid witness file) 6.1 3.3 130 300
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect 650   310   6900 900 .17  .090  - - error 3.7  2.1  83   270 timeout 960   820   11000 3800
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect 640   300   6600 860 .17  0      - - error 3.8  2.1  63   270 timeout 960   800   11000 4600
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 640   300   7000 850 .17  0      - - error 3.7  2.1  82   270 timeout 960   800   19000 4400
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 650   300   6900 880 .17  0      - - error 3.8  2.1  79   270 timeout 960   840   19000 4500
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 680   340   7700 880 .17  0      - - error 3.9  2.2  77   270 timeout 960   860   12000 4700
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 670   330   6800 900 .17  0      - - error 4.8  2.7  47   270 timeout 960   860   21000 4700
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 680   330   7000 940 .17  .19   - - error 3.8  2.1  60   270 timeout 960   860   19000 4700
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 840   490   8900 980 .17  .090  - - error 3.7  2.1  32   270 timeout 960   870   13000 4700
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 890   540   9200 1000 .098 .082  - - error 4.1  2.3  78   270 timeout 960   870   15000 5100
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 900   540   8800 990 .098 .082  - - error 3.9  2.1  52   270 timeout 960   870   13000 4700
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 0 wit inspect 760   750   11000 15000 41     0      - - error (invalid witness file) .52 .32 7.3 42 error (invalid witness file) 5.8 3.1 99 300
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 670   330   8000 890 .17  0      - - error 3.9  2.1  81   270 timeout 960   860   20000 4900
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 660   310   6700 910 .17  .090  - - error 4.9  2.7  53   280 timeout 960   860   13000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 650   310   7200 890 .17  .19   - - error 3.8  2.1  84   270 timeout 960   860   18000 4800
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 650   310   6600 850 .17  0      - - error 3.9  2.1  82   280 timeout 960   840   20000 4200
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 650   300   6900 920 .17  .082  - - error 3.9  2.2  66   280 timeout 960   800   11000 4000
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 640   300   7100 860 .17  .082  - - error 4.7  2.6  47   270 timeout 960   790   17000 4100
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 640   300   6300 890 .17  0      - - error 3.7  2.1  70   270 timeout 960   830   11000 3800
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 650   300   7500 870 .17  .090  - - error 3.9  2.2  76   280 timeout 960   850   15000 4200
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 650   300   6500 890 .17  0      - - error 3.6  2.0  60   270 timeout 960   860   12000 4800
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 650   300   7100 930 .17  0      - - error 4.4  2.4  47   270 timeout 960   860   24000 4700
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 650   300   6100 960 .17  0      - - error 4.0  2.2  68   280 timeout 960   860   16000 4700
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 660   310   6500 940 .17  0      - - error 4.1  2.2  74   280 timeout 960   870   19000 4700
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 660   310   6800 1000 .17  .090  - - error 3.8  2.1  58   270 timeout 960   870   25000 4800
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 660   310   6800 1000 .098 0      - - error 4.2  2.3  84   290 timeout 960   860   12000 4900
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect 640   300   6800 900 .17  0      - - error 3.8  2.1  68   270 timeout 960   820   19000 3900
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect 640   300   5900 870 .17  0      - - error 4.2  2.3  77   290 timeout 960   820   11000 4100
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect 640   300   6000 840 .17  0      - - error 4.0  2.2  86   270 timeout 960   800   13000 4100
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 wit inspect 650   300   6700 960 .17  0      - - error 3.8  2.1  64   270 timeout 960   830   19000 4000
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 wit inspect 650   300   6700 900 .17  0      - - error 3.6  2.0  58   270 timeout 960   820   21000 3800
array-examples/standard_partition_true-unreach-call_ground.i true 2 wit inspect 650   300   6500 870 .17  0      - - error 4.0  2.3  67   270 timeout 960   860   12000 4800
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect 640   300   6800 860 .17  0      - - error 4.1  2.3  95   280 timeout 960   800   11000 4700
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect 640   300   7500 830 .17  .082  - - error 3.9  2.2  83   270 timeout 960   800   12000 4100
array-examples/standard_running_true-unreach-call.i true 2 wit inspect 640   300   6900 870 .17  0      - - error 4.0  2.2  82   280 timeout 960   850   20000 4700
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 640   300   6600 770 .17  .082  - - error 3.6  2.0  61   270 true 13   7.0 260 400
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 0 wit inspect 250   240   2500 15000 12     0      - - error (invalid witness file) .60 .39 7.6 39 error (invalid witness file) 8.5 4.5 100 300
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect 640   300   6800 880 .17  .082  - - error 3.6  2.0  33   280 timeout 960   810   11000 5200
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 0 wit inspect 240   240   1900 15000 23     0      - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 6.2 3.3 120 300
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 wit inspect 650   300   6700 920 .17  0      - - error 3.7  2.1  63   270 timeout 960   790   14000 3800
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect 640   300   7100 860 .17  0      - - error 3.8  2.1  66   270 timeout 960   830   11000 2900
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect 640   300   6700 850 .17  0      - - error 3.8  2.1  68   280 timeout 960   820   12000 3000
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect 640   300   6500 850 .17  .19   - - error 3.8  2.1  74   270 timeout 960   810   12000 2700
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect 640   300   7200 850 .17  .082  - - error 3.8  2.1  75   270 timeout 960   830   17000 2800
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect 650   300   7200 850 .17  0      - - error 3.8  2.1  75   280 timeout 960   830   13000 2700
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect 640   300   6000 860 .17  .090  - - error 3.7  2.1  83   270 timeout 960   830   12000 2800
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect 640   300   6400 870 .17  0      - - error 3.7  2.1  64   270 timeout 960   830   12000 2700
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect 640   300   6400 840 .17  0      - - error 3.7  2.1  75   270 timeout 960   820   23000 2900
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect 640   300   6700 840 .17  0      - - error 4.2  2.3  69   280 timeout 960   830   12000 2900
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 wit inspect 640   310   6300 850 .17  0      - - error 3.9  2.2  87   270 timeout 960   820   19000 2600
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 640   300   7400 830 .17  0      - - error 3.6  2.0  65   270 timeout 960   790   13000 4000
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i out of memory 0 wit inspect 250   240   2200 15000 12     0      error (invalid witness file) .51 .32 8.0 40 error (invalid witness file) 5.8 3.1 110 300 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   900   8500 14000 .29  0      error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.1 120 300 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 36   33   440 15000 .037 0      error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.7 3.0 110 290 - -
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 5.6 2.4 46 270 .045 0      error (invalid witness file) .50 .32 8.5 40 error (invalid witness file) 6.1 3.3 120 300 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i out of memory 0 wit inspect 36   33   470 15000 .037 0      error (invalid witness file) .55 .34 12   42 error (invalid witness file) 6.5 3.4 120 320 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i out of memory 0 wit inspect 50   45   550 15000 .078 0      error (invalid witness file) .55 .36 11   42 error (invalid witness file) 7.2 3.7 140 330 - -
array-industry-pattern/array_monotonic_true-unreach-call.i true 2 wit inspect 640   300   6400 870 .17  0      - - error 4.3  2.4  43   270 timeout 960   850   15000 3100
array-industry-pattern/array_mul_init_true-unreach-call.i out of memory 0 wit inspect 35   32   460 15000 .037 .098  - - error (invalid witness file) .50 .34 4.8 40 error (invalid witness file) 5.7 3.0 120 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect 640   300   6400 880 .17  .090  - - timeout 900    890    9400   5500 timeout 960   940   17000 4900
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i true 2 wit inspect 650   300   6900 880 .18  0      - - timeout 900    890    10000   3400 timeout 960   940   8900 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i true 2 wit inspect 650   300   6200 900 .18  .090  - - timeout 900    890    11000   5300 timeout 960   830   16000 4800
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i true 2 wit inspect 650   300   6500 870 .18  .090  - - timeout 900    890    6900   3400 timeout 960   940   14000 5300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 0 wit inspect 44   41   470 15000 .037 0      - - error (invalid witness file) .50 .32 9.0 40 error (invalid witness file) 5.9 3.1 110 300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i true 2 wit inspect 650   310   6800 870 .17  0      - - timeout 910    890    8900   6300 error 11   5.7 220 320
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect 640   300   6500 890 .18  .020  - - timeout 900    890    12000   4400 timeout 960   940   11000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 2 wit inspect 650   300   7100 910 .18  0      - - timeout 900    890    10000   3600 timeout 960   940   11000 5300
array-industry-pattern/array_shadowinit_true-unreach-call.i true 2 wit inspect 650   300   6800 890 .17  0      - - timeout 910    900    8500   6400 timeout 960   810   16000 2500
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 1 wit inspect 25   16   250 430 .11  .0041 false(unreach-call) 6.7  4.0  150   380 false(unreach-call) 17   11   340 480 - -
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 1 wit inspect 32   18   290 490 .11  0      false(unreach-call) 8.9  5.7  140   400 false(unreach-call) 17   9.4 300 580 - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 50   23   420 950 .20  .0041 false(unreach-call) 12    7.8  160   480 out of memory 88   55   1000 7000 - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 95   51   860 2200 .30  0      false(unreach-call) 14    8.3  220   670 out of memory 88   52   1100 7000 - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 190   140   2300 3700 .40  .10   false(unreach-call) 21    13    190   800 out of memory 67   42   560 7000 - -
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 1 wit inspect 150   140   1800 460 .19  0      false(unreach-call) 7.3  4.3  110   380 false(unreach-call) 12   6.1 220 410 - -
reducercommutativity/avg05_true-unreach-call.i out of memory 0 wit inspect 670   660   7300 15000 .18  0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 7.1 3.7 120 320
reducercommutativity/avg10_true-unreach-call.i out of memory 0 wit inspect 420   420   6100 15000 .22  0      - - error (invalid witness file) .48 .31 7.6 39 error (invalid witness file) 6.1 3.2 120 300
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   900   11000 500 .11  0      - - error (invalid witness file) .52 .36 12   41 error (invalid witness file) 6.1 3.2 120 300
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900   900   11000 500 .14  0      - - error (invalid witness file) .57 .37 11   40 error (invalid witness file) 5.6 3.0 100 300
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900   900   12000 500 .14  0      - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 6.2 3.3 130 300
reducercommutativity/avg_true-unreach-call.i out of memory 0 wit inspect 470   470   3300 15000 .21  0      - - error (invalid witness file) .55 .34 12   43 error (invalid witness file) 6.0 3.2 120 290
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 680   320   7900 1100 .21  .19   - - true 90    81    1300   830 timeout 960   900   27000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 790   440   8100 1000 .14  0      - - timeout 900    890    11000   1900 timeout 960   890   16000 2400
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   900   10000 520 .11  0      - - error (invalid witness file) .50 .32 9.0 39 error (invalid witness file) 6.1 3.2 100 300
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900   900   13000 520 .14  .098  - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.3 3.3 120 300
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   900   11000 530 .14  0      - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.0 3.2 120 300
reducercommutativity/max_true-unreach-call.i out of memory 0 wit inspect 270   270   3300 15000 .27  0      - - error (invalid witness file) .51 .33 4.2 39 error (invalid witness file) 6.3 3.3 120 310
reducercommutativity/sep05_true-unreach-call.i true 2 wit inspect 680   320   7300 1100 .23  0      - - true 130    120    1300   970 true 210   150   2600 2800
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 680   320   7800 1000 .16  0      - - timeout 900    890    12000   1300 out of memory 740   620   16000 7000
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 670   320   7400 1000 .18  0      - - timeout 900    890    8700   1200 out of memory 340   230   5900 7000
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect 690   340   7600 1100 .19  0      - - timeout 900    890    7000   1900 out of memory 760   610   12000 7000
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect 770   410   8900 1100 .16  .090  - - timeout 900    890    8900   3200 timeout 960   820   13000 5600
reducercommutativity/sep_true-unreach-call.i out of memory 0 wit inspect 270   260   3100 15000 .30  .098  - - error (invalid witness file) .49 .32 7.3 40 error (invalid witness file) 6.1 3.2 130 300
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 710   360   7800 990 .14  .090  - - timeout 900    900    13000   1100 true 33   20   660 730
reducercommutativity/sum10_true-unreach-call.i out of memory 0 wit inspect 420   420   4700 15000 .22  0      - - error (invalid witness file) .50 .32 8.0 39 error (invalid witness file) 6.5 3.4 120 310
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900   900   9600 490 .11  0      - - error (invalid witness file) .54 .36 12   42 error (invalid witness file) 5.8 3.2 130 300
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900   900   11000 490 .14  0      - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 5.8 3.1 110 300
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900   900   12000 490 .14  0      - - error (invalid witness file) .57 .37 7.6 44 error (invalid witness file) 6.0 3.2 120 300
reducercommutativity/sum_true-unreach-call.i out of memory 0 wit inspect 420   420   3900 15000 .33  0      - - error (invalid witness file) .49 .33 6.3 40 error (invalid witness file) 5.6 3.0 120 290
../../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 162 63000 39000 670000 530000 230   3.6  135 87 54 1300 4500   135 490 280 7400 33000   135 14000 13000 160000 73000   135 59000 51000 940000 280000  
    correct results 94 162 45000 22000 470000 74000 14   3.2  6 80 49 1200 3900   3 410 240 5800 28000   3 14000 13000 160000 72000   5 59000 51000 940000 270000  
        correct true 68 136 45000 22000 470000 61000 11   2.4  0 0 0 0 0   0 0 0 0 0   3 14000 13000 160000 72000   5 59000 51000 940000 270000  
        correct false 26 26 670 450 6900 13000 2.2 .80 6 80 49 1200 3900   3 410 240 5800 28000   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) 162
Run set sv-comp17.ReachSafety-Arrays