Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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 1.3  1.3  17    91 .082  0      15    7.7  230 530 12   6.4 230 420
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 .13 .12 1.1  19 .0041 0      5.3  2.9  43 290 7.9 4.2 170 330
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 .14 .13 1.0  17 .0041 0      3.5  2.0  77 260 8.9 4.7 94 320
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 .13 .12 1.2  18 .0041 0      3.7  2.1  37 280 7.7 4.1 140 310
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 .53 .52 5.0  30 .049  0      96    76    1200 3900 28   15   380 780
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 850    850    4100    260 .16   0      .50 .33 13 41 5.6 3.0 78 290
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 .15 .14 1.1  18 .0041 0      3.7  2.0  51 290 8.0 4.3 89 310
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 850    850    3700    370 .56   0      .53 .34 10   40 5.7 3.1 100 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 850    850    2000    340 .56   .0041 .70 .45 8.1 42 6.5 3.4 91 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 850    850    4200    370 .56   0      .54 .33 12   40 6.1 3.2 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    5600    8800 10      0      .51 .33 11   40 5.2 2.8 88 290
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 660    660    6800    15000 10      0      .54 .35 9.5 40 5.4 2.9 87 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    4600    8100 3.7    0      .57 .37 11   40 6.0 3.2 120 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 850    850    3300    250 .16   0      .51 .31 12   41 5.8 3.1 120 310
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 .48 .48 5.2  17 .13   0      3.7  2.1  52   260 32   18   580 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    3700    260 .16   0      .53 .34 12   40 5.5 2.9 100 290
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    3300    1300 5.8    .0041 .52 .32 12   40 5.9 3.2 98 310
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    3300    410 .28   0      .52 .33 9.5 40 5.8 3.1 120 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 850    850    2500    300 .012  0      .51 .33 11   40 6.0 3.1 93 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    6700    3300 .20   0      .51 .33 5.7 40 7.5 4.0 78 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    8300    180 .012  0      .50 .32 12   40 5.9 3.1 130 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 850    850    3500    800 9.6    0      .53 .35 6.8 40 6.9 3.7 70 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 1.0  1.0  11    22 .17   0      4.3  2.4  52   260 8.3 4.5 150 350
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 1 1.1  1.1  11    21 .17   0      3.5  1.9  68   260 960   950   24000 2600
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 .14 .13 .95 17 .0041 0      3.4  1.9  46 270 7.8 4.2 110 310
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 .13 .12 .90 17 .0041 0      3.6  2.0  70 280 9.9 5.4 130 340
recursive-simple/fibo_10_false-unreach-call.c 0 .48 .47 4.1  19 .20   0      98    69    1700 4800 97   63   1100 4900
recursive-simple/fibo_15_false-unreach-call.c 0 1.8  1.8  22    61 1.8    0      13    6.5  130 710 90   52   1300 7000
recursive-simple/fibo_20_false-unreach-call.c 0 180    180    1100    660 18      0      77    40    460 4600 98   53   1500 6600
recursive-simple/fibo_25_false-unreach-call.c 0 850    850    4300    390 .14   0      .53 .33 11 40 5.9 3.1 120 290
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 .32 .31 2.9  19 .18   0      97    68    1800 4800 97   61   1800 5700
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 1.6  1.6  22    67 1.9    0      17    8.9  200 740 88   51   1600 7000
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 210    210    1100    710 20      0      98    51    840 4800 96   53   1100 6200
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 850    850    3900    390 .041  0      .52 .33 13 40 6.8 3.6 140 310
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 .12 .12 .97 17 .0041 0      4.1  2.2  83 270 11   5.8 130 350
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 .15 .14 .78 17 .0041 0      10    5.4  230 460 19   10   310 500
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 .15 .14 1.1  17 .0041 0      19    9.6  270 670 34   18   420 740
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 .14 .13 .88 17 .0041 0      28    15    320 1500 44   23   790 960
recursive-simple/fibo_2calls_8_false-unreach-call.c 0 .28 .27 2.5  18 .082  0      97    69    1500 4900 98   63   1100 4100
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 .25 .25 3.2  17 .037  0      14    7.5  150 610 28   15   470 710
recursive-simple/fibo_7_false-unreach-call.c 1 .29 .28 2.4  17 .053  0      54    34    600 3200 61   40   720 2900
recursive-simple/id2_b3_o2_false-unreach-call.c 1 .13 .13 .91 18 .0041 0      5.4  2.9  91 280 9.5 5.1 140 340
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 .12 .11 .98 17 .0041 0      5.6  3.0  110 280 9.8 5.3 170 350
recursive-simple/id_b3_o2_false-unreach-call.c 1 .12 .11 .98 17 .0041 0      5.7  3.1  99 270 9.5 5.0 180 350
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 .38 .37 4.1  17 .053  0      6.6  3.6  110 290 7.2 3.9 150 310
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 .50 .49 6.3  17 .082  0      7.9  4.2  150 410 7.1 3.8 160 320
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 .74 .78 7.6  30 .11   13      10    5.2  84 460 8.9 4.7 140 320
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 .87 .86 7.0  17 .15   0      13    6.5  160 510 7.8 4.2 140 320
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 .27 .26 2.6  17 .025  0      4.7  2.6  92 290 9.9 5.3 190 350
recursive-simple/id_o1000_false-unreach-call.c 0 39    39    400    390 1.4    0      11    5.8  180 600 26   14   280 1600
recursive-simple/id_o100_false-unreach-call.c 0 1.8  1.8  21    41 .26   0      97    78    910 4100 13   6.7 110 520
recursive-simple/id_o10_false-unreach-call.c 1 .44 .43 3.9  20 .053  0      13    6.5  250 510 9.2 4.9 100 320
recursive-simple/id_o200_false-unreach-call.c 0 1.6  1.6  18    41 .34   0      97    73    2200 3700 15   7.5 150 580
recursive-simple/id_o20_false-unreach-call.c 1 .78 .77 7.6  20 .11   0      28    16    450 1200 10   5.4 110 320
recursive-simple/id_o3_false-unreach-call.c 1 .27 .26 2.7  17 .025  0      5.0  2.7  83 280 7.3 3.9 130 310
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 .42 .41 4.3  17 .053  0      6.2  3.3  130 290 7.7 4.1 160 320
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 .55 .54 5.3  19 .086  0      8.3  4.4  150 410 10   5.4 110 330
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 .72 .70 7.2  17 .12   0      11    5.6  240 460 8.4 4.5 160 320
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 .85 .84 8.6  17 .16   0      13    6.8  290 530 11   5.7 120 340
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 .14 .13 .91 17 .0041 0      4.4  2.4  93 280 8.7 4.6 180 340
recursive-simple/sum_non_eq_false-unreach-call.c 1 .13 .13 .92 17 .0041 0      3.9  2.1  83 280 9.0 4.7 92 320
recursive-simple/sum_non_false-unreach-call_true-termination.c 1 .12 .12 1.1  17 .0041 0      3.7  2.1  68 280 7.8 4.2 120 320
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 .18 .18 1.7  17 .0082 0      3.6  2.0  60   260 8.6 4.6 130 320
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 .21 .20 1.6  17 .0082 0      3.1  1.8  36   260 7.5 4.0 150 310
recursive-simple/fibo_10_true-unreach-call.c 2 .54 .53 5.2  17 .17   .0041 4.4  2.5  62   270 54   31   630 2800
recursive-simple/fibo_15_true-unreach-call.c 2 2.7  2.7  29    34 1.4    0      4.6  2.5  82   280 630   580   15000 6100
recursive-simple/fibo_20_true-unreach-call.c 1 360    360    2700    350 14      0      6.3  3.4  92   440 960   900   23000 5300
recursive-simple/fibo_25_true-unreach-call.c 0 850    850    3100    390 .14   0      .66 .41 8.6 40 6.1 3.2 110 320
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 .42 .42 4.0  17 .15   0      4.1  2.3  47   270 100   60   1600 3300
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 2.5  2.5  33    35 1.5    0      5.4  3.0  66   270 960   890   23000 5500
recursive-simple/fibo_2calls_20_true-unreach-call.c 1 380    380    2100    360 15      0      6.2  3.4  98   460 960   890   16000 5200
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 850    850    3500    390 .041  0      .53 .33 11   41 6.3 3.3 89 310
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 .21 .21 1.6  17 .0082 0      4.3  2.4  51   260 12   6.5 230 360
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 .18 .18 1.9  17 .0082 0      4.5  2.5  47   250 23   13   240 550
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 .17 .16 1.9  17 .0082 0      3.5  1.9  74   260 27   15   470 650
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 .21 .20 1.7  17 .0082 0      4.6  2.5  51   270 36   20   570 650
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 .34 .34 3.5  17 .074  0      3.4  1.9  48   260 47   28   460 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 .32 .32 3.0  17 .037  0      3.4  1.9  80   250 20   11   350 570
recursive-simple/fibo_7_true-unreach-call.c 2 .35 .35 3.4  17 .049  .16   4.2  2.3  47   260 25   14   470 670
recursive-simple/id2_b2_o3_true-unreach-call.c 0 850    850    5400    4900 4.5    0      .67 .43 8.1 42 6.5 3.4 120 300
recursive-simple/id2_b3_o5_true-unreach-call.c 0 850    850    6100    4900 4.5    0      .50 .33 11   39 6.1 3.2 120 300
recursive-simple/id2_b5_o10_true-unreach-call.c 0 850    850    3500    6800 9.8    0      .54 .34 11   41 6.5 3.4 120 300
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 .18 .18 1.6  17 .0082 0      3.7  2.1  71   270 14   7.7 270 470
recursive-simple/id_b2_o3_true-unreach-call.c 0 850    850    6200    6700 5.0    0      .49 .32 10   39 7.1 3.7 94 290
recursive-simple/id_b3_o5_true-unreach-call.c 0 850    850    6600    6700 4.9    0      .67 .44 7.8 40 5.8 3.0 93 300
recursive-simple/id_b5_o10_true-unreach-call.c 0 780    780    3300    15000 4.9    0      .60 .39 8.6 41 5.7 3.0 130 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 .46 .46 4.5  17 .053  0      3.6  2.0  45   260 17   9.3 240 520
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 .61 .60 7.0  17 .082  .16   4.0  2.3  43   260 23   13   370 610
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 .76 .76 7.6  17 .11   0      4.0  2.3  54   260 42   24   330 720
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 .91 .90 9.7  17 .15   0      4.4  2.5  45   260 39   23   550 800
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 .32 .31 2.8  17 .029  0      3.2  1.8  71   250 13   7.1 190 390
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 .51 .51 4.2  17 .053  0      4.3  2.4  53   260 19   11   200 580
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 .63 .63 5.2  17 .082  0      4.0  2.3  47   260 26   15   520 710
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 .80 .79 8.0  17 .11   0      3.4  1.9  81   260 37   22   540 750
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 .90 .90 9.8  17 .15   0      4.4  2.5  47   250 45   27   890 820
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 .20 .19 1.6  17 .0082 0      3.9  2.2  47   250 12   6.3 200 370
recursive-simple/sum_non_eq_true-unreach-call.c 0 850    850    10000    320 .32   0      .48 .30 10   40 6.0 3.2 120 300
recursive-simple/sum_non_true-unreach-call_true-termination.c 0 850    850    11000    260 .17   .14   .70 .44 7.8 40 5.7 3.0 110 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 86 24000 24000 140000 91000 160   13    98 1100 720 16000 54000   98 1200 680 17000 60000   98 130 76 2000 8900   98 5300 4700 110000 52000  
    correct results 57 82 25 25 250 1100 4.4 13    31 420 250 6100 20000   32 450 240 6700 15000   3 99 55 1400 6500   25 1300 970 25000 26000  
        correct true 25 50 14 13 140 450 3.1 .33 3 0 0 0 0   11 0 0 0 0   3 99 55 1400 6500   25 1300 970 25000 26000  
        correct false 32 32 11 11 110 660 1.3 13    28 420 250 6100 20000   21 450 240 6700 15000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 14 4 1200 1200 7600 2800 75   0    0 700 470 10000 34000   3 720 420 10000 44000   0 21 12 320 1400   0 3800 3600 86000 19000  
        correct-unconfirmed true 4 4 750 750 4900 770 31   0    0 0 0 0 0   3 0 0 0 0   0 21 12 320 1400   0 3800 3600 86000 19000  
        correct-unconfirmed false 10 0 440 440 2700 2000 44   0    0 700 470 10000 34000   0 720 420 10000 44000   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) 86
Run set sv-comp17.ReachSafety-Recursive