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