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