Tool CBMC 5.6
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 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 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/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.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/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.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 .11 .10  .89 17 0      0      false(unreach-call) 3.9  2.2  66   280 false(unreach-call) 7.7 4.1 170 320 - -
loops/bubble_sort_false-unreach-call.i error (1) 0 wit inspect .30 .29  3.1  26 .0082 0      error (invalid witness file) .52 .33 12   39 error (invalid witness file) 5.6 3.0 120 280 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12 .11  .90 17 0      0      false(unreach-call) 3.6  2.0  43   280 false(unreach-call) 8.5 4.5 110 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 1 wit inspect .39 .38  3.9  26 .090  0      false(unreach-call) 8.6  4.9  140   470 timeout 96   64   1200 4500 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12 .11  .99 17 0      0      false(unreach-call) 4.0  2.2  72   280 false(unreach-call) 9.4 5.0 100 320 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.4  2.4   26    320 .037  0      false(unreach-call) 5.6  3.2  110   310 false(unreach-call) 16   8.3 340 410 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .51 .50  4.8  38 .029  0      false(unreach-call) 5.2  2.9  110   300 false(unreach-call) 8.9 4.7 210 360 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 1 wit inspect .85 .84  9.8  23 .11   0      exception 2.6  1.5  57   170 false(unreach-call) 23   12   480 580 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 5.0  5.0   76    130 6.3    0      true 12    6.6  150   400 out of memory 52   42   880 7000 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15 .14  1.3  21 0      0      unknown 3.8  2.1  83   280 false(unreach-call) 11   5.7 110 350 - -
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 190    190     2100    15000 12      .025  error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.4 2.9 60 310 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .13 .12  .98 17 0      0      false(unreach-call) 3.5  2.0  44   280 false(unreach-call) 8.0 4.3 120 320 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25 .25  3.4  39 0      0      false(unreach-call) 9.6  5.2  130   610 false(unreach-call) 9.2 4.9 120 340 - -
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 26    26     320    1200 .64   0      true 17    9.1  210   510 false(unreach-call) 48   33   1100 640 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .26 .25  2.8  19 .041  0      false(unreach-call) 5.4  3.0  120   300 false(unreach-call) 19   9.8 350 370 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40 .40  4.3  17 .045  0      false(unreach-call) 4.6  2.5  39   290 false(unreach-call) 11   5.9 200 350 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .28 .27  2.1  17 .020  0      false(unreach-call) 4.3  2.4  83   280 false(unreach-call) 13   6.8 140 370 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .43 .42  3.5  17 .041  0      false(unreach-call) 4.9  2.7  88   280 false(unreach-call) 10   5.6 210 360 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .38 .37  3.9  17 .049  0      false(unreach-call) 5.2  2.8  93   290 false(unreach-call) 21   12   250 490 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41 .40  3.7  17 .033  0      false(unreach-call) 4.3  2.4  78   290 false(unreach-call) 8.8 4.8 170 350 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .11 .11  1.0  20 0      0      false(unreach-call) 4.8  2.7  85   300 false(unreach-call) 8.4 4.5 140 340 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12 .11  .75 17 0      .16   false(unreach-call) 3.6  2.0  50   280 false(unreach-call) 9.3 5.0 100 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .14 .13  .93 19 0      .22   false(unreach-call) 3.8  2.1  88   270 false(unreach-call) 7.4 4.0 160 320 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11 .11  .98 17 0      0      false(unreach-call) 3.7  2.1  72   270 false(unreach-call) 7.4 3.9 160 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .14 .13  .90 18 0      0      false(unreach-call) 3.9  2.2  86   280 false(unreach-call) 7.6 4.0 140 330 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11 .098 1.1  17 0      0      false(unreach-call) 3.5  2.0  62   270 false(unreach-call) 7.1 3.8 110 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15 .14  .98 18 0      0      false(unreach-call) 3.7  2.1  84   270 false(unreach-call) 7.3 3.9 130 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .28 .27  2.6  17 .016  0      true 4.0  2.3  56   290 false(unreach-call) 8.2 4.4 110 320 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .35 .34  3.7  23 .033  0      false(unreach-call) 4.5  2.5  41   290 false(unreach-call) 20   11   400 580 - -
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect .54 .53  5.4  27 .34   0      false(unreach-call) 14    7.4  220   560 timeout 96   54   1100 2900 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11 .11  .78 17 0      0      false(unreach-call) 3.6  2.0  73   270 false(unreach-call) 6.6 3.6 110 300 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .19 .18  1.7  19 0      0      - - true 4.7  2.6  110   300 true 9.7 5.3 180 350
loops/bubble_sort_true-unreach-call.i error (42) 0 wit inspect 850    850     5100    14000 100      .074  - - error (invalid witness file) .51 .33 9.9 41 error (invalid witness file) 6.1 3.2 130 300
loops/count_up_down_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6000    7200 5.0    0      - - error (invalid witness file) .54 .35 8.5 40 error (invalid witness file) 6.0 3.2 120 300
loops/eureka_01_true-unreach-call.i true 1 wit inspect .95 .95  11    23 .67   .17   - - out of memory 620    590    11000   7000 timeout 960   840   13000 4000
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .31 .31  2.8  17 .041  0      - - exception 3.4  1.9  68   260 true 37   21   760 740
loops/for_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 250    250     3800    15000 4.5    .0041 - - error (invalid witness file) .63 .40 6.8 40 error (invalid witness file) 6.2 3.2 140 300
loops/for_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 260    260     3500    15000 4.5    0      - - error (invalid witness file) .51 .32 11   41 error (invalid witness file) 6.2 3.3 120 310
loops/insertion_sort_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     3700    3100 .053  0      - - error (invalid witness file) .67 .43 7.5 40 error (invalid witness file) 6.1 3.2 110 300
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .32 .32  3.2  17 .029  0      - - true 28    17    270   580 true 44   29   700 740
loops/linear_sea.ch_true-unreach-call.i error (1) 0 wit inspect 810    810     3600    11000 3.7    0      - - error (invalid witness file) .48 .32 12   41 error (invalid witness file) 6.3 3.3 130 310
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 11    11     140    210 18      .41   - - exception 6.4  3.4  110   280 out of memory 46   35   540 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .19 .19  1.6  17 0      0      - - true 9.6  7.0  170   430 true 12   6.6 220 380
loops/n.c11_true-unreach-call_false-termination.i error (42) 0 wit inspect 850    850     4400    3600 5.1    0      - - error (invalid witness file) .51 .32 9.7 40 error (invalid witness file) 7.2 3.8 82 290
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .19 .18  1.5  17 0      0      - - exception 2.9  1.6  54   260 true 180   170   5500 760
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .15 .15  1.6  17 0      0      - - exception 3.2  1.8  53   260 true 210   200   2600 760
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .51 .51  5.2  22 .11   0      - - true 10    5.5  130   320 true 11   5.8 200 370
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 19    19     210    120 2.3    0      - - timeout 910    890    23000   3500 true 23   15   220 550
loops/sum03_true-unreach-call_false-termination.i out of memory 0 wit inspect 320    320     4200    15000 5.5    .0082 - - error (invalid witness file) .53 .33 9.6 41 error (invalid witness file) 5.5 2.9 83 300
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .40 .40  5.4  17 .029  0      - - true 6.3  3.4  69   280 true 13   6.9 270 380
loops/sum_array_true-unreach-call.i error (42) 0 wit inspect 850    850     3900    1500 .34   0      - - error (invalid witness file) .56 .37 11   44 error (invalid witness file) 6.5 3.4 110 300
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .17 .17  1.8  19 0      0      - - true 5.5  3.0  63   280 true 7.4 4.0 160 320
loops/terminator_03_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6200    500 1.2    .0041 - - error (invalid witness file) .62 .40 10   39 error (invalid witness file) 5.4 2.9 90 290
loops/trex01_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     4300    6100 23      0      - - error (invalid witness file) .53 .35 9.7 41 error (invalid witness file) 6.2 3.3 130 300
loops/trex02_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     7900    1000 2.4    0      - - error (invalid witness file) .77 .47 6.8 39 error (invalid witness file) 6.2 3.3 120 300
loops/trex03_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     7000    840 2.2    0      - - error (invalid witness file) .61 .38 7.4 39 error (invalid witness file) 6.1 3.2 130 300
loops/trex04_true-unreach-call_false-termination.i error (42) 0 wit inspect 850    850     7200    2700 3.0    0      - - error (invalid witness file) .53 .35 10   39 error (invalid witness file) 6.0 3.2 130 300
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .29 .29  3.2  17 .020  0      - - exception 4.1  2.3  47   260 true 11   5.9 180 370
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 1.6  1.6   20    35 .46   0      - - true 23    13    250   560 true 10   5.4 130 370
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .48 .48  4.3  18 .074  0      - - true 6.2  3.3  87   300 true 7.9 4.2 140 320
loops/vogal_true-unreach-call.i true 2 wit inspect .33 .33  3.5  18 .061  0      - - true 64    50    1100   1000 true 210   160   3600 3400
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 260    260     3300    15000 3.1    0      - - error (invalid witness file) .48 .32 8.0 39 error (invalid witness file) 5.7 3.1 120 300
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 260    260     3200    15000 3.1    .0041 - - error (invalid witness file) .61 .39 10   39 error (invalid witness file) 7.5 3.9 99 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 wit inspect 230    230     2800    15000 5.4    .012  - - error (invalid witness file) .56 .35 8.8 40 error (invalid witness file) 5.8 3.1 110 300
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 29    29     370    1700 29      0      timeout 94    54    1300   5800 out of memory 70   44   1400 7000 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 61    61     830    3500 56      .0041 timeout 98    55    1100   6300 timeout 97   58   1300 6200 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 23    23     310    930 17      0      timeout 97    59    2000   3900 out of memory 85   52   990 7000 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 1.3  1.3   16    20 1.9    0      false(unreach-call) 37    20    780   1400 timeout 96   60   960 5300 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 1.4  1.4   15    50 .26   0      false(unreach-call) 5.7  3.1  80   290 timeout 98   57   1000 6500 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 260    260     3400    15000 3.4    .0041 error (invalid witness file) .48 .32 7.9 39 error (invalid witness file) 5.5 3.0 89 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .13 .12  .94 17 0      0      false(unreach-call) 3.9  2.2  86   270 false(unreach-call) 11   5.7 110 330 - -
loop-acceleration/nested_false-unreach-call1.i out of memory 0 wit inspect 310    310     4000    15000 13      0      error (invalid witness file) .52 .34 13   43 error (invalid witness file) 6.0 3.2 92 290 - -
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 310    310     3700    15000 .74   .0041 error (invalid witness file) .47 .31 5.5 40 error (invalid witness file) 6.6 3.5 120 310 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .13 .12  .97 17 0      0      false(unreach-call) 3.8  2.1  52   280 false(unreach-call) 7.3 4.0 130 310 - -
loop-acceleration/simple_false-unreach-call1.i error (1) 0 wit inspect 270    270     3600    15000 2.2    710      error (invalid witness file) .69 .43 11   44 error (invalid witness file) 8.2 4.2 95 310 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .13 .14  1.1  17 0      .59   false(unreach-call) 3.8  2.1  57   280 false(unreach-call) 8.9 4.8 89 310 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .11 .096 .86 17 0      0      false(unreach-call) 3.5  2.0  59   270 false(unreach-call) 9.2 4.8 92 320 - -
loop-acceleration/simple_false-unreach-call4.i error (1) 0 wit inspect 290    290     3000    15000 .88   700      error (invalid witness file) .55 .35 12   43 error (invalid witness file) 6.5 3.5 84 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .40 .39  3.3  17 .029  .061  false(unreach-call) 4.4  2.4  96   280 false(unreach-call) 13   6.9 250 360 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .36 .35  3.6  17 .029  0      false(unreach-call) 3.9  2.2  33   280 false(unreach-call) 12   6.3 260 360 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 10    10     120    1100 1.6    0      - - true 16    8.1  120   570 timeout 960   800   14000 4600
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 23    23     260    2200 4.7    0      - - out of memory 340    320    5700   7000 timeout 960   790   12000 4700
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 7.9  7.9   98    630 3.0    0      - - timeout 910    880    21000   5400 timeout 960   850   21000 4600
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 7.7  7.7   110    630 3.0    0      - - out of memory 370    350    7800   7000 timeout 960   840   14000 4000
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 1.6  1.5   15    19 1.4    0      - - true 17    8.8  260   540 timeout 960   810   21000 3000
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 1.9  1.9   21    50 .48   0      - - true 26    18    330   700 true 620   520   9700 1300
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .42 .42  4.6  24 .070  0      - - true 13    7.2  160   430 true 41   27   800 700
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 260    260     3100    15000 3.4    .0041 - - error (invalid witness file) .56 .35 8.5 44 error (invalid witness file) 5.8 3.1 73 310
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 100    100     850    270 2.2    0      - - out of memory 410    390    7600   7000 true 17   10   280 500
loop-acceleration/nested_true-unreach-call1.i out of memory 0 wit inspect 310    310     4300    15000 13      .012  - - error (invalid witness file) .71 .44 8.9 43 error (invalid witness file) 6.5 3.4 130 310
loop-acceleration/overflow_true-unreach-call1.i error (1) 0 wit inspect 280    280     3400    15000 1.3    710      - - error (invalid witness file) .63 .40 8.2 40 error (invalid witness file) 5.9 3.1 120 300
loop-acceleration/phases_true-unreach-call1.i out of memory 0 wit inspect 310    310     4900    15000 .73   .025  - - error (invalid witness file) .54 .36 11   43 error (invalid witness file) 6.5 3.4 120 310
loop-acceleration/phases_true-unreach-call2_false-termination.i error (42) 0 wit inspect 850    850     7900    5900 2.7    0      - - error (invalid witness file) .53 .33 11   41 error (invalid witness file) 5.9 3.1 120 290
loop-acceleration/simple_true-unreach-call1.i error (1) 0 wit inspect 280    280     3500    15000 .88   700      - - error (invalid witness file) .61 .38 8.3 39 error (invalid witness file) 5.4 2.9 110 280
loop-acceleration/simple_true-unreach-call2_true-termination.i error (42) 0 wit inspect 850    850     7300    4600 2.9    .26   - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.3 3.3 130 310
loop-acceleration/simple_true-unreach-call3_true-termination.i error (42) 0 wit inspect 850    850     3300    11000 3.2    0      - - error (invalid witness file) .56 .35 8.5 40 error (invalid witness file) 6.2 3.2 110 300
loop-acceleration/simple_true-unreach-call4.i error (1) 0 wit inspect 290    290     3700    15000 1.4    700      - - error (invalid witness file) .70 .44 10   44 error (invalid witness file) 6.0 3.2 130 300
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .41 .40  3.8  17 .029  0      - - true 7.3  5.2  180   400 true 59   53   1400 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .42 .42  4.8  17 .029  0      - - true 5.6  3.1  54   280 true 11   5.8 150 390
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12 .12  1.1  18 0      0      false(unreach-call) 4.0  2.2  53   280 false(unreach-call) 9.2 4.9 110 330 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     12000    200 .35   0      - - error (invalid witness file) .61 .40 9.7 41 error (invalid witness file) 5.6 3.0 110 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     5700    11000 10      0      - - error (invalid witness file) .61 .39 11   41 error (invalid witness file) 6.1 3.2 120 300
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i error (42) 0 wit inspect 850    850     9400    470 .66   0      - - error (invalid witness file) .54 .35 9.1 40 error (invalid witness file) 6.0 3.1 130 300
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     9000    470 1.1    0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.5 2.9 100 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     8900    680 1.4    0      - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 5.9 3.1 95 290
loop-invgen/down_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     4800    3600 11      0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 110 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6200    1600 18      0      - - error (invalid witness file) .53 .35 11   39 error (invalid witness file) 5.8 3.1 110 300
loop-invgen/half_2_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6700    1400 11      0      - - error (invalid witness file) .57 .37 9.4 43 error (invalid witness file) 6.7 3.5 130 310
loop-invgen/heapsort_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     7100    12000 11      0      - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.1 3.2 120 300
loop-invgen/id_build_true-unreach-call_true-termination.i error (134) 0 wit inspect 200    200     1700    12000 13      0      - - error (invalid witness file) .69 .42 8.2 40 error (invalid witness file) 6.3 3.3 100 310
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .20 .20  1.8  17 0      0      - - true 5.9  3.3  94   290 true 11   6.1 140 370
loop-invgen/nest-if3_true-unreach-call_true-termination.i error (134) 0 wit inspect 710    710     4300    13000 4.4    0      - - error (invalid witness file) .65 .42 9.2 44 error (invalid witness file) 5.6 3.0 110 290
loop-invgen/nested6_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     2900    470 24      0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.7 3.1 130 300
loop-invgen/nested9_true-unreach-call_true-termination.i error (134) 0 wit inspect 170    170     1400    12000 7.9    0      - - error (invalid witness file) .73 .46 7.5 41 error (invalid witness file) 5.8 3.1 94 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     10000    4500 9.1    0      - - error (invalid witness file) .56 .34 9.7 40 error (invalid witness file) 6.1 3.3 130 300
loop-invgen/seq_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6100    600 3.0    .13   - - error (invalid witness file) .65 .41 8.5 41 error (invalid witness file) 5.5 2.9 120 280
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     4600    9400 60      0      - - error (invalid witness file) .70 .45 7.2 42 error (invalid witness file) 5.5 2.9 110 300
loop-invgen/up_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     9000    1400 5.1    0      - - error (invalid witness file) .57 .37 11   40 error (invalid witness file) 5.8 3.1 110 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 14    14     160    150 2.0    0      - - out of memory 510    490    9800   7000 true 17   9.9 250 520
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     9200    350 .76   0      - - error (invalid witness file) .64 .41 6.8 39 error (invalid witness file) 5.5 3.0 95 290
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .28 .27  2.9  17 .012  0      - - true 5.3  3.0  49   280 true 11   5.8 210 390
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     5200    4000 6.4    0      - - error (invalid witness file) .65 .42 7.3 40 error (invalid witness file) 6.3 3.3 100 300
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .96 .95  11    17 .40   0      - - true 7.6  4.0  150   320 true 11   5.8 140 370
loop-lit/css2003_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     5100    820 8.4    0      - - error (invalid witness file) .54 .35 11   42 error (invalid witness file) 6.0 3.2 120 290
loop-lit/ddlm2013_true-unreach-call.i error (42) 0 wit inspect 850    850     9000    1300 4.2    0      - - error (invalid witness file) .61 .39 10   41 error (invalid witness file) 6.5 3.4 130 310
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 1.0  1.0   11    17 .14   0      - - true 79    71    1400   790 true 100   64   2100 1400
loop-lit/gj2007b_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     9000    2800 5.7    0      - - error (invalid witness file) .69 .43 9.3 45 error (invalid witness file) 7.3 3.8 120 310
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .97 .96  11    19 .22   0      - - true 63    54    1200   1100 true 88   52   1600 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 220    220     2000    620 4.5    0      - - timeout 900    890    19000   1600 true 27   19   680 680
loop-lit/hhk2008_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     11000    260 .36   0      - - error (invalid witness file) .73 .47 9.3 44 error (invalid witness file) 5.9 3.1 140 300
loop-lit/jm2006_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     4400    6900 4.5    0      - - error (invalid witness file) .49 .31 9.6 40 error (invalid witness file) 5.7 3.0 110 310
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     3900    5300 5.6    .10   - - error (invalid witness file) .59 .38 9.8 41 error (invalid witness file) 5.5 3.0 88 300
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 850    850     8000    6000 .43   0      - - error (invalid witness file) .64 .41 6.9 40 error (invalid witness file) 5.7 3.0 120 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .14 .13  .79 17 0      0      false(unreach-call) 3.8  2.1  60   270 false(unreach-call) 7.4 3.9 150 310 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 87    87     1100    3100 27      0      - - true 20    11    370   1300 timeout 960   800   15000 3900
loop-new/count_by_1_variant_true-unreach-call_true-termination.i out of memory 0 wit inspect 130    130     1400    15000 4.8    0      - - error (invalid witness file) .73 .46 8.8 44 error (invalid witness file) 5.9 3.1 91 290
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect 44    44     530    1600 14      0      - - out of memory 340    320    4700   7000 timeout 960   800   18000 4600
loop-new/count_by_k_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     3500    10000 3.2    0      - - error (invalid witness file) .52 .32 13   40 error (invalid witness file) 5.5 2.9 84 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     7300    1500 6.6    0      - - error (invalid witness file) .71 .45 8.3 42 error (invalid witness file) 5.9 3.1 110 290
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 wit inspect 19    19     200    130 2.0    0      - - timeout 910    890    27000   5500 timeout 960   820   14000 2800
loop-new/half_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     3500    8200 4.7    0      - - error (invalid witness file) .53 .33 9.8 41 error (invalid witness file) 5.1 2.8 75 290
loop-new/nested_true-unreach-call_true-termination.i error (42) 0 wit inspect 850    850     6100    3800 43      0      - - error (invalid witness file) .54 .35 9.5 41 error (invalid witness file) 7.5 4.0 100 300
loop-industry-pattern/aiob_1_true-unreach-call.c true 1 wit inspect 3.6  3.6   34    24 .59   0      - - exception 4.6  2.5  80   270 error 14   7.3 130 310
loop-industry-pattern/aiob_2_true-unreach-call.c true 1 wit inspect 3.9  3.8   35    24 .59   0      - - exception 4.4  2.4  92   270 error 12   6.5 240 300
loop-industry-pattern/aiob_3_true-unreach-call.c true 1 wit inspect 3.7  3.6   33    24 .59   0      - - exception 5.3  2.9  67   270 error 12   6.1 190 310
loop-industry-pattern/aiob_4_true-unreach-call.c true 1 wit inspect 3.9  3.9   32    23 .63   0      - - exception 5.6  3.0  58   270 error 13   6.9 250 320
loop-industry-pattern/mod3_true-unreach-call.c error (42) 0 wit inspect 850    850     9900    200 .29   0      - - error (invalid witness file) .62 .39 8.0 40 error (invalid witness file) 5.9 3.2 97 300
loop-industry-pattern/nested_true-unreach-call.c error (1) 0 wit inspect 360    360     4000    15000 210      11      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 5.5 3.0 96 290
loop-industry-pattern/ofuf_1_true-unreach-call.c error (42) 0 wit inspect 850    850     13000    510 1.2    0      - - error (invalid witness file) .56 .35 10   41 error (invalid witness file) 5.8 3.1 100 300
loop-industry-pattern/ofuf_2_true-unreach-call.c error (42) 0 wit inspect 850    850     9400    380 .79   0      - - error (invalid witness file) .58 .39 9.8 40 error (invalid witness file) 6.1 3.2 130 300
loop-industry-pattern/ofuf_3_true-unreach-call.c error (42) 0 wit inspect 850    850     9500    570 1.2    0      - - error (invalid witness file) .67 .44 7.7 39 error (invalid witness file) 7.6 4.0 79 300
loop-industry-pattern/ofuf_4_true-unreach-call.c error (42) 0 wit inspect 850    850     9200    500 .91   0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 5.6 2.9 92 310
loop-industry-pattern/ofuf_5_true-unreach-call.c error (42) 0 wit inspect 850    850     9900    530 .91   0      - - error (invalid witness file) .59 .38 8.4 40 error (invalid witness file) 5.9 3.1 110 300
loops/heavy_true-unreach-call.c error (42) 0 wit inspect 850    850     9500    3600 .012  0      - - error (invalid witness file) .55 .36 9.0 40 error (invalid witness file) 6.0 3.2 92 290
loops/compact_false-unreach-call.c out of memory 0 wit inspect 130    130     1700    15000 27      0      error (invalid witness file) .59 .39 11   42 error (invalid witness file) 6.1 3.2 120 300 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 410    410     5200    15000 .012  0      error (invalid witness file) .49 .32 9.7 41 error (invalid witness file) 6.0 3.2 130 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 107 49000 49000 430000 570000 970   3500      156 530 300 8500 30000   156 1100 680 17000 62000   156 6700 6400 140000 74000   156 11000 9000 180000 82000  
    correct results 67 96 500 500 5000 8100 47   1.0    36 220 120 3800 13000   34 790 460 11000 32000   21 3200 3000 66000 31000   26 4700 3800 83000 30000  
        correct true 29 58 460 460 4600 5900 44   0      2 0 0 0 0   0 0 0 0 0   21 3200 3000 66000 31000   26 4700 3800 83000 30000  
        correct false 38 38 40 40 460 2300 3.7 1.0    34 220 120 3800 13000   34 790 460 11000 32000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 15 11 250 250 3100 12000 160   .59   1 300 170 4600 16000   0 300 200 4500 27000   0 3500 3400 78000 40000   0 5900 5000 93000 33000  
        correct-unconfirmed true 11 11 130 130 1500 5500 47   .58   1 0 0 0 0   0 0 0 0 0   0 3500 3400 78000 40000   0 5900 5000 93000 33000  
        correct-unconfirmed false 4 0 120 120 1600 6200 110   .0041 0 300 170 4600 16000   0 300 200 4500 27000   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) 107
Run set sv-comp17.ReachSafety-Loops