Tool 2LS 0.5.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.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 .13  .12  1.2  23 0      0    false(unreach-call) 4.3  2.4  69   290 false(unreach-call) 7.7 4.0 160 320 - -
loops/bubble_sort_false-unreach-call.i error (134) 0 wit inspect .40  .40  4.0  62 .0082 0    error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.5 3.4 120 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  .12  .87 22 0      0    false(unreach-call) 3.6  2.1  66   270 false(unreach-call) 7.9 4.2 170 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 1 wit inspect 1.4   1.4   16    43 0      0    false(unreach-call) 6.4  3.7  93   330 false(unreach-call) 40   28   420 850 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .24  .24  2.3  26 0      2.2  false(unreach-call) 4.5  2.5  35   280 false(unreach-call) 7.5 4.0 140 330 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 380     380     2000    6400 0      0    assertion 2.5  1.4  39   170 false(unreach-call) 12   6.3 190 360 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .68  .67  8.4  36 0      0    false(unreach-call) 5.1  2.8  86   290 false(unreach-call) 9.4 4.9 160 360 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 1 wit inspect 1.1   1.1   11    58 0      0    exception 3.7  2.1  77   270 false(unreach-call) 24   13   340 590 - -
loops/ludcmp_false-unreach-call.i timeout 0 wit inspect 900     900     9200    3500 0      0    error (invalid witness file) .54 .35 14   42 error (invalid witness file) 6.5 3.4 130 290 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 64     64     370    1900 0      0    false(unreach-call) 7.3  4.7  72   480 false(unreach-call) 8.1 4.3 150 350 - -
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900     900     6800    6800 .0082 0    error (invalid witness file) .52 .33 10   41 error (invalid witness file) 5.8 3.1 110 290 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .11  .11  .83 22 0      0    false(unreach-call) 3.7  2.1  67   270 false(unreach-call) 6.8 3.7 120 320 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .91  .90  8.2  56 0      0    false(unreach-call) 4.0  2.2  66   290 false(unreach-call) 7.6 4.1 130 340 - -
loops/s3_false-unreach-call.i error (134) 0 wit inspect 210     210     1400    860 .0082 0    error (invalid witness file) .59 .36 9.4 39 error (invalid witness file) 6.2 3.3 110 300 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.0   2.0   21    45 0      0    false(unreach-call) 6.1  3.3  98   320 false(unreach-call) 20   10   360 370 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .60  .59  6.5  31 0      .13 false(unreach-call) 4.7  2.6  100   290 false(unreach-call) 11   5.8 170 360 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36  .36  4.4  29 0      0    false(unreach-call) 4.0  2.3  73   290 false(unreach-call) 9.8 5.2 190 350 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41  .41  6.0  28 0      0    false(unreach-call) 4.8  2.6  100   300 false(unreach-call) 11   5.6 160 350 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25  .25  2.7  26 0      0    false(unreach-call) 5.6  3.0  74   300 false(unreach-call) 26   14   220 490 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .42  .41  4.7  28 0      0    false(unreach-call) 4.5  2.5  110   280 false(unreach-call) 8.7 4.7 150 340 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .31  .31  3.8  36 0      0    assertion 2.5  1.4  59   170 false(unreach-call) 8.3 4.4 130 350 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .10  .82 22 0      0    false(unreach-call) 3.8  2.1  86   280 false(unreach-call) 7.5 3.9 120 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .093 .95 22 0      0    false(unreach-call) 4.2  2.3  78   290 false(unreach-call) 7.3 3.9 130 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12  .11  .76 22 0      0    false(unreach-call) 3.7  2.1  74   270 false(unreach-call) 7.6 4.1 150 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  .12  .95 23 0      0    false(unreach-call) 3.9  2.2  81   270 false(unreach-call) 7.9 4.2 140 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .097 .97 22 0      0    false(unreach-call) 3.7  2.1  77   270 false(unreach-call) 7.2 3.8 150 330 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .10  .93 23 0      0    false(unreach-call) 4.0  2.2  69   270 false(unreach-call) 7.3 3.9 140 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .10  1.1  23 0      0    true 3.7  2.1  45   280 false(unreach-call) 8.4 4.5 120 320 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .47  .47  5.6  33 0      0    false(unreach-call) 5.2  2.9  68   280 false(unreach-call) 18   10   310 570 - -
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 7.2   7.2   72    150 0      0    false(unreach-call) 13    7.0  120   560 timeout 97   58   2100 3100 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .90 22 0      0    false(unreach-call) 3.5  2.0  54   280 false(unreach-call) 7.2 3.8 160 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  .86 23 0      0    - - true 5.4  3.1  61   290 true 20   14   510 390
loops/bubble_sort_true-unreach-call.i true 2 wit inspect 1.1   1.1   8.2  77 0      .16 - - true 4.3  2.4  67   270 true 7.8 4.1 150 320
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1500 0      0    - - error (invalid witness file) .59 .38 10   40 error (invalid witness file) 5.6 3.0 91 290
loops/eureka_01_true-unreach-call.i true 1 wit inspect 16     16     150    710 0      0    - - out of memory 660    640    12000   7000 timeout 960   850   20000 4300
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 2.3   2.3   28    68 0      0    - - true 480    460    8900   5300 true 36   21   490 740
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .088 .086 .79 22 0      0    - - true 4.2  2.3  65   280 true 7.6 4.1 150 320
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .10  .10  .72 22 0      0    - - true 4.1  2.3  64   280 true 7.1 3.8 140 310
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     4900    5100 0      0    - - error (invalid witness file) .58 .37 14   44 error (invalid witness file) 5.6 3.0 110 290
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .85  .85  9.9  35 0      0    - - true 20    12    430   590 true 41   28   730 740
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     900     7700    3900 0      0    - - error (invalid witness file) .48 .32 13   39 error (invalid witness file) 5.9 3.2 110 300
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 290     290     3100    3500 0      0    - - timeout 910    870    20000   5700 out of memory 48   39   1100 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .15  .15  1.5  25 0      0    - - true 8.5  6.1  230   430 true 17   9.3 230 510
loops/n.c11_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     9700    1800 0      0    - - error (invalid witness file) .65 .41 8.2 39 error (invalid witness file) 5.6 3.0 110 300
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  1.0  27 0      0    - - true 5.3  2.9  54   270 true 170   160   2900 760
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  1.1  25 0      0    - - true 3.9  2.1  77   270 true 200   200   2900 740
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  .68 23 0      0    - - true 8.0  4.3  100   310 true 9.7 5.3 200 340
loops/sum01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1700 0      0    - - error (invalid witness file) .58 .36 7.1 40 error (invalid witness file) 7.0 3.7 81 300
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect .41  .40  4.9  26 0      0    - - true 4.4  2.4  88   280 true 7.5 4.0 140 320
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .32  .31  3.7  27 0      0    - - true 6.6  3.6  62   280 true 12   6.7 210 390
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     900     4900    12000 0      0    - - error (invalid witness file) .76 .48 7.6 44 error (invalid witness file) 5.9 3.1 130 300
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  .75 22 0      0    - - true 4.1  2.3  86   270 true 10   5.5 120 330
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect .10  .099 1.0  22 0      0    - - true 5.0  2.8  66   280 true 8.2 4.4 170 320
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 6.4   6.4   81    120 0      0    - - out of memory 480    450    9000   7000 true 8.7 4.6 140 330
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  .76 22 0      .16 - - true 4.3  2.4  74   280 true 7.4 4.0 160 320
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  .78 22 0      0    - - true 5.8  3.2  53   280 true 7.9 4.2 140 320
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect .11  .10  .74 22 0      0    - - true 6.0  3.3  62   280 true 8.6 4.7 130 320
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .099 .094 .95 23 0      0    - - out of memory 320    320    8000   7000 true 11   5.9 210 390
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  .88 24 0      .16 - - true 9.4  5.0  120   380 true 9.8 5.3 170 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .083 .081 .88 22 0      0    - - true 4.5  2.5  66   280 true 7.6 4.1 130 320
loops/vogal_true-unreach-call.i true 2 wit inspect 5.5   5.5   64    89 0      0    - - true 58    46    1100   1000 true 200   150   3100 3300
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .11  .11  .65 22 0      0    - - true 4.9  2.7  55   270 true 7.6 4.1 150 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .097 .094 .77 22 0      0    - - true 3.7  2.1  59   270 true 7.6 4.0 150 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect .093 .090 .83 22 0      0    - - true 4.6  2.6  56   270 true 7.8 4.1 110 330
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900     900     8900    10000 0      0    error (invalid witness file) .53 .34 12   43 error (invalid witness file) 6.7 3.5 130 310 - -
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     10000    11000 0      0    error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.4 3.4 110 300 - -
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900     900     7300    10000 0      0    error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.6 3.0 110 300 - -
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900     900     10000    1700 0      0    error (invalid witness file) .53 .34 13   42 error (invalid witness file) 6.0 3.1 130 290 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect .83  .83  9.2  31 0      0    false(unreach-call) 5.7  3.1  67   300 timeout 98   57   940 6400 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900     900     12000    1400 0      0    error (invalid witness file) .54 .35 13   41 error (invalid witness file) 6.1 3.2 120 310 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .098 .091 .90 22 0      0    false(unreach-call) 3.6  2.0  75   280 false(unreach-call) 7.3 3.8 140 320 - -
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900     900     10000    9600 0      0    error (invalid witness file) .51 .34 10   40 error (invalid witness file) 5.7 3.1 130 300 - -
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900     900     12000    1200 0      0    error (invalid witness file) .49 .34 5.0 40 error (invalid witness file) 6.2 3.3 120 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .17  .16  1.1  25 0      0    false(unreach-call) 3.7  2.1  82   280 false(unreach-call) 7.4 3.9 160 320 - -
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900     900     13000    1400 0      0    error (invalid witness file) .50 .33 7.9 40 error (invalid witness file) 6.1 3.2 110 300 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .12  .12  .78 22 0      0    false(unreach-call) 3.6  2.0  59   270 false(unreach-call) 7.2 3.9 150 320 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .099 .093 .87 22 0      .16 false(unreach-call) 3.4  1.9  44   270 false(unreach-call) 7.6 4.0 150 320 - -
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900     900     12000    1400 0      0    error (invalid witness file) .55 .34 13   40 error (invalid witness file) 6.2 3.3 120 310 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .23  .22  2.1  25 0      0    false(unreach-call) 3.9  2.2  32   280 false(unreach-call) 12   6.3 210 360 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .24  .23  2.2  26 0      0    false(unreach-call) 4.0  2.2  58   290 false(unreach-call) 12   6.3 220 360 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 38     38     390    540 0      0    - - true 4.3  2.4  79   280 timeout 960   800   21000 3800
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     9300    12000 0      0    - - error (invalid witness file) .66 .41 8.3 39 error (invalid witness file) 6.9 3.6 98 300
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 3.8   3.8   38    130 0      0    - - true 5.6  3.1  83   310 timeout 960   860   24000 2900
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900     900     8700    10000 0      0    - - error (invalid witness file) .59 .38 9.7 44 error (invalid witness file) 6.8 3.6 130 320
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .19  .18  1.8  24 0      0    - - true 3.9  2.2  82   270 timeout 960   810   20000 2600
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect .84  .83  11    31 0      0    - - true 17    13    290   530 true 610   520   14000 1400
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .17  .17  2.1  26 0      0    - - true 8.2  4.7  150   330 true 40   27   1100 670
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900     900     12000    1600 0      0    - - error (invalid witness file) .68 .41 7.6 40 error (invalid witness file) 7.4 3.9 89 300
loop-acceleration/multivar_true-unreach-call1_true-termination.i timeout 0 wit inspect 900     900     12000    1700 0      0    - - error (invalid witness file) .49 .33 13   40 error (invalid witness file) 5.8 3.1 110 290
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect .17  .16  1.3  24 0      0    - - true 5.6  3.1  110   290 timeout 960   860   26000 4700
loop-acceleration/overflow_true-unreach-call1.i timeout 0 wit inspect 900     900     13000    1400 0      0    - - error (invalid witness file) .52 .32 9.8 41 error (invalid witness file) 6.1 3.2 110 280
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900     900     12000    1500 0      0    - - error (invalid witness file) .67 .43 8.7 43 error (invalid witness file) 6.0 3.2 99 300
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect .12  .11  1.1  24 0      0    - - timeout 900    900    20000   440 true 8.6 4.7 180 330
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900     900     10000    1600 0      0    - - error (invalid witness file) .61 .40 8.2 40 error (invalid witness file) 5.8 3.1 110 300
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .083 .079 .77 22 0      0    - - true 5.0  2.8  57   280 true 7.3 4.0 150 320
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     900     9600    1200 0      0    - - error (invalid witness file) .62 .39 12   42 error (invalid witness file) 5.5 2.9 110 290
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .12  .11  .64 22 0      0    - - true 4.6  2.6  53   280 true 9.2 5.0 120 330
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .22  .21  2.6  25 0      0    - - true 7.7  5.4  170   400 true 77   71   1100 400
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .10  .11  1.7  25 0      2.2  - - true 4.0  2.3  64   270 true 14   7.6 210 440
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .099 .98 23 0      0    false(unreach-call) 3.8  2.1  66   270 false(unreach-call) 8.3 4.3 120 310 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    540 0      0    - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.0 3.1 100 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect .12  .11  1.1  23 0      0    - - timeout 910    900    21000   6200 true 12   6.4 210 390
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 3.7   3.7   42    48 0      2.3  - - timeout 900    890    16000   1900 true 16   9.1 300 560
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9000    2000 0      0    - - error (invalid witness file) .62 .40 9.9 40 error (invalid witness file) 6.1 3.2 120 300
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 3.4   3.4   43    43 0      0    - - timeout 900    890    17000   2300 true 14   7.7 300 470
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8900    1900 0      0    - - error (invalid witness file) .67 .43 8.7 40 error (invalid witness file) 5.7 3.1 98 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9900    3200 0      0    - - error (invalid witness file) .65 .41 7.3 40 error (invalid witness file) 6.5 3.4 100 310
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    2100 0      0    - - error (invalid witness file) .56 .35 11   40 error (invalid witness file) 5.6 3.0 80 300
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     7200    1400 0      0    - - error (invalid witness file) .62 .40 8.5 40 error (invalid witness file) 5.7 3.0 100 300
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect .18  .18  1.5  25 0      0    - - true 5.1  2.9  71   290 false(unreach-call) 7.3 3.9 110 320
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .23  .23  2.3  26 0      0    - - true 5.1  2.8  66   290 false(unreach-call) 8.0 4.3 160 320
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect .70  .70  8.1  32 0      0    - - timeout 900    890    21000   1400 true 9.9 5.3 100 330
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     5300    3200 0      0    - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.1 3.2 91 300
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8400    280 0      0    - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 5.6 3.0 100 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    2200 0      0    - - error (invalid witness file) .65 .42 8.8 39 error (invalid witness file) 5.9 3.1 88 300
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    1500 0      0    - - error (invalid witness file) .61 .38 9.2 41 error (invalid witness file) 6.5 3.5 140 310
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i true 1 wit inspect .12  .12  .75 23 0      0    - - timeout 920    750    25000   6900 timeout 960   840   15000 2800
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9400    2100 0      0    - - error (invalid witness file) .58 .38 7.5 39 error (invalid witness file) 6.0 3.2 120 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    2200 0      0    - - error (invalid witness file) .63 .39 7.1 39 error (invalid witness file) 7.0 3.7 140 310
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    300 0      0    - - error (invalid witness file) .54 .35 8.6 40 error (invalid witness file) 5.8 3.1 110 310
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .34  .33  3.5  27 0      0    - - true 4.8  2.7  76   280 true 11   5.7 230 380
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9200    1700 0      0    - - error (invalid witness file) .71 .45 6.7 40 error (invalid witness file) 6.5 3.4 110 310
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .95  .95  13    35 0      0    - - true 6.6  3.6  92   290 true 8.4 4.6 180 340
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     10000    260 0      0    - - error (invalid witness file) .52 .34 7.8 39 error (invalid witness file) 5.8 3.1 120 300
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900     900     11000    2100 0      0    - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.5 3.4 88 290
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 5.2   5.2   65    82 0      0    - - true 71    64    1700   780 true 100   65   1800 1500
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     13000    1400 0      0    - - error (invalid witness file) .50 .32 7.9 42 error (invalid witness file) 6.9 3.6 160 310
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 9.0   9.0   110    120 0      0    - - true 85    75    970   1100 true 89   53   1400 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     7200    810 0      0    - - error (invalid witness file) .63 .39 7.3 40 error (invalid witness file) 5.8 3.1 130 300
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     14000    390 0      0    - - error (invalid witness file) .64 .40 9.2 41 error (invalid witness file) 5.5 2.9 100 290
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     10000    1500 0      0    - - error (invalid witness file) .53 .34 10   40 error (invalid witness file) 6.1 3.2 97 310
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    1700 0      0    - - error (invalid witness file) .61 .40 7.7 39 error (invalid witness file) 5.8 3.1 110 300
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 890     890     6700    15000 .0082 0    - - error (invalid witness file) .64 .40 8.9 39 error (invalid witness file) 7.4 3.9 120 330
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .10  .096 1.1  23 0      0    false(unreach-call) 3.6  2.0  44   270 false(unreach-call) 9.8 5.1 150 360 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect .16  .15  1.2  23 0      0    - - true 5.0  2.8  56   280 true 8.8 4.7 160 340
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  1.6  23 0      0    - - true 4.9  2.7  53   280 true 9.1 5.0 180 360
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1200 0      0    - - error (invalid witness file) .59 .37 7.6 39 error (invalid witness file) 5.7 3.0 120 310
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    1200 0      0    - - error (invalid witness file) .58 .38 12   41 error (invalid witness file) 5.8 3.1 110 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    2100 0      0    - - error (invalid witness file) .70 .45 9.2 44 error (invalid witness file) 6.4 3.3 130 310
loop-new/gauss_sum_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    1700 0      0    - - error (invalid witness file) .56 .36 7.4 40 error (invalid witness file) 5.8 3.1 120 300
loop-new/half_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    1800 0      0    - - error (invalid witness file) .69 .43 8.3 44 error (invalid witness file) 6.2 3.3 110 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     5500    2500 0      0    - - error (invalid witness file) .66 .42 8.6 40 error (invalid witness file) 6.4 3.4 110 300
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect .35  .34  2.7  29 .020  0    - - true 29    23    520   590 error 10   5.6 210 290
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect .35  .35  3.4  30 .020  .16 - - true 25    20    730   600 error 11   5.9 230 300
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect .38  .38  3.6  29 .020  0    - - true 31    24    580   580 error 11   5.8 170 310
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect .39  .38  3.0  30 .020  0    - - true 30    23    460   570 error 11   5.7 220 300
loop-industry-pattern/mod3_true-unreach-call.c true 2 wit inspect .48  .48  5.9  27 .0041 0    - - true 11    8.8  180   330 true 23   18   540 340
loop-industry-pattern/nested_true-unreach-call.c timeout 0 wit inspect 900     900     8800    270 .0041 0    - - error (invalid witness file) .70 .44 8.8 40 error (invalid witness file) 5.8 3.1 100 300
loop-industry-pattern/ofuf_1_true-unreach-call.c error (5) 0 wit inspect .24  .23  2.3  30 .012  0    - - error (invalid witness file) .53 .34 7.6 39 error (invalid witness file) 6.4 3.4 130 290
loop-industry-pattern/ofuf_2_true-unreach-call.c error (5) 0 wit inspect .27  .27  2.0  32 .012  0    - - error (invalid witness file) .65 .42 6.4 40 error (invalid witness file) 6.3 3.3 110 310
loop-industry-pattern/ofuf_3_true-unreach-call.c error (5) 0 wit inspect .28  .27  1.8  30 .012  0    - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.2 3.3 98 300
loop-industry-pattern/ofuf_4_true-unreach-call.c error (5) 0 wit inspect .25  .24  2.4  30 .012  0    - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.3 3.3 120 300
loop-industry-pattern/ofuf_5_true-unreach-call.c error (5) 0 wit inspect .25  .25  2.0  30 .012  0    - - error (invalid witness file) .59 .37 9.0 40 error (invalid witness file) 5.8 3.1 87 310
loops/heavy_true-unreach-call.c out of memory 0 wit inspect 31     30     380    15000 .0041 0    - - error (invalid witness file) .61 .39 9.3 40 error (invalid witness file) 7.1 3.7 130 310
loops/compact_false-unreach-call.c timeout 0 wit inspect 900     900     8800    3000 .0041 0    error (invalid witness file) .53 .33 10   42 error (invalid witness file) 6.0 3.2 120 300 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 31     31     380    15000 .0041 0    error (invalid witness file) .53 .35 7.7 39 error (invalid witness file) 5.9 3.2 110 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 145 51000 51000 550000 220000 .20  7.8 156 170 96 2700 11000   156 660 370 11000 27000   156 8900 8400 190000 70000   156 8100 6700 170000 68000  
    correct results 89 142 550 550 3500 12000 .086 7.8 33 160 91 2600 10000   34 570 320 9100 22000   46 6400 6100 130000 48000   45 5800 4900 130000 39000  
        correct true 53 106 89 88 980 2400 .086 5.2 1 0 0 0 0   0 0 0 0 0   46 6400 6100 130000 48000   43 5800 4900 130000 39000  
        correct false 36 36 470 470 2600 9400 0     2.5 32 160 91 2600 10000   34 570 320 9100 22000   0 0 0 0 0   2 0 0 0 0  
    correct-unconfimed results 3 3 310 310 3300 4200 0     0   0 0 0 0 0   0 0 0 0 0   0 2500 2300 57000 20000   0 2000 1700 36000 14000  
        correct-unconfirmed true 3 3 310 310 3300 4200 0     0   0 0 0 0 0   0 0 0 0 0   0 2500 2300 57000 20000   0 2000 1700 36000 14000  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (156 tasks, max score: 261) 145
Run set sv-comp17.ReachSafety-Loops