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