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-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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 .099 .098 1.1  23 .84 0   false(unreach-call) 4.8  2.7  56   280 false(unreach-call) 7.4 4.0 140 320 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect .64  .63  6.9  49 .84 0   false(unreach-call) 6.2  3.4  100   300 error 13   7.2 150 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .68 23 .84 0   false(unreach-call) 4.7  2.6  56   270 false(unreach-call) 8.8 4.7 110 320 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 0 wit inspect .15  .15  1.9  23 .84 0   true 5.3  2.9  60   280 true 7.8 4.2 120 330 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .076 .075 .83 23 .84 0   false(unreach-call) 4.7  2.6  57   270 false(unreach-call) 7.5 4.0 94 330 - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .66  .65  7.5  23 .84 0   timeout 91    87    1600   1200 false(unreach-call) 31   18   360 670 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16  .16  1.9  23 .84 0   true 5.2  2.9  56   270 false(unreach-call) 13   6.8 150 360 - -
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect .50  .49  6.3  41 .84 0   true 6.2  3.4  68   290 timeout 98   83   1100 740 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 2.1   2.1   29    31 .84 0   true 5.9  3.2  110   290 out of memory 48   39   480 7000 - -
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12  .12  1.3  23 .84 0   false(unreach-call) 8.8  5.8  130   470 true 8.0 4.3 130 330 - -
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 340     330     3900    15000 .84 0   error (invalid witness file) .51 .32 8.3 40 error (invalid witness file) 5.3 2.9 94 290 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .073 .073 .80 23 .84 0   false(unreach-call) 3.8  2.1  78   270 false(unreach-call) 8.7 4.6 130 340 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .077 .077 .89 23 .84 0   false(unreach-call) 5.1  2.8  60   290 false(unreach-call) 7.1 3.9 140 340 - -
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 370     370     3600    2600 .84 0   false(unreach-call) 13    6.9  170   480 true 11   5.7 170 340 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15  .15  1.8  23 .84 0   false(unreach-call) 5.3  2.9  100   290 false(unreach-call) 29   16   270 480 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .092 .090 1.1  23 .84 0   false(unreach-call) 6.8  3.7  80   290 false(unreach-call) 16   8.8 220 470 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .83 23 .84 0   true 4.3  2.4  67   270 false(unreach-call) 14   8.0 120 370 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .14  .13  1.3  23 .84 0   false(unreach-call) 7.4  4.0  93   300 false(unreach-call) 16   8.9 280 490 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .093 .092 1.0  23 .84 0   false(unreach-call) 5.7  3.1  58   280 true 7.1 3.8 110 320 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .073 .073 .80 23 .84 0   false(unreach-call) 4.1  2.3  87   270 true 7.9 4.2 98 310 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .15  .15  2.0  23 .84 0   false(unreach-call) 4.8  2.7  65   300 false(unreach-call) 7.7 4.2 110 350 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .077 .076 .73 23 .84 0   false(unreach-call) 4.3  2.4  55   280 false(unreach-call) 8.9 4.7 170 340 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .10  .73 23 .84 0   false(unreach-call) 3.7  2.1  71   270 false(unreach-call) 9.6 5.1 100 320 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .074 .074 .86 23 .84 0   false(unreach-call) 4.0  2.2  51   280 false(unreach-call) 7.4 4.0 120 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .076 .075 .99 23 .84 0   false(unreach-call) 3.8  2.1  77   280 false(unreach-call) 9.0 4.8 140 330 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .079 .079 .86 23 .84 0   false(unreach-call) 4.7  2.6  46   270 false(unreach-call) 7.8 4.1 120 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .080 .080 2.0  23 .84 0   false(unreach-call) 4.8  2.7  52   270 false(unreach-call) 8.5 4.5 66 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .099 .098 .94 23 .84 0   true 4.4  2.4  73   290 false(unreach-call) 12   6.3 200 380 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16  .16  1.2  23 .84 0   false(unreach-call) 4.6  2.5  89   290 true 7.8 4.2 85 330 - -
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect .57  .57  7.1  38 .84 0   timeout 92    86    1400   590 true 17   9.0 230 420 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .077 .076 .68 23 .84 0   false(unreach-call) 3.7  2.1  57   270 true 6.8 3.6 98 310 - -
loops/array_true-unreach-call_true-termination.i out of memory 0 wit inspect 170     160     2400    15000 .84 0   - - error (invalid witness file) .53 .32 8.9 40 error (invalid witness file) 6.0 3.2 120 300
loops/bubble_sort_true-unreach-call.i timeout 0 wit inspect 900     900     8900    1100 .84 0   - - error (invalid witness file) .55 .35 13   41 error (invalid witness file) 7.0 3.7 120 320
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    2200 .84 0   - - error (invalid witness file) .47 .30 8.7 40 error (invalid witness file) 5.7 3.0 110 300
loops/eureka_01_true-unreach-call.i out of memory 0 wit inspect 400     380     6000    15000 .84 0   - - error (invalid witness file) .49 .31 6.7 39 error (invalid witness file) 6.2 3.3 120 300
loops/eureka_05_true-unreach-call_true-termination.i out of memory 0 wit inspect 130     120     1900    15000 .84 0   - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.5 3.0 85 300
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout 0 wit inspect 900     850     12000    13000 .84 0   - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.2 3.3 130 310
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout 0 wit inspect 900     850     13000    13000 .84 0   - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 6.0 3.1 120 290
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    120 .84 0   - - error (invalid witness file) .52 .35 4.1 41 error (invalid witness file) 6.3 3.3 110 300
loops/invert_string_true-unreach-call_true-termination.i out of memory 0 wit inspect 110     100     1300    15000 .84 0   - - error (invalid witness file) .49 .30 6.1 41 error (invalid witness file) 6.8 3.5 130 310
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     900     13000    5800 .84 0   - - error (invalid witness file) .50 .33 10   41 error (invalid witness file) 5.6 3.1 120 290
loops/lu.cmp_true-unreach-call.i timeout 0 wit inspect 900     860     12000    5200 .84 0   - - error (invalid witness file) .53 .33 11   41 error (invalid witness file) 6.4 3.4 130 310
loops/matrix_true-unreach-call_true-termination.i out of memory 0 wit inspect 230     220     2900    15000 .84 0   - - error (invalid witness file) .50 .31 8.3 40 error (invalid witness file) 5.7 3.1 100 300
loops/n.c11_true-unreach-call_false-termination.i timeout 0 wit inspect 900     880     2900    8800 .84 0   - - error (invalid witness file) .49 .32 4.6 40 error (invalid witness file) 6.0 3.2 120 300
loops/n.c40_true-unreach-call_true-termination.i out of memory 0 wit inspect 49     47     590    15000 .84 0   - - error (invalid witness file) .53 .35 5.5 41 error (invalid witness file) 6.4 3.4 140 300
loops/nec40_true-unreach-call_true-termination.i timeout 0 wit inspect 900     850     13000    6800 .84 0   - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.9 3.6 130 320
loops/string_true-unreach-call_true-termination.i out of memory 0 wit inspect 660     650     6300    15000 .84 0   - - error (invalid witness file) .51 .33 8.0 44 error (invalid witness file) 6.2 3.3 140 300
loops/sum01_true-unreach-call_true-termination.i out of memory 0 wit inspect 290     290     3500    15000 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.9 3.2 130 300
loops/sum03_true-unreach-call_false-termination.i timeout 0 wit inspect 900     860     13000    9700 .84 0   - - error (invalid witness file) .50 .31 6.4 39 error (invalid witness file) 5.7 3.1 110 300
loops/sum04_true-unreach-call_true-termination.i timeout 0 wit inspect 900     810     12000    8700 .84 0   - - error (invalid witness file) .50 .32 13   39 error (invalid witness file) 6.2 3.3 100 300
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     900     2800    330 .84 0   - - error (invalid witness file) .54 .35 10   42 error (invalid witness file) 5.9 3.2 110 300
loops/terminator_02_true-unreach-call_true-termination.i out of memory 0 wit inspect 510     510     5400    15000 .84 0   - - error (invalid witness file) .50 .31 9.9 39 error (invalid witness file) 6.2 3.2 120 300
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9600    3700 .84 0   - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 5.8 3.1 110 300
loops/trex01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.8 3.1 94 300
loops/trex02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9300    4000 .84 0   - - error (invalid witness file) .49 .32 9.4 39 error (invalid witness file) 6.3 3.4 110 310
loops/trex03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9500    3800 .84 0   - - error (invalid witness file) .48 .31 8.8 39 error (invalid witness file) 6.3 3.3 110 300
loops/trex04_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     10000    3900 .84 0   - - error (invalid witness file) .53 .33 11   39 error (invalid witness file) 6.1 3.2 120 290
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i out of memory 0 wit inspect 360     350     4200    15000 .84 0   - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.1 3.2 110 290
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i timeout 0 wit inspect 900     890     12000    6900 .84 0   - - error (invalid witness file) .52 .32 8.3 40 error (invalid witness file) 5.8 3.1 110 290
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i out of memory 0 wit inspect 360     350     4500    15000 .84 0   - - error (invalid witness file) .54 .34 6.6 40 error (invalid witness file) 5.9 3.1 130 300
loops/vogal_true-unreach-call.i timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .57 .36 9.0 43 error (invalid witness file) 6.2 3.3 100 300
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 740     680     9200    15000 .84 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.9 3.2 120 300
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 740     680     9900    15000 .84 0   - - error (invalid witness file) .51 .34 6.8 39 error (invalid witness file) 6.5 3.4 110 310
loops/while_infinite_loop_3_true-unreach-call_false-termination.i timeout 0 wit inspect 900     850     13000    15000 .84 0   - - error (invalid witness file) .49 .32 8.4 41 error (invalid witness file) 5.7 3.1 110 300
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 300     290     3900    510 .84 0   timeout 97    90    1300   2500 timeout 97   78   1800 5000 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 110     100     1500    1200 .84 0   timeout 96    84    1500   1600 timeout 96   65   1000 6300 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 300     300     4000    700 .84 0   timeout 97    82    1600   2700 timeout 97   77   1200 5000 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 10     8.5   120    130 .84 0   false(unreach-call) 22    12    170   1000 true 7.6 4.0 140 320 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 1.3   1.3   17    150 .92 0   false(unreach-call) 7.1  3.8  83   300 timeout 92   54   690 7000 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 640     580     9400    15000 .84 0   error (invalid witness file) .55 .35 12   42 error (invalid witness file) 6.6 3.5 110 310 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .81 23 .84 0   false(unreach-call) 4.0  2.2  41   270 false(unreach-call) 7.2 3.8 120 320 - -
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900     740     11000    8200 .84 0   error (invalid witness file) .68 .42 9.6 41 error (invalid witness file) 6.3 3.3 100 300 - -
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900     790     11000    5700 .84 0   error (invalid witness file) .51 .32 13   40 error (invalid witness file) 5.8 3.1 89 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .096 .095 .78 23 .84 0   false(unreach-call) 4.7  2.6  58   270 false(unreach-call) 7.6 4.0 140 320 - -
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900     720     11000    9100 .84 0   error (invalid witness file) .56 .36 8.6 39 error (invalid witness file) 6.4 3.4 76 280 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .11  .11  .66 23 .84 0   false(unreach-call) 3.9  2.2  57   270 false(unreach-call) 7.0 3.8 140 310 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .086 .087 .79 23 .84 0   false(unreach-call) 4.4  2.5  42   270 false(unreach-call) 7.0 3.8 100 320 - -
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900     720     13000    9000 .84 0   error (invalid witness file) .59 .39 6.7 40 error (invalid witness file) 5.3 2.8 85 290 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .073 .072 .89 23 .84 0   false(unreach-call) 4.2  2.3  88   280 true 7.4 4.0 110 310 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .075 .075 .80 23 .84 0   false(unreach-call) 3.7  2.1  60   270 true 9.0 4.8 76 330 - -
loop-acceleration/array_true-unreach-call1_true-termination.i out of memory 0 wit inspect 180     160     2200    15000 .84 0   - - error (invalid witness file) .54 .35 11   39 error (invalid witness file) 6.2 3.3 110 300
loop-acceleration/array_true-unreach-call2_true-termination.i out of memory 0 wit inspect 270     250     3400    15000 .84 0   - - error (invalid witness file) .48 .30 10   39 error (invalid witness file) 6.0 3.2 120 300
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     900     11000    4600 .84 0   - - error (invalid witness file) .60 .38 6.4 42 error (invalid witness file) 6.0 3.2 120 300
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900     900     11000    4800 .84 0   - - error (invalid witness file) .52 .34 7.1 40 error (invalid witness file) 5.5 3.0 100 280
loop-acceleration/const_true-unreach-call1.i timeout 0 wit inspect 900     760     2200    1700 .84 0   - - error (invalid witness file) .50 .31 6.1 40 error (invalid witness file) 5.6 3.0 110 290
loop-acceleration/diamond_true-unreach-call1_true-termination.i out of memory 0 wit inspect 160     160     2100    15000 .84 0   - - error (invalid witness file) .49 .32 8.6 40 error (invalid witness file) 5.9 3.1 120 290
loop-acceleration/diamond_true-unreach-call2.i out of memory 0 wit inspect 550     550     1400    15000 .84 0   - - error (invalid witness file) .58 .38 7.0 42 error (invalid witness file) 6.5 3.4 120 300
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 640     580     8900    15000 .84 0   - - error (invalid witness file) .47 .31 5.6 39 error (invalid witness file) 5.2 2.9 96 290
loop-acceleration/multivar_true-unreach-call1_true-termination.i out of memory 0 wit inspect 210     210     2700    15000 .84 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.6 3.0 110 290
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900     740     11000    8200 .84 0   - - error (invalid witness file) .48 .30 11   40 error (invalid witness file) 6.2 3.3 120 300
loop-acceleration/overflow_true-unreach-call1.i timeout 0 wit inspect 900     720     11000    9200 .84 0   - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.1 3.2 110 290
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900     790     12000    5700 .84 0   - - error (invalid witness file) .50 .32 6.2 42 error (invalid witness file) 5.4 2.9 110 280
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 0 wit inspect 900     900     7300    13000 .84 0   - - error (invalid witness file) .50 .34 12   43 error (invalid witness file) 5.7 3.0 110 290
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900     720     11000    9200 .84 0   - - error (invalid witness file) .51 .32 9.5 41 error (invalid witness file) 5.9 3.2 110 290
loop-acceleration/simple_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     900     11000    4300 .84 0   - - error (invalid witness file) .51 .31 12   40 error (invalid witness file) 5.9 3.1 110 300
loop-acceleration/simple_true-unreach-call3_true-termination.i out of memory 0 wit inspect 130     130     1800    15000 .84 0   - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.0 3.2 110 300
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900     720     11000    9100 .84 0   - - error (invalid witness file) .52 .34 14   42 error (invalid witness file) 6.8 3.6 130 310
loop-acceleration/underapprox_true-unreach-call1_true-termination.i timeout 0 wit inspect 900     820     11000    9100 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 5.8 3.1 110 300
loop-acceleration/underapprox_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     810     11000    9400 .84 0   - - error (invalid witness file) .47 .31 6.4 39 error (invalid witness file) 6.0 3.2 110 300
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .30  .30  .99 23 .84 0   false(unreach-call) 3.9  2.2  69   280 false(unreach-call) 7.4 4.0 160 320 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    770 .84 0   - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.2 3.3 130 300
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i out of memory 0 wit inspect 410     400     4600    15000 .84 0   - - error (invalid witness file) .50 .34 5.2 39 error (invalid witness file) 5.5 3.0 100 300
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     900     10000    140 .84 0   - - error (invalid witness file) .49 .33 10   40 error (invalid witness file) 5.9 3.2 120 290
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     1800    110 .84 0   - - error (invalid witness file) .55 .36 13   43 error (invalid witness file) 6.1 3.2 120 300
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    220 .84 0   - - error (invalid witness file) .52 .32 9.0 40 error (invalid witness file) 6.5 3.4 130 320
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8800    6900 .84 0   - - error (invalid witness file) .53 .35 14   42 error (invalid witness file) 6.9 3.6 93 290
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    15000 .84 0   - - error (invalid witness file) .51 .34 6.7 39 error (invalid witness file) 6.9 3.6 120 310
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     9400    4400 .99 0   - - error (invalid witness file) .48 .32 3.7 40 error (invalid witness file) 5.7 3.1 120 300
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     7600    1200 .84 0   - - error (invalid witness file) .57 .37 14   43 error (invalid witness file) 6.2 3.3 110 310
loop-invgen/id_build_true-unreach-call_true-termination.i out of memory 0 wit inspect 420     420     5300    15000 .84 0   - - error (invalid witness file) .53 .34 5.7 39 error (invalid witness file) 5.6 3.0 100 280
loop-invgen/large_const_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     8400    14000 .84 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.5 2.9 86 300
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     7700    1200 .84 0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.7 3.0 110 300
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     10000    1600 .84 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.0 3.2 120 310
loop-invgen/nested9_true-unreach-call_true-termination.i out of memory 0 wit inspect 330     330     3900    15000 .84 0   - - error (invalid witness file) .51 .34 7.4 40 error (invalid witness file) 5.5 3.0 120 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     12000    4100 .84 0   - - error (invalid witness file) .52 .35 8.1 42 error (invalid witness file) 5.9 3.1 120 300
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     11000    690 .99 0   - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.0 3.2 120 290
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i out of memory 0 wit inspect 74     74     810    15000 .84 0   - - error (invalid witness file) .50 .32 6.9 41 error (invalid witness file) 5.8 3.1 110 300
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     13000    10000 .84 0   - - error (invalid witness file) .49 .33 6.8 40 error (invalid witness file) 6.7 3.5 97 310
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    3500 .84 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.8 3.1 100 310
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    84 .84 0   - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.2 3.3 130 300
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     820     11000    9600 .84 0   - - error (invalid witness file) .53 .33 7.6 39 error (invalid witness file) 5.9 3.2 110 290
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9200    3300 .84 0   - - error (invalid witness file) .53 .36 13   40 error (invalid witness file) 5.7 3.1 110 290
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     790     11000    5800 .84 0   - - error (invalid witness file) .54 .35 8.6 40 error (invalid witness file) 5.6 3.0 89 300
loop-lit/css2003_true-unreach-call_true-termination.c.i out of memory 0 wit inspect 450     440     5400    15000 .84 0   - - error (invalid witness file) .57 .35 9.8 44 error (invalid witness file) 5.9 3.2 110 290
loop-lit/ddlm2013_true-unreach-call.i out of memory 0 wit inspect 170     170     1400    15000 .84 0   - - error (invalid witness file) .55 .35 12   39 error (invalid witness file) 6.2 3.3 130 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     790     11000    5600 .84 0   - - error (invalid witness file) .49 .31 5.7 40 error (invalid witness file) 6.0 3.2 120 300
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     13000    5100 .84 0   - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 5.4 2.9 120 290
loop-lit/gr2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     800     11000    5000 .84 0   - - error (invalid witness file) .70 .45 9.7 40 error (invalid witness file) 6.7 3.5 130 310
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     2300    1500 .84 0   - - error (invalid witness file) .49 .32 9.3 40 error (invalid witness file) 6.1 3.2 130 310
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    420 .84 0   - - error (invalid witness file) .67 .41 7.1 40 error (invalid witness file) 6.1 3.2 120 300
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     12000    2300 .84 0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 5.6 3.0 120 290
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     11000    2000 .84 0   - - error (invalid witness file) .53 .34 7.3 39 error (invalid witness file) 5.7 3.1 110 300
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     900     9200    150 .84 0   - - error (invalid witness file) .49 .32 8.9 40 error (invalid witness file) 6.7 3.5 120 320
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .093 .094 .78 23 .84 0   false(unreach-call) 4.2  2.4  59   290 false(unreach-call) 7.3 3.9 78 330 - -
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900     720     12000    10000 .84 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.9 3.6 140 310
loop-new/count_by_1_variant_true-unreach-call_true-termination.i timeout 0 wit inspect 900     840     14000    14000 .84 0   - - error (invalid witness file) .50 .33 9.1 40 error (invalid witness file) 5.9 3.1 120 300
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     730     13000    10000 .84 0   - - error (invalid witness file) .50 .34 4.7 41 error (invalid witness file) 5.9 3.1 110 300
loop-new/count_by_k_true-unreach-call_true-termination.i out of memory 0 wit inspect 150     150     1700    15000 .84 0   - - error (invalid witness file) .54 .35 9.6 41 error (invalid witness file) 5.9 3.2 120 290
loop-new/count_by_nondet_true-unreach-call_true-termination.i out of memory 0 wit inspect 330     330     2900    15000 .84 0   - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 5.3 2.8 110 290
loop-new/gauss_sum_true-unreach-call_true-termination.i out of memory 0 wit inspect 530     530     6200    15000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.3 110 300
loop-new/half_true-unreach-call_true-termination.i out of memory 0 wit inspect 400     400     5500    15000 .84 0   - - error (invalid witness file) .49 .31 9.6 39 error (invalid witness file) 6.8 3.5 100 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900     7100    2900 .84 0   - - error (invalid witness file) .67 .43 7.4 40 error (invalid witness file) 6.2 3.3 130 300
loop-industry-pattern/aiob_1_true-unreach-call.c out of memory 0 wit inspect 290     280     4700    15000 .84 0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.8 3.5 120 320
loop-industry-pattern/aiob_2_true-unreach-call.c out of memory 0 wit inspect 290     280     3900    15000 .84 0   - - error (invalid witness file) .57 .36 13   44 error (invalid witness file) 5.8 3.1 130 300
loop-industry-pattern/aiob_3_true-unreach-call.c out of memory 0 wit inspect 290     280     3900    15000 .84 0   - - error (invalid witness file) .49 .32 8.9 42 error (invalid witness file) 5.6 3.0 100 280
loop-industry-pattern/aiob_4_true-unreach-call.c out of memory 0 wit inspect 300     280     4000    15000 .84 0   - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.6 3.5 130 310
loop-industry-pattern/mod3_true-unreach-call.c timeout 0 wit inspect 900     900     12000    130 .84 0   - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 5.7 3.1 87 290
loop-industry-pattern/nested_true-unreach-call.c timeout 0 wit inspect 900     880     10000    530 .84 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.7 3.5 120 300
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect .66  .66  9.1  25 .84 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.5 3.5 100 290
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect .69  .68  7.8  25 .84 0   - - error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.0 3.2 110 300
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect .65  .65  8.4  25 .84 0   - - error (invalid witness file) .54 .34 9.6 44 error (invalid witness file) 6.1 3.2 110 300
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect .64  .63  7.5  25 .84 0   - - error (invalid witness file) .49 .31 7.4 39 error (invalid witness file) 6.1 3.3 130 300
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect .60  .59  8.1  25 .84 0   - - error (invalid witness file) .69 .43 8.5 42 error (invalid witness file) 6.1 3.3 120 300
loops/heavy_true-unreach-call.c timeout 0 wit inspect 900     900     11000    4400 .84 0   - - error (invalid witness file) .51 .35 6.1 39 error (invalid witness file) 6.0 3.2 130 300
loops/compact_false-unreach-call.c timeout 0 wit inspect 900     840     11000    7000 .84 0   error (invalid witness file) .53 .35 6.8 39 error (invalid witness file) 7.2 3.8 73 300 - -
loops/heavy_false-unreach-call.c timeout 0 wit inspect 900     900     12000    4400 .84 0   error (invalid witness file) .52 .33 8.5 39 error (invalid witness file) 7.0 3.7 65 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 36 78000 75000 910000 960000 130   0   156 690 550 10000 21000 156 960 630 12000 46000 156 55 35 990 4200   156 640 340 12000 31000  
    correct results 36 36 390 390 3700 3600 30   0   35 290 200 4200 12000 34 450 250 5700 19000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 36 36 390 390 3700 3600 30   0   32 290 200 4200 12000 25 450 250 5700 19000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 7 0 700 690 9500 2600 5.9 0   3 400 350 6000 8200 2 460 350 6000 25000 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 7 0 700 690 9500 2600 5.9 0   0 400 350 6000 8200 0 460 350 6000 25000 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) 36
Run set sv-comp17.ReachSafety-Loops