Tool SymDIVINE
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:13:29 CET [[ 2017-01-15 02:06:46 CET ]] [[ 2017-01-15 03:46:01 CET ]] [[ 2017-01-15 02:24:39 CET ]] [[ 2017-01-15 04:02:29 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options --fix_volatile --fix_inline --silent -Os [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.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)
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .074 .074 .56 9.8 .0082 0     false(unreach-call) 4.1  2.3  66   290 true 8.2 4.3 120 320 - -
loops/bubble_sort_false-unreach-call.i unknown 0 wit inspect .086 .086 .55 10   .029  0     error (invalid witness file) .51 .32 12   39 error (invalid witness file) 8.4 4.4 61 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .088 .088 .40 9.7 .0082 0     false(unreach-call) 4.3  2.4  45   280 true 8.0 4.2 150 340 - -
loops/eureka_01_false-unreach-call.i true -32 wit inspect 83     83     1000    580   .012  0     timeout 92    80    950   2100 false(unreach-call) 81   58   1400 1000 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .084 .084 .91 9.9 .0082 0     false(unreach-call) 4.0  2.2  64   290 true 8.0 4.3 110 310 - -
loops/insertion_sort_false-unreach-call_true-termination.i unknown 0 wit inspect .057 .057 .43 9.7 .012  0     error (invalid witness file) .63 .41 7.8 40 error (invalid witness file) 5.8 3.1 120 300 - -
loops/invert_string_false-unreach-call_true-termination.i unknown 0 wit inspect .072 .072 .45 9.5 .0082 0     error (invalid witness file) .54 .33 13   39 error (invalid witness file) 6.6 3.5 84 290 - -
loops/linear_search_false-unreach-call.i unknown 0 wit inspect .052 .052 .53 9.8 .0082 0     error (invalid witness file) .56 .37 6.9 39 error (invalid witness file) 7.2 3.8 110 300 - -
loops/ludcmp_false-unreach-call.i unknown 0 wit inspect .064 .064 .53 9.9 .016  0     error (invalid witness file) .54 .35 8.5 40 error (invalid witness file) 6.0 3.1 120 300 - -
loops/matrix_false-unreach-call_true-termination.i unknown 0 wit inspect .054 .054 .50 9.8 .012  0     error (invalid witness file) .48 .30 11   41 error (invalid witness file) 6.4 3.4 99 300 - -
loops/n.c24_false-unreach-call.i unknown 0 wit inspect 7.8   7.8   82    360   .012  4.1   error (invalid witness file) .49 .31 9.2 39 error (invalid witness file) 7.0 3.7 83 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .086 .086 .47 9.8 .0082 0     false(unreach-call) 4.7  2.6  59   280 true 7.8 4.1 120 320 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .060 .060 .46 9.5 .0082 0     false(unreach-call) 4.0  2.3  69   280 true 8.7 4.6 100 320 - -
loops/s3_false-unreach-call.i unknown 0 wit inspect .066 .066 .60 11   .049  0     error (invalid witness file) .62 .40 8.2 39 error (invalid witness file) 6.0 3.2 120 300 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18  .18  1.8  9.8 .012  0     false(unreach-call) 6.6  3.7  65   290 true 7.5 4.0 110 320 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16  .17  1.6  12   .0082 4.0   false(unreach-call) 5.9  3.2  63   290 true 7.8 4.1 120 310 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15  .16  1.3  12   .0082 4.1   false(unreach-call) 5.8  3.2  66   280 true 6.6 3.6 120 310 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  .22  2.7  12   .0082 4.0   false(unreach-call) 9.3  5.0  88   330 true 7.4 4.0 120 320 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .096 .11  .51 11   .0082 5.4   false(unreach-call) 4.8  2.6  65   280 true 7.1 3.7 100 320 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .086 .10  .58 11   .0082 5.3   false(unreach-call) 4.6  2.6  43   270 true 8.0 4.4 92 310 - -
loops/sum_array_false-unreach-call.i unknown 0 wit inspect .079 .081 .46 9.8 .012  0     error (invalid witness file) .57 .37 7.1 40 error (invalid witness file) 6.0 3.2 120 290 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .064 .065 .45 9.8 .0082 0     false(unreach-call) 3.5  2.0  59   270 true 7.0 3.8 140 310 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .092 .11  .92 12   .0082 4.3   false(unreach-call) 4.0  2.2  54   280 true 9.7 5.1 100 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12  .12  1.7  9.9 .0082 0     false(unreach-call) 4.3  2.4  49   280 true 7.5 4.0 80 310 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .084 .086 .55 10   .0082 0     false(unreach-call) 3.7  2.1  58   270 true 7.6 4.0 130 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .077 .077 .74 9.7 .0082 0     false(unreach-call) 3.7  2.1  40   270 true 8.1 4.3 100 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17  .17  1.9  9.8 .012  0     false(unreach-call) 4.0  2.2  54   270 true 7.3 3.9 150 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .087 .087 .49 9.8 .0082 0     false(unreach-call) 3.7  2.0  52   280 true 7.3 3.9 150 310 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 wit inspect .11  .11  1.2  10   .012  0     error (invalid witness file) .55 .36 11   42 error (invalid witness file) 6.6 3.5 99 310 - -
loops/vogal_false-unreach-call.i true -32 wit inspect 6.1   6.0   84    63   .012  0     unknown 40    28    430   990 timeout 96   70   1800 1000 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .057 .057 .46 9.6 .0082 0     false(unreach-call) 4.5  2.5  60   290 true 8.3 4.4 110 310 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .074 .074 .44 9.8 .0082 0     - - true 4.5  2.6  60   290 true 9.3 5.0 160 350
loops/bubble_sort_true-unreach-call.i unknown 0 wit inspect .058 .058 .54 9.9 .016  0     - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.9 3.1 110 300
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect .053 .054 .51 9.8 .0082 0     - - out of memory 310    300    3100   7000 true 64   57   750 420
loops/eureka_01_true-unreach-call.i true 1 wit inspect .25  .25  2.5  32   .012  0     - - out of memory 730    700    12000   7000 timeout 960   850   13000 4600
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .063 .066 .69 9.8 .0082 .82  - - true 450    440    12000   5100 true 32   19   340 730
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .077 .077 .63 9.4 .0082 .098 - - true 4.6  2.6  61   280 true 6.9 3.8 140 320
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .054 .054 .49 9.7 .0082 0     - - true 4.3  2.4  72   280 true 7.3 3.9 100 320
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect .080 .080 .47 9.9 .0082 0     - - error (invalid witness file) .61 .39 7.9 39 error (invalid witness file) 5.9 3.1 120 290
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .083 .083 .76 9.9 .0082 0     - - true 22    14    310   540 true 45   31   470 730
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect .052 .052 .51 9.4 .0082 0     - - error (invalid witness file) .68 .42 8.6 40 error (invalid witness file) 6.3 3.3 120 300
loops/lu.cmp_true-unreach-call.i unknown 0 wit inspect .064 .064 .48 10   .016  0     - - error (invalid witness file) .49 .32 8.8 39 error (invalid witness file) 5.9 3.1 78 300
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .053 .055 .48 9.7 .0082 0     - - true 7.8  5.7  68   440 true 14   7.3 220 380
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect .096 .096 .79 9.5 .0082 0     - - out of memory 230    230    3100   7000 true 11   5.8 200 390
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .14  .18  1.5  19   .0082 9.7   - - true 4.9  2.7  53   270 true 160   150   2300 870
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .14  .14  1.2  9.8 .0082 0     - - true 3.9  2.2  69   270 true 180   170   4100 730
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 8.2   8.1   110    30   .012  .34  - - true 6.4  3.5  100   290 true 9.7 5.3 180 340
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect .16  .18  .87 12   .0082 4.0   - - timeout 900    900    27000   3500 true 12   6.3 170 410
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect .057 .059 .53 9.9 .0082 .033 - - true 5.3  2.9  52   280 true 8.0 4.3 130 320
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .053 .053 .47 9.9 .0082 0     - - true 4.6  2.5  79   280 true 12   6.4 180 410
loops/sum_array_true-unreach-call.i unknown 0 wit inspect .081 .081 .47 9.9 .012  0     - - error (invalid witness file) .50 .32 8.5 39 error (invalid witness file) 6.8 3.6 130 320
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .15  .15  2.1  9.9 .0082 0     - - true 5.0  2.8  58   280 true 7.4 4.0 120 320
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1200   .0082 9.9   - - error (invalid witness file) .60 .39 11   40 error (invalid witness file) 5.7 3.1 100 290
loops/trex01_true-unreach-call_true-termination.i unknown 0 wit inspect .40  .40  5.4  9.9 .012  0     - - error (invalid witness file) .52 .33 11   43 error (invalid witness file) 6.3 3.4 130 310
loops/trex02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9900    3200   .0082 0     - - error (invalid witness file) .47 .31 8.2 41 error (invalid witness file) 5.9 3.2 110 300
loops/trex03_true-unreach-call_true-termination.i unknown 0 wit inspect .28  .28  2.9  9.6 .012  0     - - error (invalid witness file) .70 .44 7.5 39 error (invalid witness file) 5.9 3.2 110 300
loops/trex04_true-unreach-call_false-termination.i unknown 0 wit inspect .085 .084 .67 9.9 .0082 0     - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 5.2 2.8 98 280
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .052 .052 .49 9.8 .0082 0     - - out of memory 280    280    6200   7000 true 10   5.5 150 360
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i unknown 0 wit inspect .14  .14  1.3  9.7 .012  0     - - error (invalid witness file) .48 .31 9.9 39 error (invalid witness file) 6.2 3.2 110 300
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .15  .15  1.2  9.8 .0082 0     - - true 4.6  2.6  99   280 true 9.9 5.3 110 330
loops/vogal_true-unreach-call.i true 2 wit inspect .48  .48  5.5  9.7 .012  0     - - true 51    41    1300   1100 true 190   150   1900 3200
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .053 .054 .44 9.9 .0082 0     - - true 3.7  2.1  69   280 true 7.6 4.0 150 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .065 .066 .46 9.9 .0082 0     - - true 4.7  2.7  52   280 true 7.7 4.1 150 310
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect .098 .12  .47 11   .0082 5.7   - - true 3.7  2.1  51   280 true 7.8 4.2 140 320
loop-acceleration/array_false-unreach-call1_true-termination.i unknown 0 wit inspect .074 .074 .47 9.9 .0082 0     error (invalid witness file) .56 .36 12   44 error (invalid witness file) 6.6 3.5 99 300 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect .058 .058 .50 9.9 .0082 0     out of memory 45    37    430   7000 true 9.0 4.8 86 310 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 130     130     1800    820   .0082 0     timeout 96    84    1200   2700 true 7.1 3.8 150 320 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect .11  .11  .97 9.7 .0082 0     false(unreach-call) 25    15    350   1100 true 6.4 3.4 120 310 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 27     27     380    150   .0082 16     false(unreach-call) 63    51    930   1000 true 8.7 4.7 89 320 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 120     120     1400    15000   .0082 0     error (invalid witness file) .59 .37 8.7 41 error (invalid witness file) 5.5 3.0 100 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .078 .080 .53 9.6 .0082 0     false(unreach-call) 4.6  2.6  49   280 true 6.8 3.6 120 310 - -
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 0 wit inspect .050 .051 .56 9.8 .0082 0     timeout 98    84    2300   2300 true 7.8 4.1 140 330 - -
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 160     160     1700    15000   .0082 4.7   error (invalid witness file) .48 .31 10   40 error (invalid witness file) 6.1 3.2 89 290 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .086 .087 .93 9.9 .0082 0     false(unreach-call) 3.6  2.0  45   270 true 6.9 3.7 110 320 - -
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 0 wit inspect .079 .079 .46 9.8 .0082 0     timeout 96    84    1700   1900 true 8.0 4.3 110 310 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .081 .083 .40 9.9 .0082 0     false(unreach-call) 3.5  2.0  67   280 true 6.8 3.6 120 310 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .062 .094 .72 16   .0082 10     false(unreach-call) 3.4  2.0  45   280 true 8.6 4.5 93 320 - -
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 0 wit inspect .078 .078 .52 9.5 .0082 0     timeout 97    82    1200   1900 true 8.1 4.3 74 310 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .085 .11  .54 10   .0082 5.3   false(unreach-call) 3.9  2.2  62   280 true 8.3 4.4 96 320 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .052 .053 .44 9.9 .0082 0     false(unreach-call) 3.8  2.1  63   270 true 6.6 3.5 140 310 - -
loop-acceleration/array_true-unreach-call1_true-termination.i unknown 0 wit inspect .059 .059 .56 9.9 .0082 0     - - error (invalid witness file) .50 .33 12   42 error (invalid witness file) 6.0 3.2 120 300
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect .057 .057 .44 9.9 .0082 0     - - out of memory 280    270    5900   7000 timeout 960   800   17000 4400
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 370     370     4800    1700   .0082 0     - - timeout 910    890    15000   5900 timeout 960   850   14000 2800
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 360     360     4700    1700   .0082 0     - - out of memory 320    300    7100   7000 timeout 960   850   12000 2900
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .088 .088 .81 9.9 .0082 0     - - true 4.9  2.7  58   270 timeout 960   810   14000 2400
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 180     180     2400    1600   .0082 9.9   - - true 17    13    340   530 true 590   510   6500 1400
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .21  .21  2.6  10   .0082 .13  - - true 7.3  4.2  100   330 true 37   25   400 650
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 110     110     1400    15000   .0082 4.0   - - error (invalid witness file) .63 .40 10   40 error (invalid witness file) 6.2 3.3 110 300
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect .061 .061 .44 9.7 .0082 0     - - out of memory 410    400    7300   7000 true 8.4 4.4 150 320
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect .050 .051 .52 9.9 .0082 0     - - true 5.4  3.0  79   290 timeout 960   830   12000 4700
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect .053 .053 .56 9.9 .0082 0     - - out of memory 410    410    9200   7000 timeout 960   810   13000 2600
loop-acceleration/phases_true-unreach-call1.i out of memory 0 wit inspect 160     160     2200    15000   .0082 0     - - error (invalid witness file) .59 .37 9.0 40 error (invalid witness file) 5.8 3.1 120 290
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect .12  .12  1.1  9.5 .0082 0     - - timeout 900    900    15000   480 true 9.0 5.3 130 330
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect .049 .049 .65 9.9 .0082 0     - - out of memory 350    340    6900   7000 timeout 960   810   10000 2600
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .073 .075 .47 9.7 .0082 0     - - true 3.9  2.2  77   270 true 7.6 4.0 150 320
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect .058 .058 .48 9.9 .0082 0     - - out of memory 820    820    23000   7000 timeout 960   920   13000 860
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .050 .050 .56 9.9 .0082 0     - - true 3.9  2.2  81   280 true 7.8 4.2 140 320
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .080 .080 .45 9.7 .0082 0     - - true 8.6  6.2  130   390 true 44   38   590 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .055 .055 .47 9.9 .0082 0     - - true 4.2  2.4  61   270 true 10   5.6 210 370
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  1.2  11   .0082 .057 false(unreach-call) 4.2  2.4  65   280 true 7.2 3.9 140 320 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    3500   .0082 9.8   - - error (invalid witness file) .63 .40 8.0 39 error (invalid witness file) 6.0 3.2 100 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    1300   .0082 14     - - error (invalid witness file) .55 .34 10   39 error (invalid witness file) 5.9 3.1 97 290
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     11000    2400   .012  4.0   - - error (invalid witness file) .47 .32 8.8 39 error (invalid witness file) 5.4 2.9 110 290
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     14000    990   .012  0     - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 5.9 3.1 96 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    1500   .012  10     - - error (invalid witness file) .51 .32 13   41 error (invalid witness file) 5.8 3.1 120 290
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    6700   .0082 4.0   - - error (invalid witness file) .57 .36 11   42 error (invalid witness file) 6.1 3.2 100 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i out of memory 0 wit inspect 250     250     2900    15000   .0082 0     - - error (invalid witness file) .57 .36 13   44 error (invalid witness file) 5.8 3.1 120 300
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    5700   .0082 9.9   - - error (invalid witness file) .57 .37 9.4 42 error (invalid witness file) 6.3 3.4 120 300
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    730   .012  .11  - - error (invalid witness file) .60 .39 8.5 40 error (invalid witness file) 6.0 3.2 130 300
loop-invgen/id_build_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    4100   .0082 0     - - error (invalid witness file) .62 .40 8.2 42 error (invalid witness file) 6.1 3.2 110 300
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .24  .28  2.3  18   .0082 9.8   - - true 6.4  3.6  61   300 true 11   5.9 210 380
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    23   .0082 0     - - error (invalid witness file) .61 .38 11   40 error (invalid witness file) 5.9 3.1 110 290
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    2200   .0082 0     - - error (invalid witness file) .54 .33 7.9 40 error (invalid witness file) 5.3 2.9 96 290
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    5000   .012  0     - - error (invalid witness file) .63 .40 7.8 43 error (invalid witness file) 6.7 3.6 82 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1900   .0082 3.8   - - error (invalid witness file) .51 .32 8.1 39 error (invalid witness file) 6.5 3.4 140 320
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    3300   .0082 .098 - - error (invalid witness file) .62 .40 7.9 40 error (invalid witness file) 6.1 3.2 120 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    4900   .0082 0     - - error (invalid witness file) .53 .33 9.7 40 error (invalid witness file) 6.1 3.2 130 310
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    4400   .0082 0     - - error (invalid witness file) .47 .30 9.3 39 error (invalid witness file) 6.8 3.6 130 310
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 47     47     580    200   .0082 0     - - out of memory 430    420    12000   7000 true 9.1 4.9 170 330
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    2300   .0082 4.6   - - error (invalid witness file) .69 .44 7.9 42 error (invalid witness file) 5.9 3.1 100 300
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .079 .079 .46 9.8 .0082 0     - - true 5.2  2.9  46   280 true 9.8 5.3 140 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .058 .058 .49 9.9 .0082 .16  - - out of memory 370    360    8200   7000 true 11   5.9 210 380
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .064 .067 .72 9.8 .0082 0     - - true 4.6  2.5  85   280 true 8.6 4.6 140 330
loop-lit/css2003_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 510     510     6300    15000   .0082 0     - - error (invalid witness file) .47 .30 6.2 39 error (invalid witness file) 6.0 3.2 81 300
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900     900     14000    3200   .0082 0     - - error (invalid witness file) .48 .31 8.7 39 error (invalid witness file) 5.8 3.1 130 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .075 .075 .46 9.9 .0082 0     - - true 72    65    1500   790 true 94   59   940 1500
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    920   .0082 9.9   - - error (invalid witness file) .59 .38 8.9 40 error (invalid witness file) 6.3 3.3 110 290
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .058 .058 .66 9.7 .0082 0     - - true 56    49    1200   1100 true 80   48   860 1200
loop-lit/gsv2008_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 610     610     8900    15000   .0082 20     - - error (invalid witness file) .73 .46 6.6 40 error (invalid witness file) 5.7 3.1 110 290
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect .13  .16  1.2  18   .0082 9.7   - - out of memory 320    310    5900   7000 true 9.9 5.4 170 370
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect .097 .097 .77 9.9 .0082 0     - - out of memory 310    300    6300   7000 true 13   7.0 230 440
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .10  .10  .96 9.9 .0082 0     - - out of memory 360    350    6600   7000 true 13   7.4 300 450
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect .052 .052 .64 9.9 .0082 0     - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 5.7 3.0 110 290
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .078 .079 .62 9.8 .0082 0     false(unreach-call) 3.6  2.0  50   280 true 8.1 4.3 80 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect .049 .049 .72 9.7 .0082 0     - - true 4.8  2.7  50   270 timeout 960   800   12000 3900
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 64     64     690    4900   .0082 0     - - true 3.9  2.1  68   270 true 10   5.4 160 340
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect .052 .052 .47 9.7 .0082 0     - - out of memory 310    300    8700   7000 timeout 960   800   13000 4000
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    3100   .0082 4.1   - - error (invalid witness file) .54 .35 12   44 error (invalid witness file) 5.3 2.8 95 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    89   .0082 0     - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 6.1 3.2 120 300
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 wit inspect .65  .67  7.8  17   .0082 3.9   - - timeout 900    900    15000   5000 timeout 960   820   9600 2400
loop-new/half_true-unreach-call_true-termination.i unknown 0 wit inspect .074 .074 .50 9.5 .012  0     - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.9 3.1 110 300
loop-new/nested_true-unreach-call_true-termination.i unknown 0 wit inspect .068 .068 .44 9.7 .012  .025 - - error (invalid witness file) .54 .35 13   44 error (invalid witness file) 5.7 3.0 120 300
loop-industry-pattern/aiob_1_true-unreach-call.c unknown 0 wit inspect .055 .055 .58 10   .025  0     - - error (invalid witness file) .52 .32 13   40 error (invalid witness file) 6.1 3.2 110 300
loop-industry-pattern/aiob_2_true-unreach-call.c unknown 0 wit inspect .075 .075 .60 10   .025  0     - - error (invalid witness file) .52 .34 9.5 41 error (invalid witness file) 5.6 3.0 110 290
loop-industry-pattern/aiob_3_true-unreach-call.c unknown 0 wit inspect .061 .061 .50 10   .025  0     - - error (invalid witness file) .48 .31 11   40 error (invalid witness file) 7.1 3.7 130 330
loop-industry-pattern/aiob_4_true-unreach-call.c unknown 0 wit inspect .056 .057 .59 9.9 .0082 0     - - error (invalid witness file) .61 .39 10   41 error (invalid witness file) 5.6 3.0 78 290
loop-industry-pattern/mod3_true-unreach-call.c timeout 0 wit inspect 900     900     13000    6200   .0082 0     - - error (invalid witness file) .68 .43 6.9 39 error (invalid witness file) 5.8 3.1 74 300
loop-industry-pattern/nested_true-unreach-call.c out of memory 0 wit inspect 140     140     1600    15000   .0082 0     - - error (invalid witness file) .47 .32 6.6 41 error (invalid witness file) 6.1 3.2 120 300
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect .090 .092 .48 10   .029  .50  - - error (invalid witness file) .64 .42 7.4 39 error (invalid witness file) 5.8 3.1 92 300
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect .076 .076 .61 10   .029  0     - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.8 3.1 94 300
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect .084 .084 .53 9.8 .029  0     - - error (invalid witness file) .64 .41 9.6 43 error (invalid witness file) 6.0 3.2 110 300
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect .080 .080 .52 10   .029  0     - - error (invalid witness file) .50 .33 9.3 42 error (invalid witness file) 6.1 3.2 100 300
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect .059 .059 .64 10   .029  0     - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 5.8 3.1 120 300
loops/heavy_true-unreach-call.c timeout 0 wit inspect 900     900     10000    60   4.2    4.7   - - error (invalid witness file) .60 .37 9.4 39 error (invalid witness file) 6.2 3.3 120 300
loops/compact_false-unreach-call.c out of memory 0 wit inspect 860     860     8700    15000   .0082 0     error (invalid witness file) .53 .35 9.7 40 error (invalid witness file) 7.4 3.9 95 330 - -
loops/heavy_false-unreach-call.c timeout 0 wit inspect 900     900     11000    56   4.2    0     error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.6 4.0 89 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 156 60 28000 28000 350000 220000 10     240   156 780 620 11000 29000   156 540 320 8600 17000   156 11000 10000 220000 150000   156 14000 12000 180000 76000  
    correct results 72 115 330 330 4300 7600 .61  110   29 210 130 2800 9700   29 220 120 3300 9200   32 5600 5400 120000 84000   40 4700 3800 62000 33000  
        correct true 43 86 300 300 3800 7200 .36  50   0 0 0 0 0   29 0 0 0 0   32 5600 5400 120000 84000   40 4700 3800 62000 33000  
        correct false 29 29 30 30 410 440 .25  59   29 210 130 2800 9700   0 220 120 3300 9200   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 14 9 860 860 11000 4400 .12  3.9 0 430 370 6800 16000   5 40 21 560 1600   0 5000 4900 100000 60000   0 8600 7500 110000 27000  
        correct-unconfirmed true 9 9 730 730 9500 3500 .078 3.9 0 0 0 0 0   5 0 0 0 0   0 5000 4900 100000 60000   0 8600 7500 110000 27000  
        correct-unconfirmed false 5 0 130 130 1800 860 .041 0   0 430 370 6800 16000   0 40 21 560 1600   0 0 0 0 0   0 0 0 0 0  
    incorrect results 2 -64 89 89 1100 640 .025 0   0 130 110 1400 3100   1 180 130 3200 2000   0 0 0 0 0   0 0 0 0 0  
        incorrect true 2 -64 89 89 1100 640 .025 0   0 130 110 1400 3100   0 180 130 3200 2000   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (156 tasks, max score: 261) 60
Run set sv-comp17.ReachSafety-Loops