Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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 .19 .19 1.9 23 1.7  .094  false(unreach-call) 4.2  2.4  64   280 false(unreach-call) 7.5 4.0 110 330 - -
loops/bubble_sort_false-unreach-call.i out of memory 0 wit inspect 230    230    1900   15000 .84 0      error (invalid witness file) .59 .39 10   44 error (invalid witness file) 5.8 3.1 100 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.2  1.2  13   130 1.7  0      false(unreach-call) 4.5  2.5  52   270 false(unreach-call) 6.7 3.6 91 310 - -
loops/eureka_01_false-unreach-call.i timeout 0 wit inspect 900    900    6800   7800 .84 0      error (invalid witness file) .47 .31 9.3 39 error (invalid witness file) 5.8 3.1 110 300 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 890    890    9200   4300 1.7  0      false(unreach-call) 17    9.3  280   740 false(unreach-call) 23   12   240 1100 - -
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 wit inspect 900    900    7800   3000 .84 0      error (invalid witness file) .66 .42 7.7 39 error (invalid witness file) 5.8 3.1 91 290 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 890    890    13000   1700 1.7  0      true 3.9  2.2  81   270 false(unreach-call) 11   6.2 140 370 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 1.3  1.3  17   85 1.7  .094  true 5.5  3.0  130   280 timeout 97   83   1100 700 - -
loops/ludcmp_false-unreach-call.i out of memory 0 wit inspect 9.7  9.4  120   15000 .84 0      error (invalid witness file) .53 .34 11   43 error (invalid witness file) 5.8 3.1 110 290 - -
loops/matrix_false-unreach-call_true-termination.i timeout 0 wit inspect 900    900    7100   6500 .84 0      error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.2 3.2 97 300 - -
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 80    80    760   15000 .84 0      error (invalid witness file) .61 .39 9.1 40 error (invalid witness file) 5.6 3.0 91 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 1.8  1.8  20   140 1.7  0      false(unreach-call) 4.5  2.5  46   280 false(unreach-call) 6.9 3.7 120 330 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.0  1.0  11   130 1.9  .094  false(unreach-call) 31    17    450   1000 timeout 97   76   1600 4900 - -
loops/s3_false-unreach-call.i out of memory 0 wit inspect 350    350    3900   15000 1.7  0      false(unreach-call) 15    8.0  180   480 true 10   5.5 200 350 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 890    900    9100   1000 1.7  0      false(unreach-call) 6.9  3.8  77   300 false(unreach-call) 25   13   260 490 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .92 .92 10   130 1.7  0      false(unreach-call) 5.6  3.0  120   290 false(unreach-call) 15   8.2 150 450 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.8  1.8  27   140 1.9  0      true 23    12    420   670 timeout 97   78   1700 5000 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .63 .63 8.0 81 1.7  0      false(unreach-call) 7.3  3.9  73   290 false(unreach-call) 16   9.0 300 490 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .22 .22 2.8 23 1.7  0      false(unreach-call) 4.9  2.7  76   290 true 7.0 3.7 110 320 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 .17 1.3 23 1.7  .094  false(unreach-call) 4.1  2.3  85   280 true 6.7 3.6 110 310 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 52    52    720   2100 1.7  0      true 4.0  2.2  70   260 false(unreach-call) 8.7 4.7 170 350 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .60 .60 6.7 81 1.7  0      true 6.0  3.3  49   290 false(unreach-call) 28   15   410 1500 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16    16    170   920 1.7  0      false(unreach-call) 3.8  2.2  59   270 false(unreach-call) 7.0 3.7 100 320 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13    13    150   160 1.8  .094  false(unreach-call) 3.8  2.1  58   290 false(unreach-call) 7.2 3.8 90 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 42    42    490   1800 1.8  .094  false(unreach-call) 5.3  2.9  52   280 false(unreach-call) 7.3 3.9 120 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 15    15    200   890 2.5  0      true 47    26    520   1300 timeout 97   66   1300 6800 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.7  9.7  110   510 1.7  .094  false(unreach-call) 4.6  2.6  62   280 false(unreach-call) 7.5 3.9 86 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10    10    110   1200 1.7  0      true 4.3  2.4  55   280 false(unreach-call) 10   5.7 170 350 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i timeout 0 wit inspect 900    900    10000   1800 .84 0      error (invalid witness file) .56 .35 10   40 error (invalid witness file) 5.8 3.1 90 290 - -
loops/vogal_false-unreach-call.i out of memory 0 wit inspect 140    140    1400   15000 1.7  0      timeout 92    79    1600   710 true 29   16   340 660 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .22 .22 2.1 23 1.7  .094  false(unreach-call) 4.0  2.3  72   280 true 6.6 3.6 76 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .19 .19 1.8 23 1.7  0      - - true 5.5  3.1  61   290 true 11   5.9 120 350
loops/bubble_sort_true-unreach-call.i timeout 0 wit inspect 900    900    5500   7000 .84 0      - - error (invalid witness file) .54 .34 11   43 error (invalid witness file) 5.7 3.0 77 300
loops/count_up_down_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 1.3  1.3  18   140 2.0  0      - - timeout 920    890    16000   4300 out of memory 440   380   8800 7000
loops/eureka_01_true-unreach-call.i true 1 wit inspect 20    20    270   3000 1.8  0      - - out of memory 700    670    11000   7000 timeout 960   840   15000 4600
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 7.9  7.9  100   1100 1.7  .0041 - - true 440    420    10000   5100 true 36   21   550 750
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .23 .23 2.5 31 1.9  0      - - true 7.0  3.8  86   300 true 8.6 4.5 140 340
loops/for_infinite_loop_2_true-unreach-call_false-termination.i false(unreach-call) -16 wit inspect .19 .19 2.1 23 1.7  .094  - - timeout 910    890    13000   4200 true 10   5.3 93 340
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    8200   6000 .84 0      - - error (invalid witness file) .58 .38 6.8 40 error (invalid witness file) 7.1 3.8 56 290
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .18 .18 2.1 24 1.7  0      - - true 21    13    350   560 true 41   27   430 780
loops/linear_sea.ch_true-unreach-call.i true 1 wit inspect 4.8  4.8  67   110 2.0  0      - - out of memory 880    870    17000   7000 timeout 960   940   16000 830
loops/lu.cmp_true-unreach-call.i out of memory 0 wit inspect 9.8  9.5  110   15000 .84 0      - - error (invalid witness file) .47 .31 9.6 39 error (invalid witness file) 5.3 2.8 75 290
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 26    26    330   1700 1.7  0      - - true 10    7.3  160   420 true 15   8.0 120 370
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 2.2  2.2  25   220 2.3  0      - - out of memory 280    270    4700   7000 true 11   6.0 180 390
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .16 .16 1.9 23 1.7  0      - - true 4.8  2.7  55   270 true 190   180   3500 1100
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .14 .14 1.8 23 1.7  0      - - true 3.8  2.1  38   270 true 170   160   3300 780
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 12    12    140   500 3.4  0      - - true 15    8.4  240   490 true 13   6.7 160 420
loops/sum01_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 1.4  1.4  17   130 1.9  0      - - timeout 910    890    18000   940 true 120   95   2000 4800
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect .27 .27 3.6 41 2.0  0      - - true 11    6.3  83   310 true 7.7 4.1 100 320
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .13 .13 1.8 23 1.7  0      - - true 6.0  3.4  65   290 true 13   7.1 120 430
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900    900    11000   1300 .84 0      - - error (invalid witness file) .53 .33 9.8 41 error (invalid witness file) 6.3 3.3 130 300
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 35    35    370   4700 44    .0082 - - true 29    16    360   2700 true 22   12   400 1500
loops/terminator_03_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 43    43    490   320 1.9  0      - - true 20    10    140   640 true 73   57   1500 4800
loops/trex01_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 42    42    490   1800 1.8  .094  - - true 120    93    2600   1200 out of memory 130   81   1800 7000
loops/trex02_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 15    15    180   890 2.2  .094  - - true 40    23    530   1300 out of memory 98   66   1200 7000
loops/trex03_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 560    560    8000   890 2.2  0      - - true 57    35    600   1700 out of memory 110   73   870 7000
loops/trex04_true-unreach-call_false-termination.i false(unreach-call) -16 wit inspect 22    22    250   300 1.9  0      - - true 27    16    280   770 true 69   53   1300 5000
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 11    11    140   1200 2.5  0      - - out of memory 340    330    7100   7000 true 13   7.2 130 370
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    11000   1800 .84 0      - - error (invalid witness file) .51 .33 7.4 41 error (invalid witness file) 6.9 3.6 72 300
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 2.0  2.0  21   290 2.5  .0082 - - true 12    7.0  110   330 true 9.6 5.1 110 340
loops/vogal_true-unreach-call.i true 2 wit inspect 290    290    3300   14000 4.7  0      - - true 71    54    1000   910 true 200   160   2800 3100
loops/while_infinite_loop_1_true-unreach-call_false-termination.i false(unreach-call) -16 wit inspect .19 .19 1.7 23 1.7  0      - - true 4.4  2.5  47   270 true 6.2 3.4 76 310
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .19 .19 1.9 23 1.8  0      - - true 7.6  4.1  82   310 true 7.6 4.0 120 330
loops/while_infinite_loop_3_true-unreach-call_false-termination.i false(unreach-call) -16 wit inspect .20 .20 2.2 23 1.7  .094  - - true 3.8  2.1  73   280 true 7.0 3.7 150 310
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 140    140    1900   160 1.8  .094  timeout 97    89    2300   2400 timeout 97   79   1500 4600 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 140    140    2000   180 1.9  0      timeout 96    86    3100   1200 timeout 96   77   1200 4500 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 150    150    2000   230 1.9  0      timeout 98    81    1700   2900 timeout 97   76   2300 5000 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect .14 .14 1.7 23 1.7  0      false(unreach-call) 28    15    480   1000 true 7.5 4.0 140 310 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 0 wit inspect 1.3  1.3  17   130 1.7  .094  true 4.8  2.6  110   310 out of memory 78   47   930 7000 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect .16 .16 1.8 23 1.7  0      timeout 98    82    1800   1800 true 6.8 3.7 110 320 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.9  2.9  34   170 2.0  0      false(unreach-call) 37    23    860   2400 timeout 97   69   1200 5500 - -
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 0 wit inspect 3.3  3.3  33   450 1.7  0      timeout 98    83    1900   1900 true 7.0 3.7 110 320 - -
loop-acceleration/phases_false-unreach-call1.i false(unreach-call) 0 wit inspect .15 .15 1.8 23 1.7  .10   timeout 98    83    1800   2000 true 6.8 3.6 110 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect 56    56    640   3200 1.7  0      false(unreach-call) 3.6  2.0  45   270 false(unreach-call) 7.3 3.9 120 320 - -
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 0 wit inspect .14 .14 1.8 23 1.7  0      timeout 96    82    1300   1900 true 6.2 3.4 85 310 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 2.6  2.6  27   120 1.8  .094  timeout 98    82    2400   1300 false(unreach-call) 66   52   1500 4500 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 1.3  1.3  14   83 1.8  0      false(unreach-call) 28    15    340   950 false(unreach-call) 69   54   1300 4800 - -
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 0 wit inspect .14 .14 1.7 23 1.7  .094  timeout 97    86    2200   2200 true 6.6 3.6 96 310 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .14 .14 1.5 23 1.7  .094  false(unreach-call) 4.7  2.6  44   270 true 7.3 3.8 120 320 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .14 .14 1.5 23 1.7  .094  false(unreach-call) 4.9  2.7  52   270 true 7.5 4.0 94 310 - -
loop-acceleration/array_true-unreach-call1_true-termination.i false(unreach-call) -16 wit inspect 140    140    1800   160 1.8  0      - - true 44    38    950   1300 out of memory 270   230   3800 7000
loop-acceleration/array_true-unreach-call2_true-termination.i false(unreach-call) -16 wit inspect 140    140    1900   180 1.9  0      - - out of memory 260    250    5700   7000 out of memory 510   470   7800 7000
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect .83 .83 9.4 130 2.2  0      - - timeout 910    890    18000   5000 timeout 960   850   21000 2700
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect .82 .82 10   130 2.2  0      - - out of memory 340    320    6900   7000 timeout 960   840   12000 2800
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .19 .19 2.2 30 1.9  0      - - true 9.6  5.2  130   330 timeout 960   810   18000 2500
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 1.4  1.4  17   180 2.3  0      - - true 18    14    360   530 true 600   510   6800 1500
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 96    96    1000   2600 6.7  0      - - true 15    8.3  150   620 true 42   28   430 890
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect .26 .26 2.3 39 2.0  0      - - out of memory 340    330    8600   7000 timeout 960   800   13000 3500
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 1.1  1.1  15   160 2.2  0      - - out of memory 380    370    6700   7000 true 12   6.2 140 320
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 3.6  3.6  35   550 2.8  0      - - true 44    37    730   650 timeout 960   830   11000 4700
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect .16 .16 2.1 23 1.8  0      - - out of memory 430    420    8200   7000 timeout 960   810   12000 2700
loop-acceleration/phases_true-unreach-call1.i false(unreach-call) -16 wit inspect .15 .15 1.9 23 1.7  0      - - timeout 920    890    15000   4200 true 6.3 3.4 75 300
loop-acceleration/phases_true-unreach-call2_false-termination.i false(unreach-call) -16 wit inspect 57    57    540   3200 1.8  .094  - - true 16    8.2  160   570 true 51   37   1100 3600
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect .18 .18 1.9 23 1.8  0      - - out of memory 430    420    7100   7000 timeout 960   810   17000 2500
loop-acceleration/simple_true-unreach-call2_true-termination.i false(unreach-call) -16 wit inspect 2.6  2.6  33   120 1.8  .094  - - timeout 910    890    15000   2400 true 70   54   760 4800
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect .67 .67 7.4 94 2.0  0      - - timeout 910    900    18000   6200 timeout 960   920   16000 750
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .19 .19 2.1 23 1.8  0      - - true 10    5.4  120   310 true 7.9 4.3 120 330
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 8.5  6.0  97   400 true 55   49   950 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .14 .14 1.6 24 1.7  .30   - - true 4.8  2.6  68   280 true 11   5.8 130 380
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 24    24    300   2300 1.8  0      true 17    8.8  330   600 true 7.5 3.9 120 320 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 900    900    10000   2400 1.7  0      - - timeout 900    890    17000   2200 true 11   6.1 130 380
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 9.3  9.3  120   870 2.4  .0082 - - out of memory 500    490    8300   7000 true 12   6.2 160 390
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i out of memory 0 wit inspect 34    33    380   15000 .84 0      - - error (invalid witness file) .48 .31 8.4 39 error (invalid witness file) 6.5 3.4 63 290
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    13000   650 .84 0      - - error (invalid witness file) .71 .45 6.8 41 error (invalid witness file) 5.2 2.8 72 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i out of memory 0 wit inspect 140    140    1500   15000 1.7  0      - - true 28    14    300   820 true 29   16   420 3700
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 18    18    250   1000 3.0  0      - - out of memory 260    250    3800   7000 timeout 960   790   13000 4700
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true 1 wit inspect 13    13    130   1400 4.0  0      - - out of memory 540    480    8800   7000 timeout 960   800   14000 4700
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 wit inspect 31    31    410   1000 3.0  0      - - timeout 910    890    10000   6800 timeout 960   820   12000 2500
loop-invgen/heapsort_true-unreach-call_true-termination.i out of memory 0 wit inspect 39    38    370   15000 .84 0      - - error (invalid witness file) .54 .34 11   43 error (invalid witness file) 7.1 3.7 47 300
loop-invgen/id_build_true-unreach-call_true-termination.i out of memory 0 wit inspect 70    70    970   15000 1.7  0      - - true 35    29    760   720 true 9.2 4.9 140 340
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 31    31    410   2000 4.4  0      - - true 200    190    3100   980 true 12   6.6 140 440
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    8700   11000 .84 0      - - error (invalid witness file) .50 .32 12   41 error (invalid witness file) 5.7 3.1 95 300
loop-invgen/nested6_true-unreach-call_true-termination.i out of memory 0 wit inspect 52    52    540   15000 .84 0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.5 3.5 62 300
loop-invgen/nested9_true-unreach-call_true-termination.i out of memory 0 wit inspect 32    31    310   15000 .84 0      - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 5.5 2.9 62 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 38    38    460   3500 3.6  0      - - out of memory 460    450    7300   7000 true 22   12   160 650
loop-invgen/seq_true-unreach-call_true-termination.i true 1 wit inspect 92    92    1000   1200 3.6  0      - - out of memory 660    610    12000   7000 timeout 960   790   12000 3200
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900    900    10000   2800 .84 0      - - error (invalid witness file) .67 .42 7.2 40 error (invalid witness file) 6.1 3.2 100 300
loop-invgen/up_true-unreach-call_true-termination.i true 1 wit inspect 17    17    210   1000 3.0  0      - - out of memory 320    310    4300   7000 timeout 960   790   19000 4200
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 2.5  2.5  29   230 2.3  0      - - out of memory 500    490    8500   7000 true 13   7.0 120 360
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 130    130    1600   880 2.0  .094  - - timeout 910    890    17000   1500 out of memory 130   71   1100 7000
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .14 .14 1.6 23 1.7  0      - - true 5.0  2.8  68   280 true 9.6 5.2 110 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 3.0  3.0  38   220 2.2  0      - - true 28    15    310   1100 out of memory 100   66   940 7000
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 6.8  6.8  63   990 1.7  0      - - true 8.8  4.7  88   300 true 9.0 4.8 170 350
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 5.0  5.0  62   510 2.3  0      - - true 17    11    190   420 true 8.1 4.3 85 320
loop-lit/ddlm2013_true-unreach-call.i true 1 wit inspect 4.7  4.7  62   440 3.1  0      - - out of memory 330    320    6100   7000 timeout 960   840   12000 3200
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .15 .14 2.0 23 1.7  0      - - true 72    64    1600   790 true 110   71   1200 1500
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 8.1  8.1  94   380 2.5  0      - - timeout 900    890    17000   3700 true 11   6.0 93 380
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .18 .18 1.5 23 1.7  0      - - true 63    55    1200   1100 true 84   50   800 1200
loop-lit/gsv2008_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 7.3  7.3  79   220 2.0  0      - - true 30    16    470   990 true 390   340   8100 6700
loop-lit/hhk2008_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 2.7  2.7  33   150 2.0  .094  - - true 19    9.8  170   750 out of memory 410   360   11000 7000
loop-lit/jm2006_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 1.4  1.4  16   140 2.0  0      - - timeout 920    890    14000   4200 out of memory 760   700   8800 7000
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 2.0  2.0  27   210 2.2  0      - - true 100    77    1500   1900 out of memory 130   91   1700 7000
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    900    11000   880 .84 0      - - error (invalid witness file) .64 .41 7.3 42 error (invalid witness file) 5.9 3.1 79 280
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 100    100    1200   1900 1.7  .49   false(unreach-call) 7.3  4.0  90   310 false(unreach-call) 12   6.5 140 380 - -
loop-new/count_by_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect .16 .16 1.5 23 1.7  0      - - timeout 910    890    18000   2900 true 6.0 3.3 81 300
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect .23 .23 3.0 30 1.9  0      - - true 11    5.7  120   310 true 11   6.0 170 370
loop-new/count_by_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect .15 .15 1.6 23 1.7  0      - - timeout 920    890    15000   3100 true 7.3 3.8 82 320
loop-new/count_by_k_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.6  5.6  79   160 1.9  0      - - timeout 910    890    16000   2000 out of memory 86   54   790 7000
loop-new/count_by_nondet_true-unreach-call_true-termination.i out of memory 0 wit inspect 110    110    1400   15000 1.7  0      - - timeout 900    890    17000   1500 timeout 960   790   13000 4800
loop-new/gauss_sum_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 1.8  1.8  24   140 1.9  0      - - true 16    8.3  160   580 out of memory 250   220   3400 7000
loop-new/half_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 1.3  1.3  14   110 1.8  0      - - timeout 910    890    18000   3000 true 55   38   680 3100
loop-new/nested_true-unreach-call_true-termination.i out of memory 0 wit inspect 890    890    10000   15000 1.7  0      - - timeout 910    890    16000   2400 true 42   23   700 1500
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect .21 .21 2.5 25 1.7  0      - - true 29    23    450   590 error 10   5.5 130 310
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect .25 .25 2.2 25 1.7  0      - - true 32    26    550   590 error 11   5.7 120 320
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect .25 .25 2.3 25 1.7  0      - - true 27    21    560   580 error 10   5.6 140 300
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect .22 .22 2.6 25 1.7  0      - - true 26    20    380   550 error 10   5.5 140 300
loop-industry-pattern/mod3_true-unreach-call.c timeout 0 wit inspect 900    900    13000   290 .84 0      - - error (invalid witness file) .64 .40 7.5 39 error (invalid witness file) 6.2 3.4 60 290
loop-industry-pattern/nested_true-unreach-call.c out of memory 0 wit inspect 62    62    840   15000 .84 0      - - error (invalid witness file) .54 .34 13   41 error (invalid witness file) 6.2 3.3 60 300
loop-industry-pattern/ofuf_1_true-unreach-call.c timeout 0 wit inspect 900    900    12000   1800 .84 0      - - error (invalid witness file) .60 .40 8.2 40 error (invalid witness file) 6.1 3.2 85 310
loop-industry-pattern/ofuf_2_true-unreach-call.c timeout 0 wit inspect 900    900    12000   1800 .84 0      - - error (invalid witness file) .62 .39 8.3 40 error (invalid witness file) 5.8 3.0 95 300
loop-industry-pattern/ofuf_3_true-unreach-call.c timeout 0 wit inspect 900    900    11000   1800 .84 0      - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.6 3.5 120 310
loop-industry-pattern/ofuf_4_true-unreach-call.c timeout 0 wit inspect 900    900    11000   1700 .84 0      - - error (invalid witness file) .66 .41 8.1 40 error (invalid witness file) 6.1 3.2 69 310
loop-industry-pattern/ofuf_5_true-unreach-call.c timeout 0 wit inspect 900    900    11000   1700 .84 0      - - error (invalid witness file) .59 .38 7.2 39 error (invalid witness file) 6.8 3.5 60 320
loops/heavy_true-unreach-call.c out of memory 0 wit inspect 780    780    3100   15000 .84 0      - - error (invalid witness file) .50 .32 8.5 39 error (invalid witness file) 5.7 3.1 52 310
loops/compact_false-unreach-call.c timeout 0 wit inspect 900    900    11000   4400 .84 0      error (invalid witness file) .52 .32 12   39 error (invalid witness file) 5.5 2.9 82 300 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 320    320    3800   15000 .84 0      error (invalid witness file) .66 .42 8.3 40 error (invalid witness file) 5.7 3.0 85 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 -295 27000 27000 300000 400000 320 3.0  156 1300 1000 26000 34000   156 1400 960 21000 69000   156 26000 25000 460000 220000   156 23000 19000 340000 220000  
    correct results 67 107 4500 4500 52000 59000 180 1.8  26 340 220 6300 13000   25 580 380 9100 30000   32 5500 5200 100000 70000   34 3800 3100 53000 31000  
        correct true 40 80 1500 1500 17000 38000 130 .33 4 0 0 0 0   6 0 0 0 0   32 5500 5200 100000 70000   34 3800 3100 53000 31000  
        correct false 27 27 3000 3000 35000 20000 47 1.4  22 340 220 6300 13000   19 580 380 9100 30000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 27 14 680 680 9000 14000 59 .48 5 870 730 18000 19000   6 700 530 11000 35000   0 8000 7700 140000 95000   0 13000 12000 200000 43000  
        correct-unconfirmed true 14 14 200 200 2500 9700 35 0    5 0 0 0 0   6 0 0 0 0   0 8000 7700 140000 95000   0 13000 12000 200000 43000  
        correct-unconfirmed false 13 0 470 470 6500 4600 24 .48 0 870 730 18000 19000   0 700 530 11000 35000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 26 -416 1200 1200 16000 10000 49 .75 0 0 0 0 0   0 0 0 0 0   14 11000 10000 190000 53000   13 4300 3600 68000 130000  
        incorrect true 0
        incorrect false 26 -416 1200 1200 16000 10000 49 .75 0 0 0 0 0   0 0 0 0 0   0 11000 10000 190000 53000   0 4300 3600 68000 130000  
score (156 tasks, max score: 261) -295
Run set sv-comp17.ReachSafety-Loops