Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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 1.1  1.1  14   76 4.3  .045  false(unreach-call) 4.1  2.3  72   280 false(unreach-call) 7.9 4.2 150 330 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 0 wit inspect 3.0  3.0  42   240 1.7  .50   true 11    6.0  120   330 error 12   6.5 200 310 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .55 .55 7.1 75 1.7  0      false(unreach-call) 3.9  2.2  73   270 false(unreach-call) 8.7 4.6 70 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 0 wit inspect 2.9  2.9  34   190 6.8  0      true 5.0  2.7  110   280 true 73   51   860 1100 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.3  1.4  15   110 4.2  34      false(unreach-call) 4.9  2.7  59   290 false(unreach-call) 7.9 4.2 140 320 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6  3.6  56   130 9.4  0      true 5.6  3.1  61   280 false(unreach-call) 22   13   330 530 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.9  1.9  26   130 6.8  0      true 4.6  2.5  79   280 false(unreach-call) 11   6.3 220 380 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 16    16    250   76 52    .020  true 6.2  3.3  120   290 timeout 97   85   2500 730 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 7.1  7.0  100   350 18    0      true 7.3  4.0  88   290 out of memory 51   40   620 7000 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 480    480    5400   180 3.4  0      true 5.3  2.9  59   280 false(unreach-call) 14   7.6 150 360 - -
loops/n.c24_false-unreach-call.i unknown 0 wit inspect 900    900    7200   1400 17    0      error (invalid witness file) .68 .44 8.7 43 error (invalid witness file) 7.3 3.8 82 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .54 .54 6.4 76 1.7  0      false(unreach-call) 5.0  2.7  45   270 false(unreach-call) 8.5 4.6 120 330 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.2  1.2  14   76 4.3  0      false(unreach-call) 5.2  2.9  52   290 false(unreach-call) 7.4 4.0 150 330 - -
loops/s3_false-unreach-call.i unknown 0 wit inspect 890    900    11000   1600 15    0      error (invalid witness file) .59 .39 6.0 39 error (invalid witness file) 7.2 3.8 85 300 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.1  4.0  61   190 14    0      false(unreach-call) 9.1  4.9  97   300 false(unreach-call) 35   18   350 490 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.9  4.0  46   110 17    34      false(unreach-call) 5.0  2.8  78   300 false(unreach-call) 10   5.4 150 350 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.7  2.7  38   76 12    0      false(unreach-call) 5.4  2.9  60   290 false(unreach-call) 11   5.9 130 340 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.9  5.9  77   76 27    0      false(unreach-call) 6.1  3.4  57   290 false(unreach-call) 16   9.0 160 420 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.7  5.7  72   75 27    .10   false(unreach-call) 7.0  3.8  81   290 false(unreach-call) 16   8.9 220 480 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.6  4.6  57   76 22    0      false(unreach-call) 5.3  2.9  62   290 false(unreach-call) 10   5.5 170 340 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 1.4  1.3  18   160 4.3  0      true 4.9  2.7  52   270 false(unreach-call) 12   6.5 170 360 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .54 .54 6.0 75 1.7  0      false(unreach-call) 4.5  2.5  45   280 false(unreach-call) 8.8 4.7 100 310 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40 .40 4.7 75 .85 0      false(unreach-call) 4.8  2.6  62   280 false(unreach-call) 10   5.4 98 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .56 .55 6.4 75 1.7  0      false(unreach-call) 4.3  2.4  58   270 false(unreach-call) 8.3 4.5 130 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .61 .61 6.6 160 1.7  0      false(unreach-call) 5.0  2.8  60   280 false(unreach-call) 10   5.5 120 340 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36 .36 4.1 75 .85 0      false(unreach-call) 4.7  2.6  46   270 false(unreach-call) 7.2 3.9 130 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .38 .38 4.6 76 .85 0      false(unreach-call) 5.0  2.8  62   280 false(unreach-call) 7.2 3.9 130 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.4  1.4  21   75 5.9  .20   true 3.6  2.0  82   270 false(unreach-call) 8.9 4.8 110 320 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.1  2.0  25   130 6.8  0      false(unreach-call) 6.0  3.3  62   300 true 9.4 5.1 120 340 - -
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect 13    13    160   210 27    0      timeout 92    79    1500   790 timeout 98   59   820 4200 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .37 .37 4.2 75 .84 0      false(unreach-call) 3.7  2.1  82   270 false(unreach-call) 7.0 3.7 110 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 4.2  2.3  38   280 4.2  0      - - true 4.5  2.5  80   300 true 9.8 5.3 110 360
loops/bubble_sort_true-unreach-call.i unknown 0 wit inspect 900    900    10000   450 72    .086  - - error (invalid witness file) .54 .35 13   41 error (invalid witness file) 5.5 2.9 66 300
loops/count_up_down_true-unreach-call_true-termination.i unknown 0 wit inspect 69    68    900   75 260    0      - - error (invalid witness file) .60 .39 9.7 39 error (invalid witness file) 5.7 3.0 65 300
loops/eureka_01_true-unreach-call.i unknown 0 wit inspect 890    900    7300   330 19    0      - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.2 2.8 99 290
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 6.1  4.4  64   260 14    .0041 - - true 440    420    6700   5100 true 36   21   370 570
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 wit inspect 37    37    510   75 170    0      - - error (invalid witness file) .49 .32 8.0 40 error (invalid witness file) 5.9 3.1 86 300
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 wit inspect 37    37    400   75 170    0      - - error (invalid witness file) .56 .36 15   42 error (invalid witness file) 5.7 3.0 72 290
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect 890    900    10000   160 17    0      - - error (invalid witness file) .68 .42 5.7 42 error (invalid witness file) 5.8 3.0 73 300
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 17    13    180   460 14    .10   - - true 25    15    290   590 true 41   27   520 780
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect 110    110    1400   76 260    .10   - - error (invalid witness file) .63 .41 7.8 40 error (invalid witness file) 5.9 3.2 100 310
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 9.2  7.2  120   350 16    0      - - timeout 910    860    17000   5700 out of memory 57   45   610 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 14    11    170   370 4.2  0      - - true 9.9  7.3  160   420 true 12   6.5 160 370
loops/n.c11_true-unreach-call_false-termination.i unknown 0 wit inspect 57    57    720   75 260    0      - - error (invalid witness file) .57 .37 7.6 40 error (invalid witness file) 5.4 2.9 70 300
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 4.5  2.4  41   280 3.4  0      - - true 4.5  2.5  70   270 true 170   160   4200 750
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 4.4  2.3  48   280 3.4  0      - - true 4.9  2.8  57   280 true 230   210   3800 770
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 4.8  2.6  50   270 4.2  0      - - true 6.4  3.4  120   290 true 13   6.7 120 370
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 300    230    2900   3300 4.2  0      - - true 36    24    320   870 timeout 960   920   13000 1600
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 180    170    2100   1400 4.2  .14   - - true 5.0  2.8  62   280 true 7.6 4.0 51 310
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 3.3  1.9  31   260 4.2  0      - - true 5.5  3.0  40   280 true 11   6.0 170 440
loops/sum_array_true-unreach-call.i unknown 0 wit inspect 890    900    8500   240 54    .13   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.0 2.7 63 290
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 4.0  2.2  35   280 4.2  0      - - true 4.9  2.7  54   270 true 8.1 4.3 99 350
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 4.0  2.1  38   270 4.2  0      - - true 5.7  3.2  50   280 true 8.5 4.6 90 320
loops/trex01_true-unreach-call_true-termination.i unknown 0 wit inspect 820    820    8800   160 260    0      - - error (invalid witness file) .58 .36 10   42 error (invalid witness file) 5.8 3.1 70 300
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 3.6  2.1  35   260 3.4  0      - - true 5.2  2.9  54   270 true 7.2 3.9 79 320
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 3.9  2.1  36   260 3.4  0      - - true 4.8  2.7  71   280 true 7.7 4.1 150 320
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 4.5  2.4  39   280 4.2  0      - - true 4.8  2.6  62   280 true 7.5 4.0 83 320
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 4.0  2.1  37   280 3.4  0      - - out of memory 280    270    4000   7000 true 9.4 5.1 95 350
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 160    150    2000   2400 22    0      - - true 11    6.0  120   350 true 8.6 4.7 120 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 5.1  2.6  44   290 4.2  0      - - true 4.7  2.6  80   290 true 7.6 4.1 130 330
loops/vogal_true-unreach-call.i true 2 wit inspect 330    280    3500   2100 14    .10   - - true 120    110    1200   1200 true 280   220   3700 3300
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 3.1  1.7  29   260 3.4  0      - - true 4.8  2.7  59   270 true 7.1 3.8 58 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 3.2  1.7  28   250 3.4  0      - - true 4.3  2.4  69   280 true 7.1 3.8 110 310
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 3.3  1.8  30   260 3.4  .0041 - - true 4.7  2.6  43   280 true 7.9 4.2 160 320
loop-acceleration/array_false-unreach-call1_true-termination.i unknown 0 wit inspect 900    900    9400   230 110    0      error (invalid witness file) .71 .45 7.2 41 error (invalid witness file) 6.1 3.2 120 300 - -
loop-acceleration/array_false-unreach-call2_true-termination.i unknown 0 wit inspect 890    900    9000   610 160    0      error (invalid witness file) .58 .37 12   44 error (invalid witness file) 6.3 3.3 110 300 - -
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900    850    9300   8300 5.5  0      timeout 92    81    2800   2900 timeout 96   54   820 960 - -
loop-acceleration/const_false-unreach-call1.i unknown 0 wit inspect 54    53    670   75 260    0      error (invalid witness file) .53 .34 10   39 error (invalid witness file) 6.5 3.4 100 300 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 32    31    410   75 130    0      false(unreach-call) 6.3  3.4  100   290 timeout 98   55   1000 6900 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 wit inspect 36    35    390   75 170    0      error (invalid witness file) .55 .36 11   39 error (invalid witness file) 5.7 3.0 88 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .53 .53 6.5 75 1.7  0      false(unreach-call) 4.0  2.3  65   270 false(unreach-call) 7.0 3.8 140 310 - -
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900    900    8100   1400 290    0      error (invalid witness file) .55 .35 7.3 40 error (invalid witness file) 5.9 3.2 130 300 - -
loop-acceleration/phases_false-unreach-call1.i unknown 0 wit inspect 150    150    1800   75 260    0      error (invalid witness file) .48 .31 10   39 error (invalid witness file) 6.6 3.5 120 310 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .55 .54 7.0 76 1.7  0      false(unreach-call) 4.9  2.7  45   270 false(unreach-call) 7.3 3.9 130 320 - -
loop-acceleration/simple_false-unreach-call1.i unknown 0 wit inspect 54    53    660   75 260    0      error (invalid witness file) .63 .40 8.1 41 error (invalid witness file) 6.1 3.2 75 310 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .38 .38 4.5 75 .84 0      false(unreach-call) 4.6  2.5  53   280 false(unreach-call) 9.3 5.0 80 310 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .52 .52 7.2 75 1.7  0      false(unreach-call) 3.9  2.2  61   280 false(unreach-call) 7.0 3.7 110 320 - -
loop-acceleration/simple_false-unreach-call4.i unknown 0 wit inspect 53    53    670   75 260    0      error (invalid witness file) .61 .40 8.1 40 error (invalid witness file) 6.0 3.2 96 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.5  3.5  46   75 17    0      false(unreach-call) 5.1  2.8  58   270 false(unreach-call) 11   6.2 180 350 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.5  3.5  44   75 17    0      false(unreach-call) 4.8  2.7  41   280 false(unreach-call) 13   6.8 200 390 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 99    93    1300   550 4.2  .14   - - true 4.8  2.8  54   280 timeout 960   800   14000 4000
loop-acceleration/array_true-unreach-call2_true-termination.i unknown 0 wit inspect 890    900    12000   280 150    0      - - error (invalid witness file) .54 .34 14   41 error (invalid witness file) 5.9 3.1 92 300
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 14    7.1  120   1200 4.2  0      - - timeout 910    890    14000   5000 timeout 960   850   14000 2900
loop-acceleration/array_true-unreach-call4_true-termination.i unknown 0 wit inspect 890    900    11000   220 120    0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.3 3.3 130 300
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 7.4  3.7  65   430 4.2  0      - - true 4.0  2.2  39   270 timeout 960   810   13000 2600
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 270    260    3500   2900 250    0      - - true 15    11    350   530 true 750   640   11000 1700
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 8.9  5.9  99   290 14    0      - - true 9.8  5.6  110   340 true 41   28   770 710
loop-acceleration/functions_true-unreach-call1_true-termination.i unknown 0 wit inspect 36    35    440   75 170    0      - - error (invalid witness file) .57 .38 9.8 40 error (invalid witness file) 5.8 3.1 90 290
loop-acceleration/multivar_true-unreach-call1_true-termination.i unknown 0 wit inspect 63    62    750   75 260    0      - - error (invalid witness file) .58 .38 8.9 40 error (invalid witness file) 6.5 3.5 79 300
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 360    340    4100   4200 4.2  0      - - true 4.9  2.7  47   280 timeout 960   850   14000 4700
loop-acceleration/overflow_true-unreach-call1.i unknown 0 wit inspect 53    53    590   75 260    0      - - error (invalid witness file) .48 .32 9.4 40 error (invalid witness file) 5.6 3.0 86 300
loop-acceleration/phases_true-unreach-call1.i unknown 0 wit inspect 130    130    1900   75 260    0      - - error (invalid witness file) .59 .38 11   42 error (invalid witness file) 6.5 3.4 63 300
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 5.3  3.5  53   280 4.2  0      - - timeout 900    900    16000   410 true 8.8 5.1 100 330
loop-acceleration/simple_true-unreach-call1.i unknown 0 wit inspect 53    52    640   75 260    0      - - error (invalid witness file) .49 .32 6.5 39 error (invalid witness file) 5.9 3.1 98 300
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 3.6  1.9  35   280 3.4  0      - - true 4.4  2.5  70   270 true 7.0 3.8 85 310
loop-acceleration/simple_true-unreach-call3_true-termination.i unknown 0 wit inspect 56    56    750   110 260    33      - - error (invalid witness file) .59 .36 11   44 error (invalid witness file) 5.6 3.0 72 310
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 150    150    1600   1300 4.2  0      - - true 3.8  2.2  82   270 true 9.0 4.9 55 310
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 5.8  4.4  63   260 17    0      - - true 8.1  5.8  150   400 true 57   51   1200 420
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 3.2  1.9  30   260 4.2  0      - - true 4.1  2.3  86   270 true 10   5.5 97 360
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .59 .59 6.9 76 1.7  0      false(unreach-call) 4.4  2.4  76   280 false(unreach-call) 7.5 4.0 150 330 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    12000   76 210    0      - - error (invalid witness file) .57 .37 8.8 39 error (invalid witness file) 5.8 3.1 54 290
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i unknown 0 wit inspect 54    54    670   76 170    0      - - error (invalid witness file) .59 .37 9.2 42 error (invalid witness file) 5.8 3.1 71 300
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i unknown 0 wit inspect 890    900    13000   120 16    0      - - error (invalid witness file) .52 .33 8.9 41 error (invalid witness file) 5.5 3.0 73 300
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 wit inspect 890    900    13000   100 45    0      - - error (invalid witness file) .57 .37 11   40 error (invalid witness file) 5.4 2.9 94 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    12000   100 60    0      - - error (invalid witness file) .52 .34 13   39 error (invalid witness file) 5.5 3.0 82 300
loop-invgen/down_true-unreach-call_true-termination.i unknown 0 wit inspect 89    88    1100   100 170    0      - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 5.1 2.7 76 290
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i unknown 0 wit inspect 91    90    1100   130 260    0      - - error (invalid witness file) .53 .34 10   43 error (invalid witness file) 7.2 3.7 64 320
loop-invgen/half_2_true-unreach-call_true-termination.i unknown 0 wit inspect 170    170    2100   110 260    0      - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 5.8 3.1 100 300
loop-invgen/heapsort_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    12000   710 40    0      - - error (invalid witness file) .52 .33 14   39 error (invalid witness file) 6.1 3.2 96 290
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 210    200    2400   1000 4.3  0      - - true 5.9  3.3  59   290 false(unreach-call) 7.8 4.1 91 330
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 4.5  2.6  41   310 2.6  34      - - true 4.9  2.7  84   290 true 12   6.3 250 400
loop-invgen/nest-if3_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    7700   320 54    0      - - error (invalid witness file) .50 .32 8.4 40 error (invalid witness file) 6.1 3.2 56 300
loop-invgen/nested6_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    8400   4100 55    0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.0 3.2 97 300
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900    560    10000   6100 4.4  0      - - timeout 900    890    13000   5200 true 10   5.7 88 380
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 wit inspect 230    230    3000   82 260    0      - - error (invalid witness file) .54 .36 13   45 error (invalid witness file) 5.6 3.0 74 300
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900    510    8800   10000 4.2  0      - - out of memory 630    580    9700   7000 timeout 960   790   12000 2900
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    10000   15000 9.4  34      - - error (invalid witness file) .69 .44 8.1 41 error (invalid witness file) 5.9 3.1 88 300
loop-invgen/up_true-unreach-call_true-termination.i unknown 0 wit inspect 71    70    860   100 170    0      - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.2 3.2 96 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i unknown 0 wit inspect 86    85    1100   76 260    0      - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.1 3.2 57 300
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    780    10000   2200 4.2  0      - - timeout 900    900    18000   860 true 15   8.4 160 410
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 3.2  1.9  29   270 4.2  0      - - true 5.4  3.0  59   280 true 9.7 5.2 120 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    540    9100   8500 4.2  0      - - out of memory 360    350    8400   7000 true 10   5.6 120 370
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.5  2.2  42   260 4.2  0      - - true 5.5  3.0  62   280 true 9.9 5.3 180 320
loop-lit/css2003_true-unreach-call_true-termination.c.i unknown 0 wit inspect 51    50    660   77 190    0      - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 5.6 3.0 90 300
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect 210    210    2200   310 260    0      - - error (invalid witness file) .65 .42 7.3 39 error (invalid witness file) 7.6 4.0 94 310
loop-lit/gj2007_true-unreach-call_true-termination.c.i unknown 0 wit inspect 36    36    420   76 170    0      - - true 80    71    1100   770 true 100   63   1900 1600
loop-lit/gj2007b_true-unreach-call_true-termination.c.i unknown 0 wit inspect 210    210    2800   130 260    0      - - error (invalid witness file) .51 .34 9.2 40 error (invalid witness file) 5.1 2.7 67 280
loop-lit/gr2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 140    140    1800   120 260    0      - - true 54    46    950   1100 true 81   48   1200 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900    900    7100   620 250    .34   - - error (invalid witness file) .62 .39 8.2 40 error (invalid witness file) 5.3 2.8 65 280
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    540    8800   8000 4.2  0      - - out of memory 330    320    5100   7000 true 10   5.4 110 370
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.8  2.2  38   270 4.2  0      - - out of memory 340    330    5800   7000 true 12   6.7 110 440
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    530    8300   10000 4.2  0      - - out of memory 300    300    6300   7000 true 13   7.3 140 390
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 890    900    11000   100 42    0      - - error (invalid witness file) .52 .34 9.1 40 error (invalid witness file) 5.5 3.0 77 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 16    16    190   79 1.7  0      false(unreach-call) 4.0  2.2  41   290 false(unreach-call) 9.4 5.0 110 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 350    340    4000   3500 3.4  0      - - true 4.9  2.7  56   280 timeout 960   800   10000 3900
loop-new/count_by_1_variant_true-unreach-call_true-termination.i unknown 0 wit inspect 37    36    430   75 170    0      - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 6.5 3.4 74 310
loop-new/count_by_2_true-unreach-call_true-termination.i unknown 0 wit inspect 57    56    690   75 260    0      - - error (invalid witness file) .61 .39 6.6 40 error (invalid witness file) 5.5 3.0 48 300
loop-new/count_by_k_true-unreach-call_true-termination.i unknown 0 wit inspect 78    77    1100   75 260    0      - - error (invalid witness file) .58 .36 10   40 error (invalid witness file) 5.7 3.0 76 310
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900    600    10000   3800 4.2  .0041 - - timeout 900    900    23000   1300 timeout 960   800   15000 4800
loop-new/gauss_sum_true-unreach-call_true-termination.i unknown 0 wit inspect 550    550    6200   120 260    0      - - error (invalid witness file) .64 .41 8.6 39 error (invalid witness file) 6.3 3.3 96 300
loop-new/half_true-unreach-call_true-termination.i unknown 0 wit inspect 74    73    990   76 260    0      - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 7.4 3.9 53 300
loop-new/nested_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    7400   480 110    0      - - error (invalid witness file) .66 .42 7.7 39 error (invalid witness file) 5.7 3.0 87 290
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect 58    48    710   620 110    0      - - true 31    25    580   590 error 10   5.6 160 300
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect 59    48    690   640 110    0      - - true 26    20    450   590 error 11   5.8 190 310
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect 59    48    810   620 110    0      - - true 24    19    270   580 error 9.8 5.2 91 300
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect 46    36    520   620 70    .27   - - true 25    20    600   540 error 11   5.8 130 330
loop-industry-pattern/mod3_true-unreach-call.c unknown 0 wit inspect 890    900    11000   90 19    0      - - error (invalid witness file) .53 .35 8.3 40 error (invalid witness file) 5.7 3.1 92 290
loop-industry-pattern/nested_true-unreach-call.c unknown 0 wit inspect 900    900    7400   530 130    0      - - error (invalid witness file) .53 .33 12   41 error (invalid witness file) 7.0 3.7 83 300
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect 500    490    6900   600 88    0      - - error (invalid witness file) .57 .36 13   45 error (invalid witness file) 6.4 3.3 52 320
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect 500    490    7500   600 88    .22   - - error (invalid witness file) .48 .31 8.7 40 error (invalid witness file) 6.0 3.1 88 300
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect 490    490    5800   600 88    0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.5 3.5 91 300
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect 480    470    5500   590 87    34      - - error (invalid witness file) .62 .40 8.1 40 error (invalid witness file) 5.7 3.0 93 290
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect 470    470    7000   560 88    0      - - error (invalid witness file) .66 .43 9.9 42 error (invalid witness file) 6.7 3.5 100 310
loops/heavy_true-unreach-call.c true 1 wit inspect 330    320    3700   5300 4.4  0      - - timeout 900    890    18000   4000 timeout 960   880   9900 6500
loops/compact_false-unreach-call.c unknown 0 wit inspect 78    77    990   100 260    0      error (invalid witness file) .48 .31 12   39 error (invalid witness file) 7.0 3.7 100 300 - -
loops/heavy_false-unreach-call.c unknown 0 wit inspect 890    900    10000   5400 17    0      error (invalid witness file) .54 .33 6.2 42 error (invalid witness file) 5.8 3.1 100 290 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 156 120 40000 37000 450000 140000 12000 210    156 380 270 6900 15000   156 950 580 13000 36000   156 9600 9300 170000 88000   156 11000 9300 150000 80000  
    correct results 75 117 3400 3100 38000 36000 1200 100    33 160 91 2100 9300   32 450 240 5800 18000   39 2400 2300 38000 34000   33 6700 5700 95000 36000  
        correct true 42 84 2800 2500 32000 33000 860 35    5 0 0 0 0   1 0 0 0 0   39 2400 2300 38000 34000   32 6700 5700 95000 36000  
        correct false 33 33 580 580 6700 3100 350 68    28 160 91 2100 9300   31 450 240 5800 18000   0 0 0 0 0   1 0 0 0 0  
    correct-unconfimed results 8 3 390 380 4600 7900 130 .52 4 120 95 1900 2000   1 330 240 5000 13000   0 2700 2600 49000 15000   0 2000 1800 25000 16000  
        correct-unconfirmed true 3 3 350 340 4000 6900 25 0    4 0 0 0 0   1 0 0 0 0   0 2700 2600 49000 15000   0 2000 1800 25000 16000  
        correct-unconfirmed false 5 0 42 42 590 1100 110 .52 0 120 95 1900 2000   0 330 240 5000 13000   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) 120
Run set sv-comp17.ReachSafety-Loops