Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  1.1  23 .84 0   false(unreach-call) 4.0  2.2  87   280 false(unreach-call) 7.7 4.1 140 320 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect .65  .64  8.5  50 .84 0   false(unreach-call) 6.4  3.5  74   340 error 11   6.1 220 310 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .093 .094 .65 23 .84 0   false(unreach-call) 3.7  2.1  48   270 false(unreach-call) 7.3 3.9 130 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 0 wit inspect .23  .22  2.1  24 .84 0   true 4.1  2.2  55   280 true 7.3 3.9 120 330 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .093 .092 .86 23 .84 0   false(unreach-call) 3.9  2.1  43   270 false(unreach-call) 7.2 3.8 140 330 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .84  .83  11    30 .89 0   timeout 91    87    2500   1200 false(unreach-call) 30   17   270 680 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19  .19  2.0  23 .84 0   true 3.9  2.2  71   270 false(unreach-call) 11   6.1 150 360 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 2.4   2.4   34    120 .84 0   true 5.4  2.9  89   280 timeout 96   84   1100 740 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 3.5   3.4   46    80 .84 0   true 5.9  3.2  97   300 out of memory 46   37   550 7000 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15  .15  1.2  23 .84 0   false(unreach-call) 7.1  4.6  90   470 true 7.5 4.1 150 330 - -
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900     900     1900    1000 .84 0   error (invalid witness file) .52 .34 14   40 error (invalid witness file) 6.7 3.5 110 320 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .072 .072 .90 23 .84 0   false(unreach-call) 3.8  2.1  73   270 false(unreach-call) 7.3 3.9 140 320 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .084 .085 .71 23 .84 0   false(unreach-call) 4.3  2.4  47   290 false(unreach-call) 8.2 4.4 140 350 - -
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 810     810     8000    4000 .84 0   false(unreach-call) 11    6.2  130   480 true 11   5.6 190 350 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41  .41  4.7  28 .84 0   false(unreach-call) 4.7  2.6  38   300 false(unreach-call) 24   13   270 480 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15  .15  1.6  26 .84 0   false(unreach-call) 6.7  3.6  53   290 false(unreach-call) 15   8.4 260 450 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  .13  1.1  23 .84 0   true 3.6  2.0  50   260 false(unreach-call) 13   7.0 190 390 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  .19  2.3  33 .84 0   false(unreach-call) 5.5  3.0  75   290 false(unreach-call) 15   8.2 140 480 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18  .17  1.8  26 .84 0   false(unreach-call) 4.7  2.6  82   280 true 7.1 3.8 120 320 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  .13  1.7  23 .84 0   false(unreach-call) 4.0  2.2  51   280 true 8.6 4.5 140 330 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .15  .15  1.7  23 .84 0   false(unreach-call) 4.4  2.5  59   300 false(unreach-call) 7.9 4.3 140 350 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .68 23 .84 0   false(unreach-call) 3.7  2.0  48   270 false(unreach-call) 7.5 4.1 140 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .082 .083 .79 23 .99 0   false(unreach-call) 3.5  1.9  40   270 false(unreach-call) 7.4 3.9 93 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  .82 23 .84 0   false(unreach-call) 3.7  2.1  62   270 false(unreach-call) 7.8 4.2 150 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .81 23 .84 0   false(unreach-call) 3.7  2.1  57   280 false(unreach-call) 7.3 3.9 130 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .70 23 .84 0   false(unreach-call) 3.7  2.1  70   270 false(unreach-call) 7.8 4.2 120 330 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .83 23 .84 0   false(unreach-call) 4.3  2.4  83   280 false(unreach-call) 7.3 4.0 110 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12  .12  .97 23 .84 0   true 3.9  2.2  59   290 false(unreach-call) 12   6.3 170 380 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 wit inspect .13  .13  1.1  24 .84 0   error (invalid witness file) .54 .35 9.0 44 error (invalid witness file) 6.1 3.2 120 300 - -
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect 6.3   6.3   69    160 .84 0   timeout 92    76    1800   1100 timeout 97   61   930 6300 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .086 .085 .75 23 .84 0   false(unreach-call) 3.7  2.1  60   280 true 6.7 3.6 100 310 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .083 .082 .93 23 .84 0   - - true 4.4  2.5  77   290 true 9.7 5.3 140 350
loops/bubble_sort_true-unreach-call.i true 2 wit inspect .10  .10  1.3  23 .84 0   - - true 4.0  2.2  47   280 true 8.1 4.4 120 320
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    9900 .84 0   - - error (invalid witness file) .60 .39 8.2 40 error (invalid witness file) 5.9 3.2 110 300
loops/eureka_01_true-unreach-call.i timeout 0 wit inspect 900     900     8900    430 .99 0   - - error (invalid witness file) .62 .39 7.3 39 error (invalid witness file) 7.2 3.8 120 340
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .22  .22  2.0  26 .99 0   - - true 390    370    6900   5200 true 34   20   470 730
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .28  .28  .55 23 .84 0   - - true 3.9  2.2  61   280 true 7.6 4.1 150 320
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .077 .077 .75 23 .99 0   - - true 3.8  2.1  47   270 true 7.7 4.1 160 320
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    160 .84 0   - - error (invalid witness file) .59 .39 6.0 39 error (invalid witness file) 6.0 3.2 110 300
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .18  .18  2.0  24 .84 0   - - true 22    14    190   560 true 43   29   500 740
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     900     8200    9900 .84 0   - - error (invalid witness file) .51 .33 9.2 41 error (invalid witness file) 5.9 3.1 110 300
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 1.5   1.5   19    68 .84 0   - - timeout 910    870    18000   5800 out of memory 49   40   540 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .088 .087 .95 23 .84 0   - - true 8.0  5.9  120   420 true 12   6.6 170 370
loops/n.c11_true-unreach-call_false-termination.i unknown 0 wit inspect .10  .10  .74 23 .84 0   - - error (invalid witness file) .50 .34 5.5 40 error (invalid witness file) 5.9 3.1 110 300
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .085 .085 .75 23 .84 0   - - true 3.9  2.2  77   270 true 160   150   2300 810
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .076 .076 .89 23 .84 0   - - true 3.8  2.1  73   270 true 160   150   2200 780
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .083 .082 .83 23 .84 0   - - true 6.3  3.4  94   300 true 11   5.8 150 380
loops/sum01_true-unreach-call_true-termination.i out of memory 0 wit inspect 200     200     2100    15000 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.9 3.1 130 300
loops/sum03_true-unreach-call_false-termination.i out of memory 0 wit inspect 120     110     1400    15000 .84 0   - - error (invalid witness file) .51 .32 5.1 40 error (invalid witness file) 5.8 3.1 90 290
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .41  .40  1.4  23 .99 0   - - true 5.6  3.1  66   280 true 12   6.3 160 400
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     900     8600    750 .84 0   - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.3 3.3 89 310
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .29  .29  .61 23 .84 0   - - true 4.1  2.3  59   270 true 8.4 4.5 150 340
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect .088 .087 .79 23 .84 0   - - true 4.1  2.3  51   280 true 7.6 4.1 140 320
loops/trex01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    8500 .84 0   - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.4 3.4 120 300
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  .82 23 .84 0   - - true 4.2  2.3  83   280 true 7.4 4.0 130 330
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  .89 23 .84 0   - - true 4.8  2.7  91   280 true 7.5 4.0 150 320
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect .092 .091 .86 23 .84 0   - - true 4.8  2.6  95   290 true 8.2 4.3 140 330
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .086 .085 .80 23 .84 0   - - out of memory 300    290    6300   7000 true 9.8 5.4 170 360
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i unknown 0 wit inspect .11  .11  .90 24 .84 0   - - error (invalid witness file) .64 .42 8.6 40 error (invalid witness file) 5.6 3.0 120 290
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .081 .080 .82 23 .84 0   - - true 4.5  2.5  76   280 true 7.4 4.0 130 320
loops/vogal_true-unreach-call.i true 2 wit inspect 2.8   2.7   6.5  38 .84 0   - - true 59    47    530   1100 true 190   150   2300 3500
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .099 .098 .77 23 .84 0   - - true 3.9  2.2  69   270 true 7.8 4.2 160 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .079 .080 .84 23 .84 0   - - true 3.9  2.2  43   270 true 7.5 4.0 120 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect .10  .10  .76 23 .84 0   - - true 4.5  2.5  73   280 true 7.1 3.8 130 310
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900     900     10000    590 .84 0   error (invalid witness file) .49 .31 8.1 39 error (invalid witness file) 6.1 3.2 99 300 - -
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     9000    640 .84 0   error (invalid witness file) .49 .32 9.3 39 error (invalid witness file) 5.6 3.0 94 290 - -
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900     900     9500    530 .84 0   error (invalid witness file) .54 .35 12   41 error (invalid witness file) 5.7 3.1 120 290 - -
loop-acceleration/const_false-unreach-call1.i out of memory 0 wit inspect 150     150     1700    15000 .84 0   error (invalid witness file) .53 .35 9.0 43 error (invalid witness file) 5.9 3.2 140 300 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 4.0   4.0   53    410 .84 0   false(unreach-call) 6.5  3.5  78   310 timeout 96   57   670 7000 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 210     210     2600    15000 .84 0   error (invalid witness file) .52 .35 3.8 41 error (invalid witness file) 5.9 3.1 120 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .66 23 .84 0   false(unreach-call) 3.6  2.0  65   270 false(unreach-call) 7.2 3.8 120 320 - -
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900     900     10000    12000 .84 0   error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.1 3.3 110 300 - -
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900     900     11000    4200 .84 0   error (invalid witness file) .48 .31 5.7 39 error (invalid witness file) 6.3 3.3 100 310 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .28  .28  .55 23 .84 0   false(unreach-call) 3.7  2.1  57   270 false(unreach-call) 7.5 4.0 150 320 - -
loop-acceleration/simple_false-unreach-call1.i out of memory 0 wit inspect 260     260     2800    15000 .84 0   error (invalid witness file) .51 .33 6.8 42 error (invalid witness file) 6.2 3.3 120 290 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .072 .071 .96 23 .84 0   false(unreach-call) 3.7  2.0  74   270 false(unreach-call) 7.6 4.0 170 320 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .072 .072 .92 23 .99 0   false(unreach-call) 3.6  2.0  59   270 false(unreach-call) 7.6 4.0 150 320 - -
loop-acceleration/simple_false-unreach-call4.i out of memory 0 wit inspect 210     200     2500    15000 .84 0   error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.2 3.3 120 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .093 .091 1.0  23 .84 0   false(unreach-call) 3.9  2.2  54   280 true 6.9 3.6 140 310 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .089 .090 1.1  23 .84 0   false(unreach-call) 3.9  2.2  81   280 true 6.5 3.6 120 310 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect .089 .090 .82 23 .84 0   - - true 3.9  2.2  62   270 timeout 960   800   11000 3900
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     8800    570 .84 0   - - error (invalid witness file) .59 .38 7.1 42 error (invalid witness file) 6.4 3.4 120 320
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     900     9600    720 .90 0   - - error (invalid witness file) .53 .35 11   39 error (invalid witness file) 6.8 3.6 120 310
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900     900     10000    610 .84 0   - - error (invalid witness file) .48 .31 7.4 39 error (invalid witness file) 5.9 3.1 110 300
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .090 .089 .94 23 .84 0   - - true 4.0  2.2  80   280 timeout 960   810   12000 2600
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 56     56     820    1600 .84 0   - - true 16    12    210   550 true 600   510   6700 1400
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .45  .44  5.8  45 .84 0   - - true 7.8  4.4  130   330 true 38   26   680 690
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 200     190     2300    15000 .84 0   - - error (invalid witness file) .54 .35 10   44 error (invalid witness file) 5.8 3.1 80 300
loop-acceleration/multivar_true-unreach-call1_true-termination.i out of memory 0 wit inspect 180     180     2100    15000 .84 0   - - error (invalid witness file) .49 .31 8.8 40 error (invalid witness file) 6.2 3.3 120 300
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect .11  .11  .84 23 .84 0   - - true 5.7  3.2  120   290 timeout 960   830   12000 4700
loop-acceleration/overflow_true-unreach-call1.i out of memory 0 wit inspect 220     220     2300    15000 .84 0   - - error (invalid witness file) .48 .32 8.6 39 error (invalid witness file) 6.0 3.2 110 300
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900     900     9900    4400 .84 0   - - error (invalid witness file) .48 .31 8.2 40 error (invalid witness file) 6.8 3.5 140 320
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 110     110     1500    83 .84 0   - - timeout 900    900    15000   480 true 9.5 5.5 170 330
loop-acceleration/simple_true-unreach-call1.i out of memory 0 wit inspect 240     230     2700    15000 .84 0   - - error (invalid witness file) .64 .41 6.3 39 error (invalid witness file) 5.9 3.1 110 300
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .11  .11  .81 23 .84 0   - - true 4.2  2.3  86   270 true 7.5 4.1 130 320
loop-acceleration/simple_true-unreach-call3_true-termination.i out of memory 0 wit inspect 140     140     1900    15000 .84 0   - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.3 3.3 130 310
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .10  .10  .82 23 .84 0   - - true 4.0  2.2  68   270 true 7.9 4.2 160 320
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .11  .11  1.4  23 .84 0   - - true 6.6  4.8  120   400 true 71   64   1500 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .11  .11  .79 23 .84 0   - - true 4.7  2.6  62   270 true 11   5.8 200 380
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .093 .094 .84 23 .84 0   false(unreach-call) 4.0  2.2  64   280 false(unreach-call) 7.2 3.9 140 320 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    2600 .84 0   - - error (invalid witness file) .48 .32 9.8 39 error (invalid witness file) 7.3 3.8 100 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i out of memory 0 wit inspect 150     150     2000    15000 .84 0   - - error (invalid witness file) .54 .34 12   39 error (invalid witness file) 5.9 3.1 120 300
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     2300    130 .84 0   - - error (invalid witness file) .51 .33 12   42 error (invalid witness file) 7.1 3.7 130 330
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    420 .84 0   - - error (invalid witness file) .54 .35 13   40 error (invalid witness file) 6.2 3.3 120 300
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    640 .84 0   - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.4 2.9 99 300
loop-invgen/down_true-unreach-call_true-termination.i out of memory 0 wit inspect 600     600     6500    15000 .84 0   - - error (invalid witness file) .51 .34 10   39 error (invalid witness file) 6.5 3.4 130 310
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i unknown 0 wit inspect .098 .096 .85 23 .84 0   - - error (invalid witness file) .63 .42 6.4 40 error (invalid witness file) 5.6 3.0 95 290
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     2500    5400 .84 0   - - error (invalid witness file) .52 .35 12   40 error (invalid witness file) 6.3 3.4 130 310
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8000    3200 .84 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.9 3.2 110 290
loop-invgen/id_build_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     2800    5700 .84 0   - - error (invalid witness file) .54 .35 5.6 41 error (invalid witness file) 6.0 3.2 120 300
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  .87 23 .84 0   - - true 5.0  2.7  53   290 true 10   5.6 150 350
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     7500    3400 .84 0   - - error (invalid witness file) .48 .32 7.2 39 error (invalid witness file) 5.9 3.1 120 300
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    4600 .84 0   - - error (invalid witness file) .48 .31 9.9 39 error (invalid witness file) 5.7 3.0 120 290
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     2200    2500 .99 0   - - error (invalid witness file) .48 .32 10   41 error (invalid witness file) 5.7 3.0 88 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 wit inspect .095 .093 1.1  23 .84 0   - - error (invalid witness file) .53 .34 8.3 40 error (invalid witness file) 6.0 3.2 120 320
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    2500 .84 0   - - error (invalid witness file) .50 .32 9.2 40 error (invalid witness file) 5.9 3.1 110 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i out of memory 0 wit inspect 74     74     780    15000 .99 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.7 3.0 83 300
loop-invgen/up_true-unreach-call_true-termination.i out of memory 0 wit inspect 380     370     5200    15000 .84 0   - - error (invalid witness file) .51 .32 12   42 error (invalid witness file) 6.0 3.2 130 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 760     750     8300    15000 .84 0   - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 6.4 3.4 120 300
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     14000    190 .84 0   - - error (invalid witness file) .63 .39 8.4 40 error (invalid witness file) 5.5 3.0 97 300
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .12  .12  .75 23 .84 0   - - true 4.2  2.3  61   280 true 10   5.5 200 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9700    11000 .84 0   - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 5.5 3.0 96 290
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .10  .10  .88 23 .84 0   - - true 4.7  2.6  76   280 true 9.0 4.8 150 330
loop-lit/css2003_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 150     150     1800    15000 .99 0   - - error (invalid witness file) .47 .31 10   40 error (invalid witness file) 6.1 3.2 130 300
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect .30  .30  .72 23 .84 0   - - error (invalid witness file) .47 .31 7.8 39 error (invalid witness file) 6.0 3.2 110 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 58     57     130    680 .84 0   - - true 62    56    1100   780 true 96   60   960 1400
loop-lit/gj2007b_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 850     850     11000    15000 .96 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.8 3.1 120 300
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 14     13     160    740 .99 0   - - true 51    44    540   1100 true 85   50   1200 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9200    8900 .99 0   - - error (invalid witness file) .57 .36 8.2 43 error (invalid witness file) 5.3 2.9 84 290
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     14000    1000 .84 0   - - error (invalid witness file) .53 .33 13   41 error (invalid witness file) 6.2 3.3 130 300
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    7600 .84 0   - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 6.0 3.2 120 300
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    8000 .84 0   - - error (invalid witness file) .50 .32 6.9 40 error (invalid witness file) 5.5 2.9 110 290
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     10000    210 .84 0   - - error (invalid witness file) .50 .33 14   40 error (invalid witness file) 5.7 3.1 95 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .088 .087 .89 23 .84 0   false(unreach-call) 3.8  2.1  52   280 false(unreach-call) 7.1 3.8 140 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect .074 .073 .80 23 .84 0   - - true 4.8  2.7  67   270 timeout 960   800   12000 3900
loop-new/count_by_1_variant_true-unreach-call_true-termination.i out of memory 0 wit inspect 120     120     1500    15000 .84 0   - - error (invalid witness file) .48 .32 6.6 41 error (invalid witness file) 5.9 3.1 120 290
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8900    13000 .99 0   - - error (invalid witness file) .50 .32 9.0 43 error (invalid witness file) 5.7 3.0 120 290
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    10000 .84 0   - - error (invalid witness file) .54 .33 9.5 41 error (invalid witness file) 6.2 3.3 120 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8800    3500 .84 0   - - error (invalid witness file) .53 .34 13   39 error (invalid witness file) 6.3 3.3 92 310
loop-new/gauss_sum_true-unreach-call_true-termination.i out of memory 0 wit inspect 310     310     3500    15000 .84 0   - - error (invalid witness file) .63 .39 7.8 41 error (invalid witness file) 5.4 2.9 110 290
loop-new/half_true-unreach-call_true-termination.i out of memory 0 wit inspect 470     460     4500    15000 .84 0   - - error (invalid witness file) .53 .34 8.0 41 error (invalid witness file) 5.8 3.1 100 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9400    9200 .84 0   - - error (invalid witness file) .60 .38 6.9 43 error (invalid witness file) 6.1 3.2 110 300
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect 3.3   3.2   45    240 .84 0   - - true 25    20    560   590 error 11   6.1 170 320
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect 3.3   3.2   45    240 .84 0   - - true 25    20    380   590 error 10   5.6 150 290
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect 3.3   3.2   48    240 .84 0   - - true 25    20    380   580 error 11   5.6 160 300
loop-industry-pattern/aiob_4_true-unreach-call.c unknown 0 wit inspect .11  .11  1.4  25 .84 0   - - error (invalid witness file) .48 .32 6.4 39 error (invalid witness file) 6.2 3.3 120 300
loop-industry-pattern/mod3_true-unreach-call.c unknown 0 wit inspect 2.5   2.5   31    23 .84 0   - - error (invalid witness file) .51 .34 8.4 40 error (invalid witness file) 6.7 3.5 130 300
loop-industry-pattern/nested_true-unreach-call.c timeout 0 wit inspect 900     900     6900    2600 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 7.2 3.7 140 320
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect .13  .13  1.1  25 .84 0   - - error (invalid witness file) .49 .33 4.0 41 error (invalid witness file) 5.3 2.8 100 290
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect .10  .10  1.1  25 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.2 3.3 100 300
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect .13  .13  1.0  25 .84 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.2 3.3 110 300
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect .10  .10  1.1  25 .84 0   - - error (invalid witness file) .53 .34 11   43 error (invalid witness file) 6.2 3.3 120 290
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect .13  .13  1.2  25 .84 0   - - error (invalid witness file) .50 .34 7.1 39 error (invalid witness file) 5.3 2.9 110 290
loops/heavy_true-unreach-call.c true 1 wit inspect 19     19     240    4400 .84 0   - - timeout 900    890    8800   3700 timeout 960   880   12000 6600
loops/compact_false-unreach-call.c timeout 0 wit inspect 900     900     2500    460 .84 0   error (invalid witness file) .51 .33 7.2 41 error (invalid witness file) 6.1 3.2 99 290 - -
loops/heavy_false-unreach-call.c out of memory 0 wit inspect 640     640     7400    15000 .84 0   error (invalid witness file) .52 .34 13   40 error (invalid witness file) 5.8 3.1 89 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 118 44000 44000 450000 510000 130   0   156 350 260 6700 13000   156 740 460 9900 37000   156 3900 3700 62000 39000   156 7000 5700 88000 68000  
    correct results 75 116 1100 1100 11000 9900 64   0   33 240 170 4600 11000   32 420 230 5800 19000   39 2000 1900 35000 27000   34 5600 4600 69000 36000  
        correct true 41 82 260 260 2800 4700 35   0   3 0 0 0 0   7 0 0 0 0   39 2000 1900 35000 27000   34 5600 4600 69000 36000  
        correct false 34 34 820 820 8100 5200 29   0   30 240 170 4600 11000   25 420 230 5800 19000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 6 2 33 33 410 4800 5.0 0   3 110 84 2000 1900   1 250 190 2700 14000   0 1800 1800 26000 9500   0 1000 920 12000 14000  
        correct-unconfirmed true 2 2 21 21 260 4400 1.7 0   3 0 0 0 0   1 0 0 0 0   0 1800 1800 26000 9500   0 1000 920 12000 14000  
        correct-unconfirmed false 4 0 12 12 150 380 3.4 0   0 110 84 2000 1900   0 250 190 2700 14000   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) 118
Run set sv-comp17.ReachSafety-Loops