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-Recursive
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)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .16  .16  2.1  25 .84 0   false(unreach-call) 5.2  2.9  89   290 false(unreach-call) 11   6.0 170 380 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .13  .13  1.1  23 .84 0   false(unreach-call) 4.8  2.7  100   290 false(unreach-call) 7.4 3.9 140 320 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .10  .10  .89 23 .84 0   true 3.3  1.9  37   270 false(unreach-call) 7.2 3.9 140 310 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .079 .078 .75 23 .84 0   false(unreach-call) 4.0  2.2  52   280 false(unreach-call) 7.4 3.9 140 320 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .15  .15  1.8  25 .84 0   false(unreach-call) 53    35    530   1800 timeout 96   67   850 5500 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 1.0   .98  12    120 .84 0   timeout 97    68    1400   4400 timeout 98   70   1000 6100 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .087 .087 .73 23 .84 0   false(unreach-call) 4.1  2.3  50   290 false(unreach-call) 7.2 3.8 130 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     7000    2600 .84 0   - - error (invalid witness file) .53 .34 7.0 42 error (invalid witness file) 5.8 3.1 120 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     7500    2400 .84 0   - - error (invalid witness file) .61 .37 6.9 41 error (invalid witness file) 6.1 3.2 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     2500    1900 .84 0   - - error (invalid witness file) .50 .33 8.9 40 error (invalid witness file) 6.9 3.6 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 400     390     3200    15000 .84 0   - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.5 3.4 110 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 400     400     4100    15000 .84 0   - - error (invalid witness file) .52 .33 9.9 41 error (invalid witness file) 5.7 3.0 97 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 410     410     5100    15000 .84 0   - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.2 3.3 110 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8400    2200 .84 0   - - error (invalid witness file) .51 .32 9.7 40 error (invalid witness file) 6.6 3.5 96 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .48  .47  7.5  33 .84 0   - - error (recursion) 3.7  2.1  54   250 true 29   17   350 1400
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    3900 .99 0   - - error (invalid witness file) .60 .39 5.4 39 error (invalid witness file) 6.1 3.2 97 310
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8400    4700 .84 0   - - error (invalid witness file) .50 .32 8.8 40 error (invalid witness file) 5.3 2.8 100 280
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     6400    2900 .84 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.1 3.2 120 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 520     520     4300    15000 .84 0   - - error (invalid witness file) .50 .32 8.9 39 error (invalid witness file) 5.9 3.1 110 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     14000    160 .84 0   - - error (invalid witness file) .49 .33 7.1 40 error (invalid witness file) 7.0 3.7 120 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    850 .84 0   - - error (invalid witness file) .57 .38 8.9 40 error (invalid witness file) 5.9 3.1 110 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 470     470     5200    15000 .84 0   - - error (invalid witness file) .53 .33 12   39 error (invalid witness file) 5.9 3.1 120 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.5   1.4   21    110 .84 0   - - error (recursion) 3.7  2.1  74   260 true 9.2 4.9 140 360
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.8   1.8   24    110 .84 0   - - error (recursion) 3.3  1.9  48   260 timeout 960   950   12000 2600
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .094 .094 .76 23 .84 0   false(unreach-call) 3.5  2.0  57   270 true 7.4 3.9 140 310 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .074 .073 .95 23 .84 0   false(unreach-call) 3.3  1.9  26   280 true 7.5 3.9 130 310 - -
recursive-simple/fibo_10_false-unreach-call.c false(unreach-call) 1 wit inspect 1.1   1.1   12    39 .84 0   false(unreach-call) 8.6  4.6  150   450 true 7.2 3.9 150 320 - -
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 390     390     4900    270 .84 0   false(unreach-call) 37    26    650   1900 true 7.3 3.9 130 340 - -
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 900     900     9200    310 .84 0   error (invalid witness file) .49 .32 8.2 41 error (invalid witness file) 6.2 3.3 120 300 - -
recursive-simple/fibo_25_false-unreach-call.c timeout 0 wit inspect 900     900     9700    310 .84 0   error (invalid witness file) .50 .31 11   41 error (invalid witness file) 6.4 3.4 120 300 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .73  .72  8.3  29 .84 0   false(unreach-call) 9.0  4.8  140   470 true 7.2 3.8 130 320 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 200     200     2400    150 .84 0   false(unreach-call) 39    28    600   2100 true 6.9 3.7 110 310 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 900     900     8600    240 .84 0   error (invalid witness file) .51 .32 13   40 error (invalid witness file) 5.9 3.1 120 300 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 900     900     11000    240 .85 0   error (invalid witness file) .62 .39 9.2 40 error (invalid witness file) 6.6 3.5 130 310 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .075 .075 .80 23 .99 0   false(unreach-call) 3.7  2.1  64   280 true 7.2 3.9 150 310 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .077 .98 23 .84 0   false(unreach-call) 4.5  2.5  85   280 true 7.7 4.1 140 330 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .083 .082 1.1  23 .84 0   false(unreach-call) 4.8  2.6  84   290 true 7.2 3.9 150 320 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .13  1.3  23 .84 0   false(unreach-call) 5.6  3.0  88   300 true 6.8 3.7 140 310 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c false(unreach-call) 1 wit inspect .15  .15  1.8  23 .84 0   false(unreach-call) 7.8  4.1  81   300 true 7.0 3.8 150 320 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .099 1.2  23 .84 0   false(unreach-call) 4.5  2.5  74   300 true 6.6 3.6 120 310 - -
recursive-simple/fibo_7_false-unreach-call.c false(unreach-call) 1 wit inspect .16  .15  1.9  25 .84 0   false(unreach-call) 5.2  2.8  74   290 true 7.0 3.7 100 320 - -
recursive-simple/id2_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .085 .085 .82 23 .84 0   false(unreach-call) 5.2  2.8  76   290 false(unreach-call) 8.3 4.4 150 340 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .077 .91 23 .84 0   false(unreach-call) 4.3  2.4  68   280 true 7.5 4.0 120 320 - -
recursive-simple/id_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .091 .090 .91 23 .84 0   false(unreach-call) 4.3  2.4  72   280 false(unreach-call) 9.6 5.2 160 350 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .10  1.4  23 .84 0   false(unreach-call) 4.3  2.4  55   290 true 7.9 4.2 150 330 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .54  .50  1.2  25 .84 0   false(unreach-call) 4.8  2.7  94   290 true 6.8 3.7 120 310 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  .17  2.2  30 .84 0   false(unreach-call) 4.7  2.5  51   280 true 7.2 3.8 150 310 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20  .19  2.5  35 .84 0   false(unreach-call) 5.0  2.7  52   280 true 7.0 3.8 130 310 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .089 .088 .89 23 .84 0   false(unreach-call) 4.1  2.3  71   280 true 6.4 3.5 110 300 - -
recursive-simple/id_o1000_false-unreach-call.c out of memory 0 wit inspect 740     730     8500    15000 .84 0   error (invalid witness file) .50 .34 6.6 39 error (invalid witness file) 6.7 3.5 130 320 - -
recursive-simple/id_o100_false-unreach-call.c false(unreach-call) 0 wit inspect 16     15     210    810 .99 0   timeout 97    75    2400   4000 timeout 98   68   1100 4600 - -
recursive-simple/id_o10_false-unreach-call.c false(unreach-call) 1 wit inspect .17  .16  2.5  29 .84 0   false(unreach-call) 7.0  3.7  130   330 timeout 98   59   750 6700 - -
recursive-simple/id_o200_false-unreach-call.c false(unreach-call) 0 wit inspect 110     110     1600    3700 .84 0   timeout 96    76    1000   4100 timeout 97   69   1500 6300 - -
recursive-simple/id_o20_false-unreach-call.c false(unreach-call) 1 wit inspect .46  .44  5.0  56 .84 0   false(unreach-call) 15    7.8  180   560 timeout 98   64   900 6200 - -
recursive-simple/id_o3_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  1.2  23 .84 0   false(unreach-call) 4.6  2.5  97   270 false(unreach-call) 8.6 4.6 150 340 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .13  1.3  23 .84 0   false(unreach-call) 4.3  2.4  69   280 true 6.8 3.6 130 310 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  1.8  25 .84 0   false(unreach-call) 4.4  2.5  60   270 true 6.7 3.6 120 310 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .21  .20  2.1  30 .84 0   false(unreach-call) 4.9  2.7  100   290 true 6.7 3.6 140 310 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .22  .21  2.6  35 .84 0   false(unreach-call) 5.2  2.8  94   280 true 6.7 3.6 140 310 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .090 .089 1.1  23 .84 0   false(unreach-call) 4.1  2.2  53   280 true 6.5 3.5 120 310 - -
recursive-simple/sum_non_eq_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .83 23 .84 0   false(unreach-call) 4.0  2.2  86   280 false(unreach-call) 7.3 3.9 140 320 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  .72 23 .84 0   false(unreach-call) 3.6  2.0  48   270 false(unreach-call) 7.3 3.8 140 320 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .085 .085 .82 23 .84 0   - - true 3.4  1.9  34   270 true 8.8 4.7 120 310
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .072 .072 .77 23 .84 0   - - true 3.3  1.9  73   260 true 7.3 4.0 150 310
recursive-simple/fibo_10_true-unreach-call.c true 2 wit inspect 1.0   1.0   12    43 .84 0   - - error (recursion) 3.4  1.9  33   260 true 40   23   390 2800
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 450     450     5300    310 .84 0   - - error (recursion) 3.8  2.1  58   250 true 620   560   14000 6300
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900     900     13000    310 .84 0   - - error (invalid witness file) .55 .34 7.8 42 error (invalid witness file) 5.9 3.1 100 300
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900     900     11000    310 .84 0   - - error (invalid witness file) .52 .33 9.8 42 error (invalid witness file) 5.3 2.9 110 290
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .64  .63  6.8  30 .84 0   - - error (recursion) 3.8  2.1  86   270 true 82   50   690 4200
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 270     270     3700    210 .84 0   - - error (recursion) 5.6  3.1  49   270 timeout 960   890   13000 5500
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900     900     12000    240 .84 0   - - error (invalid witness file) .56 .36 5.6 39 error (invalid witness file) 6.1 3.2 100 300
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900     900     11000    240 .84 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 5.8 3.1 110 290
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .086 .086 .65 23 .84 0   - - true 4.3  2.4  48   260 true 12   6.5 150 390
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  .86 23 .99 0   - - error (recursion) 4.0  2.2  54   260 true 19   11   230 540
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  .94 23 .84 0   - - error (recursion) 3.5  2.0  72   260 true 23   13   250 590
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  1.0  23 .84 0   - - error (recursion) 3.4  1.9  43   260 true 35   20   460 720
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .16  .16  4.3  23 .84 0   - - error (recursion) 3.6  2.0  64   260 true 51   29   640 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .10  .10  1.2  23 .99 0   - - error (recursion) 3.8  2.1  67   260 true 16   8.9 240 520
recursive-simple/fibo_7_true-unreach-call.c true 2 wit inspect .22  .22  2.6  25 .84 0   - - error (recursion) 3.6  2.0  76   260 true 20   12   320 660
recursive-simple/id2_b2_o3_true-unreach-call.c out of memory 0 wit inspect 410     410     4500    15000 .84 0   - - error (invalid witness file) .49 .32 4.2 40 error (invalid witness file) 5.2 2.8 100 290
recursive-simple/id2_b3_o5_true-unreach-call.c out of memory 0 wit inspect 450     440     6600    15000 .84 0   - - error (invalid witness file) .56 .36 9.0 40 error (invalid witness file) 5.9 3.2 110 300
recursive-simple/id2_b5_o10_true-unreach-call.c out of memory 0 wit inspect 410     410     5000    15000 .84 0   - - error (invalid witness file) .55 .35 7.4 43 error (invalid witness file) 5.3 2.9 94 290
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .092 .090 .90 23 .84 0   - - error (recursion) 3.6  2.0  50   260 true 13   7.5 170 470
recursive-simple/id_b2_o3_true-unreach-call.c out of memory 0 wit inspect 400     400     5600    15000 .84 0   - - error (invalid witness file) .48 .30 9.8 39 error (invalid witness file) 5.9 3.1 100 300
recursive-simple/id_b3_o5_true-unreach-call.c out of memory 0 wit inspect 460     450     6900    15000 .84 0   - - error (invalid witness file) .49 .31 9.1 40 error (invalid witness file) 5.3 2.9 100 300
recursive-simple/id_b5_o10_true-unreach-call.c out of memory 0 wit inspect 420     420     5600    15000 .84 0   - - error (invalid witness file) .64 .41 6.3 40 error (invalid witness file) 6.1 3.2 130 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .11  .11  1.3  23 .84 0   - - error (recursion) 3.4  1.9  55   250 true 17   9.6 210 550
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .15  .15  1.5  25 .84 0   - - error (recursion) 3.4  1.9  57   250 true 22   12   270 610
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .17  .16  2.2  30 .84 0   - - error (recursion) 3.5  2.0  73   260 true 31   18   320 720
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .21  .20  2.4  36 .84 0   - - error (recursion) 3.4  1.9  61   260 true 39   23   500 810
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .34  .33  .64 23 .84 0   - - error (recursion) 3.5  1.9  76   250 true 12   6.4 210 370
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .14  .14  1.3  23 .84 0   - - error (recursion) 3.6  2.0  67   270 true 19   11   280 570
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .15  .15  1.6  25 .99 0   - - error (recursion) 3.3  1.9  53   250 true 25   15   250 630
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .19  .18  2.7  30 .84 0   - - error (recursion) 3.3  1.9  55   260 true 34   20   390 790
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .25  .25  3.0  36 .98 0   - - error (recursion) 3.4  1.9  64   260 true 46   27   470 910
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .077 .076 1.0  23 .84 0   - - error (recursion) 3.6  2.0  48   260 true 11   6.3 160 390
recursive-simple/sum_non_eq_true-unreach-call.c timeout 0 wit inspect 900     900     13000    3200 .84 0   - - error (invalid witness file) .49 .31 6.1 40 error (invalid witness file) 5.6 3.0 91 280
recursive-simple/sum_non_true-unreach-call_true-termination.c out of memory 0 wit inspect 300     290     4200    15000 .84 0   - - error (invalid witness file) .51 .34 7.3 39 error (invalid witness file) 5.8 3.1 120 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 98 89 23000 23000 260000 230000 83   0   98 600 410 9400 29000   98 870 550 11000 48000   98 110   64   1800 8000   98 3300 2800 50000 43000  
    correct results 62 87 1000 1000 13000 2400 53   0   37 300 190 4500 16000   34 540 320 7100 29000   3 89   50   1500 6500   25 1200 920 22000 27000  
        correct true 25 50 460 460 5400 1000 22   0   1 0 0 0 0   24 0 0 0 0   3 89   50   1500 6500   25 1200 920 22000 27000  
        correct false 37 37 590 590 7400 1300 31   0   36 300 190 4500 16000   10 540 320 7100 29000   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 5 2 390 390 5500 5000 4.3 0   0 290 220 4800 12000   0 290 210 3600 17000   0 9.0 4.9 97 520   0 1900 1800 25000 8100  
        correct-unconfirmed true 2 2 270 270 3700 330 1.7 0   0 0 0 0 0   0 0 0 0 0   0 9.0 4.9 97 520   0 1900 1800 25000 8100  
        correct-unconfirmed false 3 0 120 120 1800 4600 2.7 0   0 290 220 4800 12000   0 290 210 3600 17000   0 0   0   0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 89
Run set sv-comp17.ReachSafety-Recursive