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