Tool VeriAbs
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-14 09:46:18 CET [[ 2017-01-15 04:55:34 CET ]] [[ 2017-01-15 05:46:09 CET ]] [[ 2017-01-15 05:17:25 CET ]] [[ 2017-01-15 05:48:02 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.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 10   4.1 84 290 .090 0      false(unreach-call) 5.2  2.9  55   290 false(unreach-call) 7.3 4.0 140 320 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 290   270   2300 2100 .25  0      false(unreach-call) 7.2  3.8  130   350 error 13   7.0 180 320 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.5 3.8 76 280 .14  0      false(unreach-call) 3.8  2.2  68   270 false(unreach-call) 7.3 4.0 150 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 1 wit inspect 47   16   380 1100 .11  0      false(unreach-call) 7.5  4.2  150   350 timeout 96   77   1400 1300 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   4.0 79 280 .090 .0041 false(unreach-call) 4.2  2.3  96   270 false(unreach-call) 7.7 4.1 140 320 - -
loops/insertion_sort_false-unreach-call_true-termination.i out of memory 0 wit inspect 96   92   1300 15000 .094 .098  error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 110 300 - -
loops/invert_string_false-unreach-call_true-termination.i out of memory 0 wit inspect 110   110   1200 15000 .12  0      error (invalid witness file) .53 .35 13   39 error (invalid witness file) 5.9 3.2 100 300 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 9.8 3.9 72 280 .11  0      true 4.7  2.6  99   280 true 56   46   930 650 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 270   250   2800 1300 .094 0      false(unreach-call) 13    9.5  220   950 out of memory 47   38   780 7000 - -
loops/matrix_false-unreach-call_true-termination.i out of memory 0 wit inspect 66   62   730 15000 .078 0      error (invalid witness file) .52 .35 4.1 41 error (invalid witness file) 5.8 3.1 110 300 - -
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 850   840   8400 15000 37     0      error (invalid witness file) .50 .33 4.6 42 error (invalid witness file) 6.3 3.3 120 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 9.5 4.0 71 280 .15  0      false(unreach-call) 3.8  2.1  73   280 false(unreach-call) 7.2 3.9 140 330 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 25   19   230 290 .30  .0041 false(unreach-call) 4.3  2.4  88   290 false(unreach-call) 8.1 4.3 150 350 - -
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 110   97   1100 2500 .28  0      false(unreach-call) 8.4  4.5  160   320 true 18   9.5 250 530 - -
loops/string_false-unreach-call_true-termination.i witness invalid (false(unreach-call)) 0 wit inspect 12   4.3 90 320 .098 0      error (invalid witness file) .50 .32 6.5 41 error (invalid witness file) 5.8 3.1 110 300 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12   4.5 90 300 .11  0      false(unreach-call) 4.2  2.3  52   280 false(unreach-call) 9.5 5.1 89 360 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 81   74   840 310 2.5   .0041 false(unreach-call) 4.2  2.4  96   280 false(unreach-call) 9.4 5.1 140 360 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13   4.7 100 350 .12  7.8    false(unreach-call) 5.5  3.0  73   290 false(unreach-call) 13   7.0 240 590 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   4.9 110 460 .11  0      false(unreach-call) 5.4  3.0  110   290 timeout 97   59   790 7000 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   4.1 86 300 .094 .0041 false(unreach-call) 4.2  2.3  63   280 false(unreach-call) 10   5.3 180 410 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 15   7.6 120 290 .090 0      false(unreach-call) 4.8  2.7  89   300 false(unreach-call) 9.2 4.8 180 360 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.4 3.7 63 280 .090 .0041 false(unreach-call) 4.0  2.2  83   280 false(unreach-call) 7.8 4.2 120 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.2 3.8 73 280 .11  0      false(unreach-call) 3.7  2.1  71   270 false(unreach-call) 7.2 3.9 160 320 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.6 3.8 66 290 .090 0      false(unreach-call) 3.8  2.1  76   280 false(unreach-call) 7.9 4.3 140 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   4.2 68 280 .11  0      false(unreach-call) 3.8  2.1  68   270 false(unreach-call) 7.8 4.1 140 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.8 3.9 70 290 .11  .0041 false(unreach-call) 3.8  2.1  85   280 false(unreach-call) 7.1 3.8 150 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   4.2 74 280 .11  .0041 false(unreach-call) 3.9  2.2  86   270 false(unreach-call) 7.7 4.1 160 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   3.8 73 290 .090 .0082 false(unreach-call) 3.9  2.2  85   280 false(unreach-call) 11   6.0 150 370 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18   11   150 290 .098 .012  false(unreach-call) 4.9  2.7  100   280 false(unreach-call) 20   11   300 570 - -
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 18   6.0 130 460 .11  0      false(unreach-call) 6.5  3.6  140   310 timeout 96   70   1400 2000 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.8 3.8 72 280 .090 0      false(unreach-call) 3.8  2.1  62   280 false(unreach-call) 7.3 3.9 160 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 510   300   6100 870 .098 .016  - - true 4.4  2.5  91   280 true 9.5 5.2 200 350
loops/bubble_sort_true-unreach-call.i true 2 wit inspect 6.8 2.3 51 280 .041 .0082 - - true 3.8  2.1  54   270 true 7.5 4.1 140 340
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 15   4.0 110 510 .16  0      - - out of memory 340    330    4200   7000 true 58   50   1500 400
loops/eureka_01_true-unreach-call.i true 1 wit inspect 12   4.3 99 260 .13  0      - - out of memory 580    560    7100   7000 timeout 960   850   11000 4300
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 11   4.1 82 270 .10  0      - - true 440    420    5600   5200 true 37   21   630 720
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 9.4 2.9 77 300 .045 0      - - true 4.5  2.5  94   280 true 7.5 4.0 140 330
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 9.2 2.9 64 290 .045 0      - - true 4.3  2.4  98   280 true 7.7 4.1 140 320
loops/insertion_sort_true-unreach-call_true-termination.i out of memory 0 wit inspect 49   45   630 15000 .094 0      - - error (invalid witness file) .53 .35 13   41 error (invalid witness file) 6.1 3.2 110 310
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 650   300   7300 910 .18  0      - - true 19    12    330   540 true 42   28   550 710
loops/linear_sea.ch_true-unreach-call.i true 1 wit inspect 640   300   6200 850 .17  .0082 - - out of memory 730    720    11000   7000 timeout 960   940   22000 800
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 270   250   2600 1200 .14  0      - - timeout 910    870    10000   5800 out of memory 45   36   1100 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 28   8.0 200 630 .18  0      - - true 8.2  6.1  190   420 true 13   6.8 230 380
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 570   520   6800 670 2.7   0      - - out of memory 220    210    2200   7000 true 11   5.8 210 380
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 650   300   6000 870 .17  0      - - true 4.1  2.2  81   270 true 170   160   4000 910
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 650   300   6000 910 .17  0      - - true 4.3  2.4  67   270 true 170   160   3500 730
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 11   4.1 89 270 .10  0      - - true 5.9  3.2  110   290 true 10   5.5 190 360
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 14   3.7 100 470 .045 0      - - timeout 900    900    9900   3700 true 13   6.9 270 370
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 12   3.8 99 360 .074 0      - - true 4.1  2.3  85   270 true 7.5 4.1 140 310
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 14   3.7 100 490 .082 0      - - true 5.3  2.9  98   280 true 14   7.5 200 390
loops/sum_array_true-unreach-call.i true 1 wit inspect 660   310   7400 1100 .17  0      - - timeout 900    880    11000   6400 timeout 960   870   13000 4700
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 9.8 3.0 71 320 .053 0      - - true 4.7  2.6  74   280 true 8.6 4.6 180 340
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 12   3.4 89 470 .045 .0082 - - true 4.7  2.6  65   280 true 7.9 4.3 170 320
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 19   4.7 150 580 .053 0      - - out of memory 440    410    4700   7000 true 7.9 4.2 160 320
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 15   3.9 110 560 .16  0      - - true 4.7  2.6  98   280 true 7.3 3.9 140 320
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 31   8.0 230 690 .18  .11   - - true 5.9  3.2  120   310 true 8.4 4.5 180 320
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 12   3.4 82 440 .053 0      - - true 5.5  2.9  120   290 true 7.7 4.2 140 320
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 13   3.4 89 460 .045 0      - - out of memory 280    280    5100   7000 true 10   5.6 230 360
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 20   12   190 270 .10  0      - - true 8.9  4.7  180   360 true 9.0 4.9 170 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 12   3.4 82 420 .045 .0082 - - true 5.9  3.2  120   310 true 8.0 4.2 150 320
loops/vogal_true-unreach-call.i true 2 wit inspect 660   310   7100 1200 .21  0      - - true 46    37    520   980 true 190   150   2700 3700
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 12   3.4 89 470 .078 0      - - true 4.2  2.4  88   280 true 8.4 4.4 160 340
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 9.0 2.8 65 280 .045 0      - - true 4.1  2.3  50   280 true 7.6 4.0 170 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 13   3.5 95 480 .082 0      - - true 4.2  2.4  79   280 true 7.4 4.0 150 320
loop-acceleration/array_false-unreach-call1_true-termination.i witness invalid (false(unreach-call)) 0 wit inspect 340   300   4100 3700 .045 0      error (invalid witness file) .51 .33 6.2 39 error (invalid witness file) 5.4 3.0 100 290 - -
loop-acceleration/array_false-unreach-call2_true-termination.i witness invalid (false(unreach-call)) 0 wit inspect 360   320   4200 4000 1.9   .082  error (invalid witness file) .48 .31 6.2 40 error (invalid witness file) 6.3 3.3 110 310 - -
loop-acceleration/array_false-unreach-call3_true-termination.i witness invalid (false(unreach-call)) 0 wit inspect 350   310   4100 3700 1.0   0      error (invalid witness file) .51 .34 13   40 error (invalid witness file) 6.5 3.5 130 320 - -
loop-acceleration/const_false-unreach-call1.i witness invalid (false(unreach-call)) 0 wit inspect 340   300   3500 3700 .65  0      error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.2 3.2 110 300 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 83   51   820 1900 .18  0      false(unreach-call) 6.8  3.6  140   310 timeout 96   55   740 6600 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 wit inspect 24   16   210 220 14     0      error (invalid witness file) .54 .36 7.9 40 error (invalid witness file) 6.0 3.2 98 290 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 22   17   260 280 .27  0      false(unreach-call) 3.7  2.1  76   270 false(unreach-call) 7.2 3.9 140 320 - -
loop-acceleration/nested_false-unreach-call1.i unknown 0 wit inspect 150   140   1900 7100 180     0      error (invalid witness file) .55 .36 11   43 error (invalid witness file) 6.2 3.3 110 300 - -
loop-acceleration/phases_false-unreach-call1.i unknown 0 wit inspect 140   140   1600 6000 88     0      error (invalid witness file) .51 .33 9.7 41 error (invalid witness file) 6.2 3.3 120 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect 37   32   310 580 .26  0      false(unreach-call) 3.9  2.2  79   270 false(unreach-call) 7.9 4.3 160 330 - -
loop-acceleration/simple_false-unreach-call1.i unknown 0 wit inspect 140   140   2000 8700 11     .098  error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.5 2.9 96 300 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 8.9 3.5 63 280 .090 .0041 false(unreach-call) 3.6  2.0  77   270 false(unreach-call) 6.9 3.7 130 310 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 130   120   690 860 .24  0      false(unreach-call) 3.6  2.1  57   270 false(unreach-call) 7.5 4.0 140 330 - -
loop-acceleration/simple_false-unreach-call4.i unknown 0 wit inspect 150   140   1600 8400 150     0      error (invalid witness file) .50 .35 5.7 40 error (invalid witness file) 6.0 3.1 110 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 10   3.8 80 290 .094 .0041 false(unreach-call) 3.9  2.2  69   270 false(unreach-call) 11   6.0 220 370 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 10   3.9 76 290 .094 0      false(unreach-call) 4.3  2.4  90   280 false(unreach-call) 12   6.4 240 350 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 640   300   6500 840 .17  .090  - - true 4.0  2.3  85   280 timeout 960   800   13000 4300
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 640   300   7500 830 .17  .090  - - out of memory 270    270    2800   7000 timeout 960   800   12000 3900
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 640   300   6200 860 .17  .19   - - timeout 900    890    12000   5900 timeout 960   850   11000 2800
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 640   300   6300 860 .17  .32   - - out of memory 320    300    4200   7000 timeout 960   840   11000 2900
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 11   3.1 89 420 .045 0      - - true 4.7  2.6  110   280 timeout 960   810   20000 2600
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 20   6.1 150 480 .20  0      - - true 15    11    260   530 true 600   510   9500 1300
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 140   110   1700 670 .18  0      - - true 10    5.5  190   410 true 41   27   990 700
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect 16   4.2 110 540 .045 .0082 - - out of memory 330    320    5100   7000 timeout 960   810   19000 3000
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 12   3.3 88 440 .045 0      - - out of memory 390    380    3800   7000 true 7.8 4.2 170 330
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 16   4.2 110 620 .086 0      - - true 6.8  3.6  51   310 timeout 960   830   11000 4700
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 12   3.3 97 450 .045 0      - - out of memory 360    350    4700   7000 timeout 960   810   24000 2500
loop-acceleration/phases_true-unreach-call1.i unknown 0 wit inspect 140   140   1900 6100 11     0      - - error (invalid witness file) .49 .31 5.7 39 error (invalid witness file) 5.4 2.9 100 300
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 11   3.2 90 440 .045 0      - - timeout 900    900    16000   480 true 9.4 5.5 200 320
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect 12   3.3 77 450 .045 0      - - out of memory 370    360    5800   7000 timeout 960   810   11000 2500
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 13   3.8 87 480 .15  0      - - true 4.5  2.5  77   270 true 7.8 4.2 150 320
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect 11   3.2 85 440 .045 0      - - out of memory 760    750    11000   7000 timeout 960   920   25000 800
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 12   3.4 85 450 .053 0      - - true 4.5  2.5  96   280 true 11   5.7 150 320
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 20   6.4 150 520 .18  .0082 - - true 6.8  4.9  130   400 true 63   56   1800 410
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 13   3.5 93 470 .082 .0082 - - true 4.6  2.5  87   280 true 11   5.9 190 370
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   4.0 70 280 .090 0      false(unreach-call) 4.2  2.4  95   280 false(unreach-call) 7.4 4.0 100 310 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 15   4.0 100 480 .045 0      - - timeout 900    890    9700   2700 true 11   5.7 210 360
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 13   3.6 90 470 .045 0      - - out of memory 400    390    5000   7000 true 11   6.1 220 380
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 55   16   400 800 .045 0      - - timeout 900    890    7000   2100 true 16   9.0 300 540
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 wit inspect 670   660   5400 1200 3.0   0      - - error (invalid witness file) .51 .34 6.6 40 error (invalid witness file) 6.2 3.3 120 300
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 wit inspect 650   640   5300 1400 2.2   0      - - error (invalid witness file) .50 .31 7.3 40 error (invalid witness file) 5.8 3.1 120 290
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 19   5.6 150 640 .19  0      - - out of memory 270    260    3400   7000 timeout 960   800   12000 4800
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i unknown 0 wit inspect 530   520   3500 510 2.5   .098  - - error (invalid witness file) .49 .33 12   40 error (invalid witness file) 5.5 3.0 100 290
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 wit inspect 21   5.8 150 620 .19  0      - - out of memory 820    810    5200   7000 timeout 960   820   11000 2400
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout (true) 0 wit inspect 900   190   4600 1500 .098 0      - - error (invalid witness file) .56 .36 7.3 44 error (invalid witness file) 6.1 3.3 130 300
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 19   4.7 140 630 .045 0      - - true 6.1  3.3  110   300 true 8.6 4.7 180 340
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 27   7.9 180 720 .25  0      - - true 6.3  3.4  54   330 true 11   6.1 250 360
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 28   7.5 180 680 .045 .0082 - - timeout 900    890    7400   1600 true 7.7 4.1 150 320
loop-invgen/nested6_true-unreach-call_true-termination.i unknown 0 wit inspect 900   890   6000 2800 1.9   0      - - error (invalid witness file) .57 .37 9.9 44 error (invalid witness file) 6.0 3.1 120 300
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 82   51   810 950 .045 0      - - timeout 900    890    14000   5300 true 12   6.3 240 370
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 820   730   7200 2000 2.0   .090  - - out of memory 450    440    4900   7000 true 21   12   430 500
loop-invgen/seq_true-unreach-call_true-termination.i true 1 wit inspect 46   25   430 650 .48  .11   - - out of memory 560    510    7000   7000 timeout 960   790   17000 3400
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i unknown 0 wit inspect 520   520   4300 530 1.1   0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.2 110 300
loop-invgen/up_true-unreach-call_true-termination.i true 1 wit inspect 19   5.5 140 620 .19  0      - - out of memory 260    250    2800   7000 timeout 960   790   12000 4400
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 15   3.9 110 520 .045 0      - - out of memory 410    400    3700   7000 true 8.7 4.7 150 340
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 26   12   240 600 .045 0      - - timeout 900    900    11000   940 true 13   7.0 280 360
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 14   3.7 88 490 .045 0      - - true 5.0  2.7  97   290 true 12   6.4 220 390
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 17   4.4 110 600 .16  .11   - - out of memory 330    320    3900   7000 true 10   5.6 200 340
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 13   3.6 93 450 .045 0      - - true 5.4  2.9  70   290 true 9.6 5.2 200 350
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 16   4.2 110 560 .10  .0082 - - true 5.0  2.7  85   290 true 7.7 4.2 170 320
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect 310   310   3600 1200 11     0      - - error (invalid witness file) .63 .42 6.3 39 error (invalid witness file) 5.9 3.1 120 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 21   6.1 150 520 .20  0      - - true 55    49    670   760 true 100   62   950 1700
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 15   3.9 110 500 .045 0      - - timeout 900    900    12000   3800 true 11   5.9 220 380
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 21   6.0 170 600 .25  0      - - true 50    43    490   1100 true 85   50   1200 1400
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 130   120   1300 540 1.5   0      - - timeout 900    900    10000   1300 true 8.2 4.5 180 320
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 15   4.3 100 510 .16  .0082 - - out of memory 320    310    5100   7000 true 9.6 5.3 200 360
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 18   4.5 130 640 .16  0      - - out of memory 360    350    6200   7000 true 13   7.3 250 370
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 16   4.5 110 610 .16  0      - - out of memory 360    350    4100   7000 true 14   7.8 290 370
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true 1 wit inspect 640   310   6100 800 .18  .19   - - unknown 6.3  3.5  120   320 timeout 960   890   11000 1300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 9.9 4.1 73 280 .11  .72   false(unreach-call) 4.0  2.2  87   280 false(unreach-call) 7.6 4.1 140 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 11   3.1 73 420 .045 0      - - true 5.5  3.1  71   280 timeout 960   800   18000 3700
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 14   4.3 97 360 .082 0      - - true 5.5  3.0  79   280 true 10   5.4 190 350
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect 12   3.4 86 440 .045 0      - - out of memory 320    310    4900   7000 timeout 960   800   11000 3900
loop-new/count_by_k_true-unreach-call_true-termination.i true 1 wit inspect 13   3.7 110 470 .045 0      - - timeout 900    900    17000   2500 timeout 960   900   25000 1500
loop-new/count_by_nondet_true-unreach-call_true-termination.i unknown 0 wit inspect 670   660   6500 620 2.2   0      - - error (invalid witness file) .50 .32 6.7 41 error (invalid witness file) 7.0 3.7 130 310
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 wit inspect 37   21   290 560 .53  0      - - timeout 900    900    12000   5100 timeout 960   820   17000 2500
loop-new/half_true-unreach-call_true-termination.i unknown 0 wit inspect 220   210   2300 300 10     0      - - error (invalid witness file) .52 .34 7.8 44 error (invalid witness file) 6.4 3.4 120 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   5500 760 1.0   0      - - error (invalid witness file) .50 .33 7.1 39 error (invalid witness file) 5.5 3.0 120 300
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect 67   40   670 670 .18  0      - - true 27    21    450   640 error 11   6.0 230 300
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect 66   40   650 690 .18  0      - - true 26    20    400   620 error 11   5.9 210 300
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect 66   41   620 670 .18  0      - - true 26    20    340   650 error 12   6.2 200 320
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect 76   47   880 710 .24  0      - - true 23    18    330   590 error 12   6.2 220 310
loop-industry-pattern/mod3_true-unreach-call.c true 2 wit inspect 20   7.2 170 570 .045 0      - - true 9.6  7.4  210   340 true 20   16   560 330
loop-industry-pattern/nested_true-unreach-call.c true 1 wit inspect 500   300   5500 1000 .96  .082  - - timeout 900    890    9000   2000 timeout 960   820   11000 4000
loop-industry-pattern/ofuf_1_true-unreach-call.c true 1 wit inspect 140   91   1500 820 .053 .11   - - error (recursion) 7.0  3.7  120   330 error 13   7.0 230 300
loop-industry-pattern/ofuf_2_true-unreach-call.c true 1 wit inspect 110   60   1000 810 .053 .0082 - - error (recursion) 6.7  3.6  76   290 error 11   6.0 260 310
loop-industry-pattern/ofuf_3_true-unreach-call.c true 1 wit inspect 110   59   980 790 .053 0      - - error (recursion) 6.2  3.4  95   320 error 12   6.5 250 310
loop-industry-pattern/ofuf_4_true-unreach-call.c true 1 wit inspect 14   4.7 100 300 .082 0      - - error (recursion) 6.1  3.3  71   320 error 11   5.7 210 300
loop-industry-pattern/ofuf_5_true-unreach-call.c true 1 wit inspect 14   4.7 94 280 .082 0      - - error (recursion) 4.9  2.7  90   300 error 11   5.9 230 310
loops/heavy_true-unreach-call.c true 1 wit inspect 15   7.5 130 1800 .045 0      - - timeout 900    890    11000   3300 timeout 960   880   10000 6600
loops/compact_false-unreach-call.c out of memory 0 wit inspect 240   240   1700 15000 .41  0      error (invalid witness file) .51 .33 9.9 39 error (invalid witness file) 7.0 3.7 130 320 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 520   520   6000 15000 .094 0      error (invalid witness file) .51 .32 9.2 40 error (invalid witness file) 6.0 3.2 120 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 194 24000   17000   220000 240000 550    11    156 180   100   3400 11000   156 860 540 13000 40000   156 26000 25000 320000 250000   156 25000 22000 400000 120000  
    correct results 101 168 8000   4800   78000 57000 20    9.0  34 170   94   3200 10000   28 700 440 9800 34000   46 13000 13000 160000 130000   59 5900 4800 100000 46000  
        correct true 67 134 6600   3800   66000 39000 13    .48 0 0   0   0 0   1 0 0 0 0   46 13000 13000 160000 130000   59 5900 4800 100000 46000  
        correct false 34 34 1400   1100   12000 19000 7.0  8.6  34 170   94   3200 10000   27 700 440 9800 34000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 27 26 5300   2700   53000 19000 4.6  1.1  1 4.7 2.6 99 280   1 56 46 930 650   0 12000 12000 160000 120000   0 19000 17000 300000 72000  
        correct-unconfirmed true 26 26 5300   2700   53000 18000 4.5  1.1  1 0   0   0 0   1 0 0 0 0   0 12000 12000 160000 120000   0 19000 17000 300000 72000  
        correct-unconfirmed false 1 0 9.8 3.9 72 280 .11 0    0 4.7 2.6 99 280   0 56 46 930 650   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) 194
Run set sv-comp17.ReachSafety-Loops