Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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 .12  .12  1.0  23 .84 0   false(unreach-call) 4.0  2.2  64   280 false(unreach-call) 6.9 3.8 140 320 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect .66  .66  8.1  49 .84 0   false(unreach-call) 7.8  4.2  90   350 error 11   5.9 170 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .072 .072 .80 23 .84 0   false(unreach-call) 3.6  2.1  84   270 false(unreach-call) 7.3 3.9 140 310 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 0 wit inspect .17  .17  1.9  24 .84 0   true 4.4  2.4  65   280 true 7.8 4.2 110 320 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .71 23 .84 0   false(unreach-call) 3.9  2.1  78   270 false(unreach-call) 7.5 4.1 150 320 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9   2.9   5.9  25 .84 0   timeout 93    89    1200   1400 false(unreach-call) 34   19   510 740 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18  .18  2.3  23 .84 0   true 4.4  2.4  60   270 false(unreach-call) 12   6.7 210 380 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect .84  .82  11    66 .84 0   true 5.5  3.0  85   280 timeout 96   84   1300 680 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 2.1   2.1   30    33 .84 0   true 5.6  3.0  94   290 out of memory 45   36   540 7000 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  1.6  23 .84 0   false(unreach-call) 8.2  5.3  150   470 true 7.7 4.1 150 320 - -
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 310     300     3600    15000 .84 0   error (invalid witness file) .52 .34 4.6 44 error (invalid witness file) 6.5 3.5 120 310 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .10  .10  .73 23 .84 0   false(unreach-call) 3.8  2.1  80   270 false(unreach-call) 8.0 4.2 140 330 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .073 .072 .85 23 .84 0   false(unreach-call) 4.1  2.3  78   280 false(unreach-call) 8.3 4.5 150 350 - -
loops/s3_false-unreach-call.i timeout 0 wit inspect 900     900     8800    3600 .84 0   error (invalid witness file) .52 .35 4.3 42 error (invalid witness file) 7.3 3.9 91 300 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16  .16  1.9  23 .84 0   false(unreach-call) 7.1  3.8  110   320 false(unreach-call) 27   15   480 490 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  1.1  23 .84 0   false(unreach-call) 6.8  3.7  56   290 false(unreach-call) 15   8.5 230 460 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .34  .34  .70 23 .84 0   true 3.9  2.1  79   270 false(unreach-call) 14   7.6 230 380 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .14  .14  1.7  25 .84 0   false(unreach-call) 6.0  3.3  110   300 false(unreach-call) 17   9.2 240 510 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  1.1  23 .84 0   false(unreach-call) 4.6  2.6  73   270 true 7.3 3.9 140 320 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .10  .85 23 .84 0   false(unreach-call) 4.0  2.2  73   270 true 7.4 3.9 140 310 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .16  .16  2.0  23 .84 0   false(unreach-call) 4.7  2.7  83   310 false(unreach-call) 9.2 4.9 170 360 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .072 .072 .82 23 .84 0   false(unreach-call) 4.0  2.3  63   270 false(unreach-call) 8.1 4.3 130 310 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .080 .079 .84 23 .84 0   false(unreach-call) 4.5  2.5  52   270 false(unreach-call) 7.4 4.0 150 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .077 .077 .78 23 .84 0   false(unreach-call) 3.6  2.1  57   270 false(unreach-call) 8.1 4.3 160 330 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .082 .081 .79 23 .84 0   false(unreach-call) 4.1  2.3  68   290 false(unreach-call) 7.6 4.0 130 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .074 .073 .81 23 .91 0   false(unreach-call) 3.8  2.2  74   270 false(unreach-call) 7.0 3.8 140 310 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  .75 23 .99 0   false(unreach-call) 4.3  2.4  72   280 false(unreach-call) 8.1 4.3 130 330 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .084 .083 .93 23 .84 0   true 3.8  2.1  78   280 false(unreach-call) 11   6.2 240 380 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17  .16  1.7  24 .84 0   false(unreach-call) 4.5  2.6  81   290 true 8.3 4.5 170 330 - -
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect .60  .60  6.6  40 .84 0   timeout 91    80    1200   820 timeout 98   60   930 6600 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  .73 23 .84 0   false(unreach-call) 4.6  2.6  41   280 true 7.6 4.1 120 310 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  .86 23 .84 0   - - true 4.3  2.4  83   280 true 9.8 5.3 150 350
loops/bubble_sort_true-unreach-call.i timeout 0 wit inspect 900     900     11000    5100 .84 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.5 2.9 100 290
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    5500 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.8 3.1 110 300
loops/eureka_01_true-unreach-call.i true 1 wit inspect .31  .31  5.0  38 .84 0   - - out of memory 550    520    6400   7000 timeout 960   850   13000 4500
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .083 .082 1.1  23 .84 0   - - true 390    370    5100   5200 true 35   20   400 760
loops/for_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 410     390     6800    15000 .84 0   - - error (invalid witness file) .53 .33 9.4 40 error (invalid witness file) 5.1 2.8 87 280
loops/for_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 420     390     5800    15000 .84 0   - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.8 3.1 120 300
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    130 .84 0   - - error (invalid witness file) .50 .33 8.5 40 error (invalid witness file) 7.0 3.6 150 320
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .089 .088 .97 23 .84 0   - - true 18    11    250   570 true 43   28   680 790
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     890     13000    11000 .84 0   - - error (invalid witness file) .51 .35 12   42 error (invalid witness file) 6.2 3.3 130 320
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .14  .14  1.5  24 .84 0   - - timeout 910    870    12000   5800 out of memory 47   38   510 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .10  .10  1.1  23 .84 0   - - true 9.1  6.6  130   430 true 11   6.2 150 370
loops/n.c11_true-unreach-call_false-termination.i out of memory 0 wit inspect 180     180     2400    15000 .84 0   - - error (invalid witness file) .51 .32 8.9 39 error (invalid witness file) 5.4 2.9 62 290
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  .87 23 .84 0   - - true 4.1  2.3  75   270 true 170   160   3200 780
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .075 .075 .81 23 .84 0   - - true 4.1  2.3  75   270 true 170   160   3000 770
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 3.1   3.1   8.4  39 .84 0   - - true 6.7  3.6  97   310 true 11   5.9 160 380
loops/sum01_true-unreach-call_true-termination.i out of memory 0 wit inspect 200     200     2900    15000 .84 0   - - error (invalid witness file) .54 .35 6.6 43 error (invalid witness file) 5.6 2.9 110 280
loops/sum03_true-unreach-call_false-termination.i out of memory 0 wit inspect 410     390     5800    15000 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.3 3.4 120 300
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .087 .086 .88 23 .84 0   - - true 5.4  3.0  43   280 true 11   6.3 150 410
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     900     9300    790 .84 0   - - error (invalid witness file) .60 .39 8.9 40 error (invalid witness file) 5.4 2.9 110 280
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .10  .11  .89 23 .84 0   - - true 4.0  2.2  50   280 true 7.7 4.1 100 330
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    6700 .84 0   - - error (invalid witness file) .51 .32 7.6 40 error (invalid witness file) 5.1 2.8 92 290
loops/trex01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    7000 .84 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 5.8 3.1 120 300
loops/trex02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    12000 .84 0   - - error (invalid witness file) .68 .42 11   44 error (invalid witness file) 5.8 3.1 110 290
loops/trex03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    5300 .84 0   - - error (invalid witness file) .49 .32 8.5 39 error (invalid witness file) 5.7 3.0 92 290
loops/trex04_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     12000    7300 .84 0   - - error (invalid witness file) .55 .37 7.7 39 error (invalid witness file) 6.1 3.2 120 300
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  .87 23 .84 0   - - out of memory 280    270    4600   7000 true 10   5.5 200 350
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .35  .34  3.4  36 .84 0   - - true 10    5.4  180   400 true 9.5 5.1 150 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .097 .096 1.1  23 .84 0   - - true 4.9  2.7  88   290 true 8.5 4.6 140 320
loops/vogal_true-unreach-call.i true 2 wit inspect .30  .30  3.9  24 .84 0   - - true 50    39    840   1000 true 200   150   3500 3600
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 430     390     6700    15000 .84 0   - - error (invalid witness file) .51 .32 13   41 error (invalid witness file) 5.7 3.0 92 300
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 430     390     6600    15000 .84 0   - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.9 3.2 120 300
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 wit inspect 420     400     6000    15000 .84 0   - - error (invalid witness file) .58 .37 15   42 error (invalid witness file) 6.1 3.2 120 300
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 310     310     4800    2000 .84 0   timeout 97    90    960   2400 timeout 97   78   1100 5000 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 180     160     2400    9200 .84 0   timeout 96    84    2300   1600 timeout 98   63   1100 6300 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 320     310     4300    2300 .84 0   timeout 96    84    750   2800 timeout 97   79   1900 4600 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 21     17     280    1500 .84 0   false(unreach-call) 25    14    500   1000 true 7.2 3.8 140 310 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 2.2   2.2   29    260 .84 0   false(unreach-call) 5.6  3.1  94   300 timeout 98   57   1000 7000 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 260     240     3800    15000 .84 0   error (invalid witness file) .52 .32 10   41 error (invalid witness file) 6.0 3.2 110 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .088 .087 .77 23 .84 0   false(unreach-call) 4.2  2.4  44   280 false(unreach-call) 7.6 4.1 150 320 - -
loop-acceleration/nested_false-unreach-call1.i out of memory 0 wit inspect 330     270     4100    15000 .84 0   error (invalid witness file) .49 .32 13   40 error (invalid witness file) 5.9 3.1 110 300 - -
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 510     450     6700    15000 .84 0   error (invalid witness file) .50 .32 6.0 40 error (invalid witness file) 6.0 3.2 110 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .074 .074 .83 23 .84 0   false(unreach-call) 3.9  2.2  86   270 false(unreach-call) 7.7 4.1 150 320 - -
loop-acceleration/simple_false-unreach-call1.i out of memory 0 wit inspect 310     250     3800    15000 .99 0   error (invalid witness file) .48 .32 4.5 39 error (invalid witness file) 6.0 3.2 130 300 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .074 .074 1.1  23 .84 0   false(unreach-call) 3.6  2.0  68   270 false(unreach-call) 7.0 3.8 130 320 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .10  .10  .83 23 .84 0   false(unreach-call) 3.6  2.0  73   270 false(unreach-call) 7.6 4.1 150 320 - -
loop-acceleration/simple_false-unreach-call4.i out of memory 0 wit inspect 310     250     4100    15000 .84 0   error (invalid witness file) .54 .34 13   41 error (invalid witness file) 5.9 3.2 120 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .66 23 .84 0   false(unreach-call) 3.8  2.1  78   270 true 6.9 3.7 140 310 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .29  .29  1.1  23 .84 0   false(unreach-call) 3.8  2.1  65   270 true 6.7 3.6 140 300 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 110     99     200    1600 .84 0   - - true 8.7  4.7  93   310 timeout 960   800   11000 3800
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 140     120     1800    8500 .84 0   - - out of memory 290    280    3800   7000 timeout 960   800   12000 4000
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 64     60     810    2100 .84 0   - - timeout 910    890    14000   6000 timeout 960   850   17000 2900
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 65     61     850    2000 .84 0   - - out of memory 280    270    4900   7000 timeout 960   850   12000 3000
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 21     18     270    1500 .84 0   - - true 9.2  4.9  100   310 timeout 960   810   11000 2600
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 11     11     140    1100 .84 0   - - true 16    12    290   540 true 600   510   9500 1400
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .25  .25  3.3  37 .84 0   - - true 8.0  4.6  150   340 true 36   25   420 660
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 260     240     3000    15000 .84 0   - - error (invalid witness file) .50 .33 8.9 41 error (invalid witness file) 5.3 2.9 100 290
loop-acceleration/multivar_true-unreach-call1_true-termination.i out of memory 0 wit inspect 160     150     1700    15000 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.4 3.4 96 300
loop-acceleration/nested_true-unreach-call1.i out of memory 0 wit inspect 330     270     3800    15000 .84 0   - - error (invalid witness file) .49 .31 8.9 39 error (invalid witness file) 6.3 3.3 140 300
loop-acceleration/overflow_true-unreach-call1.i out of memory 0 wit inspect 320     250     3600    15000 .84 0   - - error (invalid witness file) .54 .34 12   43 error (invalid witness file) 6.1 3.2 130 300
loop-acceleration/phases_true-unreach-call1.i out of memory 0 wit inspect 510     450     6600    15000 .84 0   - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 5.9 3.1 120 300
loop-acceleration/phases_true-unreach-call2_false-termination.i out of memory 0 wit inspect 740     740     5200    15000 .84 0   - - error (invalid witness file) .55 .36 11   39 error (invalid witness file) 5.7 3.1 100 300
loop-acceleration/simple_true-unreach-call1.i out of memory 0 wit inspect 310     250     4200    15000 .84 0   - - error (invalid witness file) .49 .32 6.0 40 error (invalid witness file) 5.8 3.1 91 300
loop-acceleration/simple_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     10000    8200 .84 0   - - error (invalid witness file) .55 .35 14   42 error (invalid witness file) 6.0 3.2 110 290
loop-acceleration/simple_true-unreach-call3_true-termination.i out of memory 0 wit inspect 130     120     1500    15000 .84 0   - - error (invalid witness file) .48 .31 12   39 error (invalid witness file) 5.9 3.1 110 300
loop-acceleration/simple_true-unreach-call4.i out of memory 0 wit inspect 310     250     4000    15000 .84 0   - - error (invalid witness file) .51 .33 9.0 39 error (invalid witness file) 5.9 3.1 110 300
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .080 .079 .98 23 .84 0   - - true 7.0  5.0  130   400 true 55   49   640 410
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .081 .080 .83 23 .84 0   - - true 4.2  2.3  89   280 true 10   5.4 150 360
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .095 .095 .90 23 .84 0   false(unreach-call) 4.0  2.2  79   270 false(unreach-call) 7.7 4.1 170 330 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1600 .84 0   - - error (invalid witness file) .55 .35 12   41 error (invalid witness file) 5.6 3.0 89 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i out of memory 0 wit inspect 220     220     2700    15000 .84 0   - - error (invalid witness file) .49 .33 9.7 40 error (invalid witness file) 5.8 3.1 110 300
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     9300    170 .84 0   - - error (invalid witness file) .50 .32 9.3 41 error (invalid witness file) 5.5 2.9 81 300
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    310 .84 0   - - error (invalid witness file) .47 .31 8.8 39 error (invalid witness file) 6.2 3.3 120 310
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    400 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.8 3.2 110 300
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9900    14000 .84 0   - - error (invalid witness file) .47 .31 4.5 40 error (invalid witness file) 5.2 2.8 100 290
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i out of memory 0 wit inspect 450     450     5800    15000 .84 0   - - error (invalid witness file) .54 .35 11   39 error (invalid witness file) 6.1 3.3 110 300
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9700    9100 .84 0   - - error (invalid witness file) .51 .35 6.9 39 error (invalid witness file) 5.6 3.0 94 290
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8700    2300 .84 0   - - error (invalid witness file) .51 .34 9.8 41 error (invalid witness file) 5.7 3.1 81 300
loop-invgen/id_build_true-unreach-call_true-termination.i out of memory 0 wit inspect 240     240     2700    15000 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.7 3.1 110 290
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .091 .090 .97 23 .84 0   - - true 5.2  2.9  110   280 true 10   5.6 120 360
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8700    2400 .84 0   - - error (invalid witness file) .51 .34 7.6 41 error (invalid witness file) 6.5 3.4 94 320
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    2500 .84 0   - - error (invalid witness file) .54 .36 12   40 error (invalid witness file) 6.3 3.3 100 300
loop-invgen/nested9_true-unreach-call_true-termination.i out of memory 0 wit inspect 210     210     2800    15000 .84 0   - - error (invalid witness file) .55 .37 7.3 42 error (invalid witness file) 5.8 3.1 110 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    11000 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.9 3.2 120 300
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .69 .44 8.5 42 error (invalid witness file) 5.9 3.1 110 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i out of memory 0 wit inspect 74     74     780    15000 .84 0   - - error (invalid witness file) .47 .32 10   40 error (invalid witness file) 6.4 3.4 120 300
loop-invgen/up_true-unreach-call_true-termination.i out of memory 0 wit inspect 570     570     6900    15000 .84 0   - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.4 3.4 110 310
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     13000    7700 .84 0   - - error (invalid witness file) .49 .31 7.1 40 error (invalid witness file) 6.1 3.2 110 300
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     13000    130 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.7 3.1 100 290
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .28  .28  .79 23 .84 0   - - true 4.1  2.3  50   280 true 10   5.4 160 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    7500 .84 0   - - error (invalid witness file) .66 .42 6.8 42 error (invalid witness file) 5.9 3.1 120 300
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .39  .35  4.9  52 .84 0   - - true 6.6  3.6  130   300 true 8.3 4.5 110 350
loop-lit/css2003_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 220     220     2600    15000 .84 0   - - error (invalid witness file) .49 .31 9.9 39 error (invalid witness file) 6.3 3.4 120 310
loop-lit/ddlm2013_true-unreach-call.i out of memory 0 wit inspect 330     330     2600    15000 .84 0   - - error (invalid witness file) .48 .31 5.8 40 error (invalid witness file) 5.3 2.8 110 290
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .45  .42  5.5  43 .84 0   - - true 56    49    550   790 true 94   59   860 1500
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    11000 .84 0   - - error (invalid witness file) .50 .34 4.0 39 error (invalid witness file) 6.3 3.3 100 300
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .49  .44  6.8  48 .95 0   - - true 52    45    920   1100 true 78   47   820 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9400    6200 .84 0   - - error (invalid witness file) .50 .33 4.2 41 error (invalid witness file) 6.0 3.2 120 290
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     13000    740 .84 0   - - error (invalid witness file) .49 .31 8.9 40 error (invalid witness file) 5.9 3.2 95 300
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    4900 .84 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.3 3.3 120 310
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    4800 .84 0   - - error (invalid witness file) .51 .32 8.7 39 error (invalid witness file) 6.7 3.5 130 320
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     10000    180 .84 0   - - error (invalid witness file) .48 .32 6.8 39 error (invalid witness file) 5.9 3.1 100 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .28  .28  .79 23 .84 0   false(unreach-call) 3.7  2.1  73   270 false(unreach-call) 7.8 4.1 150 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i out of memory 0 wit inspect 300     240     3300    15000 .99 0   - - error (invalid witness file) .50 .32 9.5 40 error (invalid witness file) 5.6 3.0 120 300
loop-new/count_by_1_variant_true-unreach-call_true-termination.i out of memory 0 wit inspect 390     360     5300    15000 .84 0   - - error (invalid witness file) .52 .33 9.6 41 error (invalid witness file) 6.5 3.5 89 300
loop-new/count_by_2_true-unreach-call_true-termination.i out of memory 0 wit inspect 310     250     3600    15000 .84 0   - - error (invalid witness file) .47 .31 6.8 39 error (invalid witness file) 5.4 2.9 85 290
loop-new/count_by_k_true-unreach-call_true-termination.i out of memory 0 wit inspect 150     150     1800    15000 .84 0   - - error (invalid witness file) .63 .40 7.7 40 error (invalid witness file) 6.1 3.3 120 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9800    2800 .84 0   - - error (invalid witness file) .50 .31 8.2 40 error (invalid witness file) 5.8 3.1 92 300
loop-new/gauss_sum_true-unreach-call_true-termination.i out of memory 0 wit inspect 250     250     3500    15000 .84 0   - - error (invalid witness file) .52 .35 8.7 43 error (invalid witness file) 6.0 3.2 120 300
loop-new/half_true-unreach-call_true-termination.i out of memory 0 wit inspect 880     850     2400    15000 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 120 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8800    5400 .84 0   - - error (invalid witness file) .53 .34 11   42 error (invalid witness file) 6.7 3.5 130 310
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect .82  .78  11    82 .84 0   - - true 25    20    490   600 error 11   5.8 210 300
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect .84  .81  10    81 .84 0   - - true 27    22    540   590 error 10   5.5 180 290
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect .83  .80  9.5  81 .84 0   - - true 24    19    250   590 error 10   5.5 140 300
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect 3.4   3.3   7.9  81 .84 0   - - true 23    18    500   540 error 10   5.5 160 300
loop-industry-pattern/mod3_true-unreach-call.c timeout 0 wit inspect 900     900     13000    150 .84 0   - - error (invalid witness file) .50 .33 6.1 40 error (invalid witness file) 6.1 3.2 130 290
loop-industry-pattern/nested_true-unreach-call.c out of memory 0 wit inspect 290     290     3700    15000 .84 0   - - error (invalid witness file) .49 .32 12   43 error (invalid witness file) 5.9 3.1 110 300
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect .71  .70  10    25 .84 0   - - error (invalid witness file) .50 .32 6.9 42 error (invalid witness file) 5.8 3.1 110 300
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect .71  .70  8.9  25 .84 0   - - error (invalid witness file) .52 .35 8.3 42 error (invalid witness file) 6.1 3.2 94 300
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect .68  .68  8.7  25 .84 0   - - error (invalid witness file) .55 .34 11   40 error (invalid witness file) 5.9 3.1 95 290
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect .62  .61  8.2  25 .84 0   - - error (invalid witness file) .49 .33 8.9 40 error (invalid witness file) 6.0 3.2 120 300
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect .62  .62  7.0  25 .84 0   - - error (invalid witness file) .46 .31 6.2 39 error (invalid witness file) 6.2 3.3 120 300
loops/heavy_true-unreach-call.c out of memory 0 wit inspect 860     860     11000    15000 .84 0   - - error (invalid witness file) .50 .32 8.6 40 error (invalid witness file) 5.7 3.0 94 290
loops/compact_false-unreach-call.c out of memory 0 wit inspect 340     310     4700    15000 .84 0   error (invalid witness file) .50 .32 9.5 40 error (invalid witness file) 5.9 3.2 100 300 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 870     870     12000    15000 .84 0   error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.6 3.5 110 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 156 96 48000 47000 580000 820000 130   0   156 670 540 9700 21000   156 1000 680 15000 52000   156 4000 3800 58000 60000   156 7900 6500 110000 67000  
    correct results 63 91 190 170 1000 7700 53   0   34 270 190 4200 12000   33 440 240 7100 19000   27 1100 940 16000 24000   22 3600 2900 48000 24000  
        correct true 28 56 160 140 700 5100 24   0   3 0 0 0 0   8 0 0 0 0   27 1100 940 16000 24000   22 3600 2900 48000 24000  
        correct false 35 35 30 27 350 2500 30   0   31 270 190 4200 12000   25 440 240 7100 19000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 12 5 1100 1000 15000 26000 10   0   3 400 350 5400 8400   1 540 400 6900 30000   0 2900 2800 41000 33000   0 3900 3400 54000 21000  
        correct-unconfirmed true 5 5 270 250 3400 13000 4.2 0   3 0 0 0 0   1 0 0 0 0   0 2900 2800 41000 33000   0 3900 3400 54000 21000  
        correct-unconfirmed false 7 0 810 790 12000 14000 5.9 0   0 400 350 5400 8400   0 540 400 6900 30000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (156 tasks, max score: 261) 96
Run set sv-comp17.ReachSafety-Loops